9th International Workshop on CPAchecker
(CPA 2024)

We give an overview of Kratos, a tool for the verification of imperative programs. Kratos operates on an intermediate verification language called K2, with a formal semantics based on Satisfiability Modulo Theories (SMT), allowing the specification of both reachability and liveness properties. It integrates several state-of-the-art verification engines based on SAT and SMT. Moreover, it provides additional functionalities such as a flexible API, a customizable C front-end, generation of counterexamples, support for simulation and symbolic execution, and translation into multiple low-level verification formalisms. In this talk, we will discuss the main features of Kratos, provide some details about its underlying verification engines, and overview some of its recent industrial applications.

Confidential computing is a rising security paradigm to protect data in use, especially when data are processed in pay-per-use cloud services. To prevent untrusted software of the host, e.g., virtual-machine managers (VMMs) or operating systems, from accessing the guests' data in the process, trusted execution environments should be used to isolate the guests' workloads. Intel's Trust Domain Extensions (TDX) introduces a firmware module between the host VMM and guest VMs and offers data confidentiality and integrity to cloud users, with the help of hardware extensions to the instruction-set architecture. We are interested in formally verifying the implementation of the TDX firmware module, which consists of C and assembly code that models and interacts with hardware. This talk will discuss properties the TDX firmware module should satisfy and the challenges of applying utomatic software verifiers for generic C programs, such as CPAchecker and CBMC, to verify these firmware properties.

I will present our joint work on CPA-Daemon. We use CPAchecker as a library to retain JIT optimizations and mitigate restart overhead.

There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. This hinders the integration of software model checking into the development process (continuous integration). We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries (block contracts) are computed — based on independent, distributed, continuous refinement by communication between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (computed from postconditions received from block predecessors, i.e., which program states reach this block) and violation conditions to check at the block exit (computed from violation conditions received from block successors, i.e., which program states lead to a specification violation). This separation of concerns leads to an architecture in which all blocks can be analyzed in parallel, as independent verification problems. Whenever new information (as a postcondition or violation condition) is available from other blocks, the verification can decide to restart with this new information. We realize our approach on the basis of configurable program analysis and implement it for the verification of C programs in the widely used verifier CPAchecker. A large experimental evaluation shows the potential of our new approach: The distribution of the workload to several processing units works well, and there is a significant reduction of the response time when using multiple processing units. There are even cases in which the new approach beats the highly-tuned, existing single-threaded predicate abstraction.

The existing Distributed Summary Synthesis is implemented as a monolithic, multi-threaded approach within CPAchecker. This approach has its limits with regards to concurrently running workers. To improve scalability, we decompose Distributed Summary Synthesis into individual services that communicate through the network. This talk presents our latest developments on this.

Assuring the correctness of computing systems is fundamental to our society and economy, and formal verification is a class of techniques approaching this issue with mathematical rigor. Researchers have invented numerous algorithms to automatically prove whether a computational model, e.g., a software program or a hardware digital circuit, satisfies its specification. In the past two decades, Craig interpolation has been widely used in both hardware and software verification. Despite the similarities in the theoretical foundation between hardware and software verification, previous works usually evaluate interpolation-based algorithms on only one type of verification tasks (e.g., either circuits or programs), so the conclusions of these studies do not necessarily transfer to different types of verification tasks. To investigate the transferability of research conclusions from hardware to software, we adopt two performant approaches of interpolation-based hardware model checking, (1) Interpolation-Sequence-Based Model Checking (Vizel and Grumberg, 2009) and (2) Intertwined Forward-Backward Reachability Analysis Using Interpolants (Vizel, Grumberg, and Shoham, 2013), for software verification. We implement the algorithms proposed by the two publications in the software verifier CPAchecker because it has a software-verification adoption of the first interpolation-based algorithm for hardware model checking from 2003, which the two publications use as a comparison baseline. To assess whether the claims in the two publications transfer to software verification, we conduct an extensive experiment on the largest publicly available suite of safety-verification tasks for the programming language C. Our experimental results show that the important characteristics of the two approaches for hardware model checking are transferable to software verification, and that the cross-disciplinary algorithm adoption is beneficial, as the approaches adopted from hardware model checking were able to tackle tasks unsolvable by existing methods. This work consolidates the knowledge in hardware and software verification and provides open-source implementations to improve the understanding of the compared interpolation-based algorithms.

Verification witnesses are objects containing useful information to either aid the verification of a program or identify potential counterexamples. Primarily produced by automatic software verifiers, they can be used to not only confirm or refute verification results, but also for general exchange of information among various tools. This talk will provide an introduction to witnesses and a brief introduction in how they are exported and used inside CPAchecker.

Software specifications often come in the form of contracts, detailing in particular pre- and postconditions of functions, libraries or modules. Research on contracts often centers around questions of contract inference or contract validation. We study the less investigated aspect of quality of contracts. More specifically, we define the concept of redundancy for preconditions and propose three techniques with differing efficiency and effectiveness for detecting redundant preconditions. All three techniques are implemented within the software verification tool CPAchecker, and we present results of an experimental evaluation on a dataset of around 40 C programs. The results confirm differences in precision and resource consumption of the techniques, but the experiments also reveal unexpected outcomes about the completeness of the most precise, predicate analysis based technique.

Since last year, we have two termination analyses implemented in CPAchecker. The older one - LassoRankerAnalysis - focuses on finding a ranking function and hence proving the termination, whereas the new one goals to transform the liveness property into a safety one and solve termination using a reachability analysis. In the talk I will introduce the ideas behind the new analysis and show the results when the two analyses are combined.

CPAchecker removed its old Symbolic Memory Graph (SMG) based MemorySafety analysis in favor of a new SMG analysis. This new analysis debuted at SV-COMP 2024 and has since been improved. We will give a brief overview of the current state of our new SMG based analysis, as well as planned future developments.

JavaSMT 5 has recently been released and is now usable in CPAchecker. We will discuss the new features of JavaSMT, for example the two new additional SMT solvers Bitwuzla and OpenSMT, as well as a new automated debugger for common errors. Furthermore, we will also talk about new developments that are currently being worked on.

CPAchecker is currently hosted in a Subversion repository, but most developers use Git as their primary version-control system, and switching to Git is a common wish of CPAchecker developers. The remaining blockers for this have been removed in the past months, and now is the time to switch the CPAchecker repository fully to Git. In this session we will present the plan and collect feedback, both for the immediate switch as well as for the repository organization and development process of CPAchecker in the future. The latter includes for example topics such as the branch-management policy, push permissions to the main branch, and an increased use of merge requests and reviews.