Abstract Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve, e.g., abstract data types. In this work, we leverage structured prompts to elicit Large Language Models (LLMs) to generate auxiliary lemmas that are necessary for reasoning about these inductive definitions. We further propose a neuro-symbolic approach, which synergistically integrates LLMs with constraint solvers: the LLM iteratively generates conjectures, while the solver checks their validity and usefulness for proving the goal. We evaluate our approach on a diverse benchmark suite comprising constraints originating from algebraic data types and recurrence relations. The experimental results show that our approach can improve the state-of-the-art SMT and CHC solvers, solving considerably more (around 25%) proof tasks involving inductive definitions, demonstrating its efficacy.

Chisel is an open-source hardware description language embedded in Scala to facilitate parameterized and reusable digital circuit design. Chisel is becoming increasingly popular and has been used to design RISC-V CPUs, e.g. RocketChip and XiangShan. While Chisel features high-level hardware designs, its verification is still low-level: Low-level (e.g. Verilog) programs are first generated from Chisel programs, then the verification tools are applied to these low-level programs. In this work, we focus on formal verification of arithmetic units. Efficient low-level formal verification of arithmetic units has always been a challenge and remains an active research area, attributed to the state explosion problem brought on by bit widths. To circumvent this problem for arithmetic Chisel designs, we propose an approach to their high-level formal verification so that their correctness is verified for all bit widths at once, instead of for each bit width separately. The key idea is to transform arithmetic Chisel designs into Scala software programs that simulate their behaviors, where the high-level features are preserved, then resort to Stainless, a deductive formal verification tool for Scala. We validate the effectiveness of this approach by formally verifying the correctness of dividers and multipliers in two representative open source RISC-V processors, namely, RocketChip and XiangShan. Compared to the existing proof-assistant-based parameterized verification approaches for arithmetic designs (e.g. Kami), the verification cost in our approach is much lower on average.

As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. While there are techniques for verifying DNNs with formal guarantees, they are limited in scalability and accuracy. In this article, we present a novel counterexample-guided abstraction refinement (CEGAR) approach for scalable and exact verification of DNNs. Specifically, we propose a novel abstraction to break down the size of DNNs by over-approximation. The result of verifying the abstract DNN is conclusive if no spurious counterexample is reported. To eliminate each spurious counterexample introduced by abstraction, we propose a novel counterexample-guided refinement that refines the abstract DNN to exclude the spurious counterexample while still over-approximating the original one, leading to a sound, complete yet efficient CEGAR approach. Our approach is orthogonal to and can be integrated with many existing verification techniques. For demonstration, we implement our approach using two promising tools, Marabou and Planet , as the underlying verification engines, and evaluate on widely used benchmarks for three datasets ACAS , Xu , MNIST , and CIFAR-10 . The results show that our approach can boost their performance by solving more problems in the same time limit, reducing on average 13.4%–86.3% verification time of Marabou on almost all the verification tasks, and reducing on average 8.3%–78.0% verification time of Planet on all the verification tasks. Compared to the most relevant CEGAR-based approach, our approach is 11.6–26.6 times faster.

Abstract We present a certified algebraic abstraction technique for verifying bit-accurate non-linear integer computations. In algebraic abstraction, programs are lifted to polynomial equations in the abstract domain. Algebraic techniques are employed to analyze abstract polynomial programs; SMT QF_BV solvers are adopted for bit-accurate analysis of soundness conditions. We explain how to verify our abstraction algorithm and certify verification results. Our hybrid technique has verified non-linear computations in various security libraries such as Bitcoin and OpenSSL. We also report the certified verification of Number-Theoretic Transform programs from the post-quantum cryptosystem Kyber.

Abstract We present the verified model checker CoqCryptoLine for cryptographic programs with certified verification results. The CoqCryptoLine verification algorithm consists of two reductions. The algebraic reduction transforms into a root entailment problem; and the bit-vector reduction transforms into an SMTQF_BV problem. We specify and verify both reductions formally using Coq with MathComp. The CoqCryptoLine tool is built on the OCaml programs extracted from verified reductions. CoqCryptoLine moreover employs certified techniques for solving the algebraic and logic problems. We evaluate CoqCryptoLine on cryptographic programs from industrial security libraries.

Correct implementations of cryptographic primitives are essential for modern security. These implementations often contain arithmetic operations involving non-linear computations that are infamously hard to verify. We present llvm2CryptoLine, an automated formal verification tool for arithmetic operations in cryptographic C programs. llvm2CryptoLine successfully verifies 51 arithmetic C programs from industrial cryptographic libraries OpenSSL, wolfSSL and NaCl. Most of the programs are verified fully automatically and efficiently. A screencast that showcases llvm2CryptoLine can be found at https://youtu.be/QXuSmja45VA. Source code is available at https://github.com/fmlab-iis/llvm2cryptoline.

Robustness of neural networks need be guaranteed in many safety-critical scenarios, such as autonomous driving and cyber-physical controlling. In this paper, we present MpBP, a tool for verifying the robustness of neural networks. MpBP is inspired by classical bound propagation methods for neural network verification, and aims to improve the effectiveness by exploiting the notion of propagation paths. Specifically, MpBP extends classical bound propagation methods, including forward bound propagation, backward bound propagation, and forward+backward bound propagation, with multiple propagation paths. MpBP is based on the widely-used PyTorch machine learning framework, hence providing efficient parallel verification on GPUs and user-friendly usage. We evaluate MpBP on neural networks trained on standard datasets MNIST, CIFAR-10 and Tiny ImageNet. The results demonstrate the effectiveness advantage of MpBP beyond two state-of-the-art bound propagation tools LiRPA and GPUPoly, with comparable efficiency to LiRPA and significantly higher efficiency than GPUPoly. A video demonstration that showcases the main features of MpBP can be found at https://youtu.be/3KyPMuPpfR8. Source code is available at https://github.com/formes20/MpBP and https://doi.org/10.5281/zenodo.7029261.

Abstract User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom’s decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, confluence of a terminating set of left-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. The present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pairs. The rewrite relation used for analyzing confluence may rewrite arbitrarily many non-overlapping redexes in a single step. This relation gives rise to critical pairs that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. Practical examples of use of this technique are analyzed.

Abstract We present a certified SMT QF_BV solver CoqQFBV built from a verified bit blasting algorithm, Kissat, and the verified SAT certificate checker GratChk in this paper. Our verified bit blasting algorithm supports the full QF_BV logic of SMT-LIB; it is specified and formally verified in the proof assistant Coq . We compare CoqQFBV with CVC4, Bitwuzla, and Boolector on benchmarks from the QF_BV division of the single query track in the 2020 SMT Competition, and real-world cryptographic program verification problems. CoqQFBV surprisingly solves more program verification problems with certification than the 2020 SMT QF_BV division winner Bitwuzla without certification.

We develop an automated formal technique to specify and verify signed computation in cryptographic programs. In addition to new instructions, we introduce a type system to detect type errors in programs. A type inference algorithm is also provided to deduce types and instruction variants in cryptographic programs. In order to verify signed cryptographic C programs, we develop a translator from the GCC intermediate representation to our language. Using our technique, we have verified 82 C functions in cryptography libraries including NaCl, wolfSSL, bitcoin, OpenSSL, and BoringSSL.

Today, large and complex software is developed with integrated components using application programming interfaces (APIs). Correct usage of APIs in practice presents a challenge due to implicit constraints, such as call conditions or call orders. API misuse, i.e., violation of these constraints, is a well-known source of bugs, some of which can cause serious security vulnerabilities. Although researchers have developed many API-misuse detectors over the last two decades, recent studies show that API misuses are still prevalent. In this paper, we provide a comprehensive empirical study on API-misuse bugs in open-source C programs. To understand the nature of API misuses in practice, we analyze 830 API-misuse bugs from six popular programs across different domains. For all the studied bugs, we summarize their root causes, fix patterns and usage statistics. Furthermore, to understand the capabilities and limitations of state-of-the-art static analysis detectors for API-misuse detection, we develop APIMU4C, a dataset of API-misuse bugs in C code based on our empirical study results, and evaluate three widely-used detectors on it qualitatively and quantitatively. We share all the findings and present possible directions towards more powerful API-misuse detectors.

Cryptographic primitives are ubiquitous for modern security. The correctness of their implementations is crucial to resist malicious attacks. Typical arithmetic computation of these C programs contains large numbers of non-linear operations, hence is challenging existing automatic C verification tools. We present an automated approach to verify cryptographic C programs. Our approach successfully verifies C implementations of various arithmetic operations used in NIST P-224, P-256, P-521 and Curve25519 in OpenSSL. During verification, we expose a bug and a few anomalies that have been existing for a long time. They have been reported to and confirmed by the OpenSSL community. Our results establish the functional correctness of these C implementations for the first time.

Application Programming Interfaces (APIs) usually have usage constraints, such as call conditions or call orders. Incorrect usage of these constraints, called API misuse, will result in system crashes, bugs, and even security problems. It is crucial to detect such misuses early in the development process. Though many approaches have been proposed over the last years, recent studies show that API misuses are still prevalent, especially the ones specific to individual projects. In this paper, we strive to improve current API-misuse detection capability for large-scale C programs. First, We propose IMSpec, a lightweight domain-specific language enabling developers to specify API usage constraints in three different aspects (i.e., parameter validation, error handling, and causal calling), which are the majority of API-misuse bugs. Then, we have tailored a constraint guided static analysis engine to automatically parse IMSpec rules and detect API-misuse bugs with rich semantics. We evaluate our approach on widely used benchmarks and real-world projects. The results show that our easily extensible approach performs better than state-of-the-art tools. We also discover 19 previously unknown bugs in real-world open-source projects, all of which have been confirmed by the corresponding developers.