Abstract In this paper, we present rIC3, an efficient bit-level hardware model checker primarily based on the IC3 algorithm. It boasts a highly efficient implementation and integrates several recently proposed optimizations, such as the specifically optimized SAT solver, dynamically adjustment of generalization strategies, and the use of predicates with internal signals, among others. As a first-time participant in the Hardware Model Checking Competition, rIC3 was independently evaluated as the best-performing tool, not only in the bit-level track but also in the word-level bit-vector track through bit-blasting. Our experiments further demonstrate significant advancements in both efficiency and scalability. rIC3 can also serve as a backend for verifying industrial RTL designs using SymbiYosys. Additionally, the source code of rIC3 is highly modular, with the IC3 algorithm module being particularly concise, making it an academic platform that is easy to modify and extend.

Abstract The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and completeness. It utilizes SAT solvers to solve a series of SAT queries associated with relative induction. In this paper, we introduce several optimizations for the SAT solver in IC3 based on our observations of the unique characteristics of these SAT queries. By observing that SAT queries do not necessarily require decisions on all variables, we compute a subset of variables that need to be decided before each solving process while ensuring that the result remains unaffected. Additionally, noting that the overhead of binary heap operations in VSIDS is non-negligible, we replace the binary heap with buckets to achieve constant-time operations. Furthermore, we support temporary clauses without the need to allocate a new activation variable for each solving process, thereby eliminating the need to reset solvers. We developed a novel lightweight CDCL SAT solver, GipSAT, which integrates these optimizations. A comprehensive evaluation highlights the performance improvements achieved by GipSAT. Specifically, the GipSAT-based IC3 demonstrates an average speedup of $$3.61$$ 3.61 times in solving time compared to the IC3 implementation based on MiniSat.

Model checking is an automated method used to formally verify systems by checking them against properties. However, a major problem in model checking is the state explosion. To overcome this challenge, one approach is to utilize parallel processing capabilities to either speed up computations or handle larger-scale problems. Explicit model checking has lower computational complexity and can be easily parallelized. There are numerous parallel explicit model checking algorithms available in the literature. Symbolic model checking offers significant advantages over explicit model checking in terms of problem scalability and verification speed. However, treating states encountered during the search as sets poses a challenge in devising efficient parallel algorithms. As a result, current research on parallelizing symbolic model checking has primarily focused on reachability analysis or safety properties, rather than attempting to parallelize the nested fixpoint calculations. In this paper, we propose a novel property-driven approach for parallel symbolic model checking of full LTL. Our algorithm introduces a fair model state labelling function that forms a partition of the nested fixpoint across the product combining the model and the property Büchi automaton. The experimental results demonstrate significant speedup, ranging from 2.81 to 17.19 times compared to sequential approaches on a 32-core machine. Moreover, in comparison to existing parallel model checking methods, our approach not only surpasses those relying on BDD libraries with a maximum improvement of up to 134% and an average improvement of 33.1% but also demonstrates significant superiority over the state-of-theart parallel explicit model checker.

In an operating system, the file system manages data and provides security guarantees. The features of delayed write and crash safety increase the complexity of a concurrent file system, which in turn increases the likelihood of data leakage. Formal verification methods, through rigorous mathematical proofs, can ensure the correctness of a file system. However, due to the limitations of concurrent separation logic, the verification of concurrent file systems that combine crash safety and delayed write has not been fully explored. This study extends concurrent separation logic with the non-persistent conditions to model the non-persistent state under delayed write and uses tree space to capture state changes to verify the properties that the file system must adhere to. Based on the extended concurrent separation logic and tree space, this paper provides a formal specification and proof of the correctness properties that must be satisfied. During the proof process, a correctness theorem is presented which ensures consistency between the file system behavior and the formal specification. The results of the experimental evaluation show that the formal verification method proposed in this paper ensures the correctness of the file system implementations. Furthermore, compared to existing verified concurrent file systems, NPFS demonstrates better performance.

Design verification is a complex and costly task, especially for large and intricate processor projects. Formal verification techniques provide advantages by thoroughly examining design behaviors, but they require extensive labor and expertise in property formulation. Recent research focuses on verifying designs using the self-consistency universal property, reducing verification difficulty as it is design-independent. However, the single self-consistency property faces false positives and scalability issues due to exponential state space growth. To tackle these challenges, this paper introduces TIUP, a technique using tautologies as universal properties. We show how TIUP effectively uses tautologies as abstract specifications, covering processor data and control paths. TIUP simplifies and streamlines verification for engineers, enabling efficient formal processor verification.

Symbolic quick error detection (SQED) has greatly improved efficiency in formal chip verification. However, it has a limitation in detecting single-instruction bugs due to its reliance on the self-consistency property. To address this, we propose a new variant called symbolic quick error detection by semantically equivalent program execution (SEPE-SQED), which utilizes program synthesis techniques to find sequences with equivalent meanings to original instructions. SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program (instruction sequence). To manage the search space associated with program synthesis, we introduce the CEGIS based on the highest priority first algorithm. The experimental results show that our proposed CEGIS approach improves the speed of generating the desired set of equivalent programs by 50% in time compared to previous methods. Compared to SQED, SEPE-SQED offers a wider variety of instruction combinations and can provide a shorter trace for triggering bugs in certain scenarios.

The IC3 algorithm, also known as PDR, has made a significant impact in the field of safety model checking in recent years due to its high efficiency, scalability, and completeness. The most crucial component of IC3 is inductive generalization, which involves dropping variables one by one and is often the most time-consuming step. In this paper, we propose a novel approach to predict a possible minimal lemma before dropping variables by utilizing the counterexample to propagation (CTP). By leveraging this approach, we can avoid dropping variables if predict successfully. The comprehensive evaluation demonstrates a commendable success rate in lemma prediction and a significant performance improvement achieved by our proposed method.

Speculative execution attacks exploit incorrect speculation to execute malicious instructions and leak data via microarchitectural covert channels. Existing mitigations focus on restricting transmission-related instructions related to covert channels. In this paper, we propose the Execute on Clear (EoC), which offers an efficient defense strategy against covert channels in speculative execution attacks. EoC employs a two-stage identification method, which precisely identifies malicious transmission-related instructions by considering both the insecure data dependency and the status of microarchitecture components exploited by the attack. Moreover, with identification results, EoC guarantees the safe execution of transmission-related instructions, preventing unnecessary blocking. By reducing the misidentification and the blocked execution of such instructions, EoC avoids unnecessary maintenance operations and reduces performance overheads. We evaluate EoC on SPEC2006 and PARSEC3.0 workloads, revealing a performance overhead of merely 0.98% and 3.29% in the Spectre and Futuristic defense models, respectively. Notably, EoC exhibits lower performance overhead in comparison to existing methods.

In recent years, speculative execution attacks bring severe threats to hardware security. An attacker tempts the victim process to read secret data during speculative execution and recovers it via micro-architectural covert channels. Most defense strategies in the literature adopt a blocking approach, in which the execution of malicious speculative instructions is withheld until they become safe and, thus, excessive performance overhead is inevitable. Although several non-blocking approaches have also been proposed, extra hardware components are introduced to buffer data of speculative cache accesses, bringing on significant hardware costs. In this paper, we propose the Secure Access Policy (SAP) to enable the non-blocking execution of malicious speculative instructions in an isolated environment, which reuses the existing Line Fill Buffer and Translation Lookaside Buffer, without introducing any new hardware component. The isolated environment, named Safe Shelter area (SS area), maintains the data accessed by malicious speculative instructions and those data cannot be transmitted to the outside. An improved taint tracking technique is introduced to effectively reduce the number of accesses to the SS area. In addition, an extended cache coherence mechanism and a process-bound technique are also proposed to guarantee the validity and security of SS area’s data. We evaluate SAP on SPEC2006 and PARSEC3.0 workloads. The evaluation results show that SAP can effectively defend those attacks leveraging speculative executions and cache covert channels, and outperforms existing approaches in performance overhead, 2.35% and 3.21% in the Spectre and Futuristic defense models, respectively.

One critical challenge of designing an efficient prefetcher is to strike a balance between performance and hardware overhead. Some state-of-the-art prefetchers achieve very high performance at the price of a very large storage requirement, which makes them not amenable to hardware implementations in commercial processors. We argue that merging memory access patterns can be a feasible solution to reducing storage overhead while obtaining high performance, although no existing prefetchers, to the best of our knowledge, have succeeded in doing so because of the difficulty of designing an effective merging strategy. After analysis of a large number of patterns, we find that the address offset of the first access in a certain memory region is a good feature for clustering highly similar patterns. Based on this observation, we propose a novel hardware data prefetcher, named Pattern Merging Prefetcher (PMP), which achieves high performance at a low cost. The storage requirement for storing patterns is largely reduced and, at the same time, the prefetch accuracy is guaranteed by merging similar patterns in the training process. In the prefetching process, a strategy based on access frequencies of prefetch candidates is applied to accurately extract prefetch targets from merged patterns. According to the experimental results on a wide range of various workloads, PMP outperforms the enhanced Bingo by 2.6% with 30× lesser storage overhead and Pythia by 8.2% with 6× lesser storage overhead.

To learn complex memory access patterns effectively, many spatial data prefetchers have been proposed that characterize the patterns as fixed-length delta sequences. However, because complex patterns are variable in workloads, it is difficult for fixed-length delta sequences to recognize them with both high competitive coverage and accuracy. That is, longer delta sequences increase accuracy at a lower probability of pattern matching, while shorter delta sequences increase coverage at a higher probability of false predictions. A classical strategy is to introduce the multiple matching mechanism associated with variable-length delta sequences, but sequences have to be redundantly stored in multiple tables.

Kernel rootkits pose a serious threat to system security by tampering with the state of operating system inconspicuously. To ensure operating system kernel integrity, Virtual Machine Monitor (VMM) based approaches have been proposed. Most of these approaches use snapshot-based or event-triggered techniques. However, snapshot-based techniques have been suffering from missing transient attacks or significant performance overhead, while event-triggered methods are facing with heavy workload as integrity checking might be triggered by any suspicious actions. In this paper, we propose a novel solution which is a behavior-triggered integrity checking approach named BehaviorKI. By analyzing attacking processes, BehaviorKI can extract a set of behavior patterns which characterize malicious behaviors. BehaviorKI will trigger integrity checking with kernel invariants when a malicious behavior pattern detected. In this way, our approach can alleviate the performance burden by reducing the frequent kernel integrity checking. The experiment results show that Be-haviorKI outperforms existing snapshot-based and event-triggered approaches.

Covert channels are widely considered as a major risk of information leakage in various operating systems, such as desktop, cloud, and mobile systems. The existing works of modeling covert channels have mainly focused on using finite state machines (FSMs) and their transforms to describe the process of covert channel transmission. However, a FSM is rather an abstract model, where information about the shared resource, synchronization, and encoding/decoding cannot be presented in the model, making it difficult for researchers to realize and analyze the covert channels. In this paper, we use the high-level Petri Nets (HLPN) to model the structural and behavioral properties of covert channels. We use the HLPN to model the classic covert channel protocol. Moreover, the results from the analysis of the HLPN model are used to highlight the major shortcomings and interferences in the protocol. Furthermore, we propose two new covert channel models, namely: (a) two channel transmission protocol (TCTP) model and (b) self-adaptive protocol (SAP) model. The TCTP model circumvents the mutual inferences in encoding and synchronization operations; whereas the SAP model uses sleeping time and redundancy check to ensure correct transmission in an environment with strong noise. To demonstrate the correctness and usability of our proposed models in heterogeneous environments, we implement the TCTP and SAP in three different systems: (a) Linux, (b) Xen, and (c) Fiasco.OC. Our implementation also indicates the practicability of the models in heterogeneous, scalable and flexible environments.

Studying the spread of phenomena in social networks is critical but still not fully solved. Existing influence maximization models assume a static network, disregarding its evolution over time. We introduce the continuous time constrained influence maximization problem for dynamic diffusion networks, based on a novel diffusion model called DynaDiffuse. Although the problem is NP-hard, the influence spread functions are monotonic and submodular, enabling fast approximations on top of an innovative stochastic model checking approach. Experiments on real social network data show that our model finds higher quality solutions and our algorithm outperforms state-of-art alternatives.

Selection of the right user stories and planning their implementation for the next iteration is critical for success of extreme Programming (XP). Success here is measured by the total business value generated from all user stories implemented within time. The business value of an iteration is composed by the value of the individual user stories selected and additional value created from themes of user stories. In this paper, a method combining advanced search and risk analysis is proposed to support decision-making for the "best" set of user stories. The advanced search technique combines genetic search with subsequent application of the hill climbing technique. The top candidate solutions are further analyzed pro-actively in terms of their risk to be implementable in-time with the available effort. As a proof-of-concept, the applicability of the proposed method is applied for the planning of one iteration in a case study project with 40 user stories. As a result, a set of trade-off solutions is offered as decision support for XP teams.

Productivity is a crucial concern for most software organizations. It can help project managers to make project plan, supervise project progress, and measure the project members' performance. Thus it has been widely measured and analyzed by both industry and researchers. But in the actual software project management, the project data filled by the developers may be incomplete and imprecise. Especially it is very hard for the developers to give the precise work product scale of each task. Therefore, the productivity calculated basing on those data is also imprecise. To solve the problem, this paper presents a method for precise productivity estimation. The method calculates work product scale of each task using change set size information by rebuilding relationships between the tasks and the SVN commits, and then calculates the productivity. And an experimental study has been done basing on Qone. Qone is an integrated system for project management developed by Institute of Software Chinese Academy of Sciences (ISCAS). It has been used in more than 200 software companies in China.

The features in multi-threaded programs, such as recursion, dynamic creation and communication, pose a great challenge to formal verification. A widely adopted strategy is to verify tentatively a system with a smaller size, by limiting the depth of recursion or the number of replicated processes, to find errors without ensuring the full correctness. The model checking of parameterized systems, a parametric infinite family of systems, is to decide if a property holds in every size instance. There has been a quest for finding cut-offs for the verification of parameterized systems. The basic idea is to find a cut-off on the number of replicated processes or on the maximum length of paths needed to prove a property, standing a chance of improving verification efficiency substantially if one can come up with small or modest cut-offs. In this paper, a novel approach, called Forward Bounded Reachability Analysis (FBRA), based upon the cut-off on the maximum lengths of paths is proposed for the verification of parameterized systems. Experimental results show that verification efficiency has been significantly improved as a result of the introduction of our new cut-offs.