Abstract:The performance acceleration of high-performance libraries on CPUs can be achieved by efficiently leveraging SIMD hardware through vectorization. Implementing vectorization depends on programming methods specific to the target SIMD hardware. However, the programming models and methods of different SIMD extensions vary significantly. To avoid redundant implementation of algorithm optimizations across various platforms and improve the maintainability of algorithm libraries, a hardware abstraction layer (HAL) is often introduced in high-performance libraries. Since existing SIMD extension instruction sets are designed with fixed-length vector registers, most hardware abstraction layers only support fixed-length vector types and operations. However, the design of fixed-length vector representations in hardware abstraction layers cannot accommodate the variable vector register lengths introduced by the RISC-V vector extension. Treating RISC-V vector extensions as fixed-length vectors within existing HAL designs would introduce unnecessary overhead and cause performance degradation. To address this problem, the paper proposes a HAL design method compatible with variable-length vector extension platforms and fixed-length SIMD extension platforms. Based on our method, the OpenCV universal intrinsic functions have been redesigned and optimized to support RISC-V vector extension devices better while maintaining compatibility with existing SIMD platforms. Moreover, we designed experiments to compare the performance of the OpenCV library optimized using our approach against the original version. The results demonstrate that the universal intrinsic redesigned by our method efficiently integrates RISC-V vector extensions into the hardware abstraction layer optimization framework. Our method achieved a 3.93x performance improvement in core modules, significantly enhancing the execution performance of the high-performance library on RISC-V devices, thereby validating the effectiveness of this paper. Additionally, our work has been open-sourced and integrated into the OpenCV source code, demonstrating our approach’s practicality and application value.

Abstract:Fuzz testing techniques play a significant role in software quality assurance and software security testing. However, when dealing with systems like compilers that have complex input semantics, existing fuzz testing tools often struggle as a lack of semantic awareness in their mutation strategies leads to the generated programs failing to pass compiler frontend checks. This study proposes a semantically-aware greybox fuzz testing method, aiming at enhancing the efficiency of fuzz testing tools in the domain of compiler testing. It designs and implements a series of mutation operators that can maintain input semantic validity and explore contextual diversity, and develops efficient selection strategies according to the characteristics of these operators. The greybox fuzz testing tool SemaAFL is developed by integrating these strategies with traditional greybox fuzz testing tools. Experimental results indicate that by applying these mutation operators, SemaAFL achieves approximately 14.5% and 11.2% higher code coverage on GCC and Clang compilers compared to AFL++ and similar tools like GrayC. During a week-long experimental period, six previously unknown bugs in GCC and Clang are discovered and reported by SemaAFL.

Abstract:Java has become one of the most popular programming languages for application project development nowadays, due to its rich dependency libraries and convenient build tools such as Maven and Gradle. However, with the continuous increase in the scale of dependency libraries, the dependency management of Java projects becomes increasingly complex and constantly exceeds the management capabilities of existing tools. The potential problems are likely to be triggered unexpectedly, seriously affecting the building and running of the current project and other projects in the Java ecosystem, such as causing build errors, runtime crashes, or semantic conflicts. This study aims to address the gaps in the analysis of dependency management issues found in existing research and technical literature by introducing the concept of “dependency smell”, to build a unified model for these challenges. This study conducts a comprehensive empirical study on dependency management issues, covering all categories of Maven and Gradle related problems. This study analyzes diverse dependency management issues gathered from open-source communities (e.g., GitHub), official documentation (e.g., Maven manual), as well as various surveys and technical papers. Finally, 13 types of dependency smell, as well as their triggering roots and impact characteristics, are summarized. Based on the findings of this empirical study, a unified detection algorithm for dependency smells in Java projects is designed, and a special detection tool JDepAna suitable for Maven and Gradle build tools is implemented. Experimental results demonstrate that for known dependency smells, JDepAna achieves a detection recall rate of 95.9%. For hundreds of new Java projects, JDepAna detects 30689 instances of dependency smells. 360 instances are selected, and the true positive rate of manual verification reaches 96.1%. Additionally, this study reports 48 instances to developers, with 42 instances promptly confirmed and 21 promptly fixed, thereby validating the efficacy and practicality of the proposed Java dependency smell detection algorithm and tool in facilitating quality assurance for Java projects.

Abstract:With the rapid development of information technology, security authentication technology has become a crucial safeguard for personal privacy and data security. Among them, iris recognition technology, with its outstanding accuracy and stability, is widely applied in fields such as system access control, healthcare, and judicial practices. However, once the iris feature data of a user is leaked, it means permanent loss, as it cannot be changed or revoked. Therefore, the privacy protection of iris feature data is particularly important. With the prominent performance of neural network technology in image processing, secure iris recognition schemes based on neural networks have been proposed, which maintain the high performance of recognition systems while protecting privacy data. However, in the face of constantly changing data and environments, secure iris recognition schemes are required to have effective scalability, that is, the recognition scheme should be able to maintain performance with new user registrations. However, most of the existing research on neural network-based secure iris recognition schemes does not consider the scalability of the schemes. Aiming at the above problems, the generative feature replay-based secure incremental iris recognition (GFR-SIR) method and the privacy-preserving template replay-based secure incremental iris recognition (PTR-SIR) method are proposed in this study. Specifically, the GFR-SIR method uses generative feature replay and feature distillation techniques to alleviate the forgetting of previous task knowledge during the expansion of neural networks and adopts the improved TNCB method to protect the privacy of iris feature data. The PTR-SIR method preserves the privacy-protecting templates obtained through the TNCB method in previous tasks and replays these templates during the model training of the current task to achieve the scalability of the recognition scheme. Experimental results show that after completing 5 rounds of expansion tasks, the recognition accuracy of GFR-SIR and PTR-SIR on the CASIA-Iris-Lamp dataset reaches 68.32% and 98.49% respectively, which is an improvement of 58.49% and 88.66% compared with the fine-tuning method. The analysis indicates that the GFR-SIR method has significant advantages in terms of security and model training efficiency since the data of previous tasks is not saved; while the PTR-SIR method is more outstanding in maintaining recognition performance, but its security and efficiency are lower than those of GFR-SIR.

Abstract:Constraint solving is a fundamental approach for verifying deep neural network (DNN). In the field of AI safety, DNNs often undergo modifications in their structure and parameters for purposes such as repair or attack. In such scenarios, the problem of incremental DNN verification is proposed, which aims to determine whether a safety property still holds after the DNN has been modified. To address this, an incremental satisfiability modulo theory (SMT) algorithm based on the Reluplex framework is presented. The proposed algorithm, DeepInc, leverages the key features of the configurations from the previous solving procedure, heuristically checking whether these features can be applied to prove the correctness of the modified DNN. Experimental results demonstrate that DeepInc outperforms Marabou in terms of efficiency in most cases. Moreover, for cases where the safety property is violated both before and after modification, DeepInc achieves significantly faster performance, even when compared to the state-of-the-art verifier α, β-CROWN.

Abstract:The single-sphere driven balancing robot is an omnidirectional mobile robot, whose flexibility is particularly evident in narrow or complex environments. During the design of the kinematics and dynamics for this type of robot, it is crucial to ensure the correctness of the model. Traditional methods based on testing and simulation may not cover all system states and thus might fail to identify certain design flaws or potential safety risks. To ensure that the single-sphere driven balancing robot satisfies the correctness and safety verification requirements for safety-critical robots, a formal model of its kinematics and dynamics is constructed using the HOL Light theorem prover. The model is based on theorem libraries such as the real analysis library, matrix analysis library, and robot kinematics and dynamics library, and involves higher-order logic derivation and proof.

Abstract:The operating system serves as the foundational platform for software, and the security of its kernel is often of paramount importance. Rust, a memory-safe programming language that has steadily gained popularity, incorporates safety mechanisms such as lifetimes, ownership, borrowing checks, and RAII. Using Rust to build kernels has emerged as a prominent area of research. However, systems built with Rust often include some unsafe code segments, which prevent the language from offering comprehensive safety guarantees at the language level. As a result, verifying these unsafe code segments is essential to ensuring the correctness and reliability of Rust-based kernels. This study proposes a method for combining the safe and unsafe code segments, called GhostFunc, to verify a microkernel constructed with Rust. Different levels of abstraction are applied to the two types of code segments, and GhostFunc is used for combined verification. Focusing on the task management and scheduling module, this study formalizes unsafe code segments such as Arc using λRust and presents the formal implementation of GhostFunc. An example verification of this method is also provided. All verification efforts are based on theorem proving, and correctness is validated in Coq using the Iris separation logic framework.

Abstract:Dynamic order statistic tree structures are a type of data structure that integrates the features of dynamic sets, order statistics, and search tree structures, supporting efficient data retrieval operations. These structures are widely used in fields such as database systems, memory management, and file management. However, current research primarily focuses on structural invariants, such as balance, while neglecting discussions on functional correctness. In addition, existing research methods mainly involve manual derivation or interactive mechanized verification for specific algorithms, lacking mature and reliable general verification frameworks and exhibiting a low level of automation. To address this, a functional modeling and automated verification framework for dynamic order statistic search tree structures, based on Isabelle, has been designed. A verified general lemma library is established to reduce the time and cost of code verification for developers. Using this functional modeling framework, unbalanced binary search trees, balanced binary search trees (exemplified by red-black trees), and balanced multi-way search trees (exemplified by 2–3 trees) are selected as instantiated cases for demonstration. With the help of the automated verification framework, multiple instantiated cases can be automatically verified by simply using induction and invoking the auto method once, or by using the try command. This provides a reference for automated verification of functional and structural correctness in complex data structure algorithms.

Abstract:The synchronous dataflow language Lustre is commonly used in the development of safety-critical systems. However, existing official code generators and the SCADE KCG code generator have not been formally verified, and their inner workings remain opaque to users. In recent years, translation validation methods that indirectly verify compiler correctness by proving the equivalence between source and target code have proven successful. This study proposes a trusted compilation method for the Lustre language, based on a pushdown automaton compilation approach and a semantic consistency verification method. The proposed method successfully implements a trusted compiler from Lustre to C and rigorously proves the translation process’s correctness using Isabelle.

Abstract:Operating system (OS) kernels serve as the foundation for designing safety-critical software systems. The correct functioning of computer system depends on the correctness of the underlying OS kernels, making their formal verification a critical task. However, behaviors such as multi-task concurrency, data sharing, and race conditions inherent in OS kernels pose significant challenges for formal verification. In recent years, theorem-proving methods have been widely applied to verify the functionality of OS kernel modules, achieving notable successes. The capability-based access control module in OS kernels provides fine-grained access control, designed to prevent unauthorized users from accessing kernel resources and services. Its implementation involves capability spaces for tasks, which form a set of tree structures. Each capability node includes nested, complex data structures and capability functions frequently perform operations such as access, modification, and recursive deletion of capability spaces. These factors make the formal verification of capability-based access control significantly more challenging compared to other OS modules. This study employs concurrent separation logic with refinement (CSL-R) to verify the functional correctness of a capability-based access control module in the aerospace embedded domain. The verification establishes refinement between the API functions of the capability module and their abstract specifications. First, the capability data structure is formally molded, followed by the definition of a global invariant to ensure the consistency of capability spaces. Next, the preconditions and postconditions for internal functions and the abstract specifications for API functions are defined to reflect functional correctness. Finally, the refinement between the C implementation of the API functions and their abstract specifications is rigorously proven. All definitions and verification steps are formalized using the Coq theorem prover. During the verification process, errors are identified in the C implementation, which are subsequently confirmed and corrected by the OS kernel designers.