Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof to EasyCrypt. Our motivating use-case is the X-Wing hybrid KEM, for which we present the first formally verified implementation.

This article proposes a term-level generalized symbolic trajectory evaluation (GSTE) to tackle parameterized hardware verification. We develop a theorem-proving technique for parameterized GSTE verification. In our technique, a constraint is associated with a node in GSTE graphs to specify reachable states. Generalized inductive relations between nodes of GSTE graphs are formulated; instantaneous implications are formalized on the edges of GSTE graphs. Based on this formalization, parameterized GSTE are verified. We moreover formalize our techniques in Isabelle. Furthermore, once a parametrized design is verified at the term level, we can convert the generally parameterized invariants into concrete ones, which can be used to verify a synthesized netlist of an instance of the parameterized design at the Boolean level. We demonstrate the effectiveness of our techniques in case studies. Interestingly, subtleties between different implementations of FIFOs are discovered by our parameterized verification, although these circuits have been extensively studied previously.

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.

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.

Loop invariant generation has long been a challenging problem. Black-box learning has recently emerged as a promising method for inferring loop invariants. However, the performance depends heavily on the quality of collected examples. In many cases, only after tens or even hundreds of constraint queries, can a feasible invariant be successfully inferred.

Software products are evolving during their life cycles. Ideally, every revision need be formally verified to ensure software quality. Yet repeated formal verification requires significant computing resources. Verifying each and every revision can be very challenging. It is desirable to ameliorate regression verification for practical purposes. In this paper, we regard predicate analysis as a process of assertion annotation. Assertion annotations can be used as a certificate for the verification results. It is thus a waste of resources to throw them away after each verification. We propose to reuse the previously-yielded assertion annotation in regression verification. A light-weight impact-analysis technique is proposed to analyze the reusability of assertions. A novel assertion strengthening technique is furthermore developed to improve reusability of annotation. With these techniques, we present an incremental predicate analysis technique for regression verification. Correctness of our incremental technique is formally proved. We performed comprehensive experiments on revisions of Linux kernel device drivers. Our technique outperforms the state-of-the-art program verification tool CPAchecker by getting 2.8x speedup in total time and solving additional 393 tasks.

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.

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.

Arithmetic over large finite fields is indispensable in modern cryptography. For efficienty, these operations are often implemented in manually optimized assembly programs. Since these arithmetic assembly programs necessarily perform lots of non-linear computation, checking their correctness is a challenging verification problem. We develop techniques to verify such programs automatically in this paper. Using our techniques, we have successfully verified a number of assembly programs in OpenSSL. Moreover, our tool verifies the boringSSL Montgomery Ladderstep (about 1400 assembly instructions) in 1 hour. This is by far the fastest verification technique for such programs.

Mathematical constructs are necessary for computation on the underlying algebraic structures of cryptosystems. They are often written in assembly language and optimized manually for efficiency. We develop a certified technique to verify low-level mathematical constructs in X25519, the default elliptic curve Diffie-Hellman key exchange protocol used in OpenSSH. Our technique translates an algebraic specification of mathematical constructs into an algebraic problem. The algebraic problem in turn is solved by the computer algebra system Singular. The proof assistant Coq certifies the translation and solution to algebraic problems. Specifications about output ranges and potential program overflows are translated to SMT problems and verified by SMT solvers. We report our case studies on verifying arithmetic computation over a large finite field and the Montgomery Ladderstep, a crucial loop in X25519.

The Vienna Development Method (VDM) is a formal method that supports modeling and analysis of software systems at various levels of abstractions. For a model specified by the VDM specification language (VDM-SL), the correctness of the model relies on discharging the proof obligations (POs), especially in the case of implicit specifications. In this paper, we propose an approach that encodes and discharges POs of VDM-SL models using SMT solvers. More specifically, POs generated by the Overture tool are encoded and discharged in the Z3 SMT solver. Our case studies showed that the approach can discharge significant part of proof obligations of a VDM-SL model efficiently.

We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning an approximate regular model of the set of feasible paths in a program, and testing whether this model contains an incorrect behavior. Exact learning algorithms require checking equivalence between the model and the program, which is a difficult problem, in general undecidable. Our learning procedure is therefore based on the framework of probably approximately correct (PAC) learning, which uses sampling instead, and provides correctness guarantees expressed using the terms error probability and confidence. Besides the verification result, our procedure also outputs the model with the said correctness guarantees. Obtained preliminary experiments show encouraging results, in some cases even outperforming mature software verifiers.

We present a code- and input-sensitive sanitization synthesis approach for repairing string vulnerabilities that are common in web applications. The synthesized sanitization patch modifies the user input in an optimal way while guaranteeing that the repaired web application is not vulnerable. Given a web application, an input pattern and an attack pattern, we use automata-based static string analysis techniques to compute a sanitization signature that characterizes safe input values that obey the given input pattern and are safe with respect to the given attack pattern. Using the sanitization signature, we synthesize an optimal sanitization patch that converts malicious user inputs to benign ones with minimal editing. When the generated patch is added to the web application, it is guaranteed that the repaired web application is no longer vulnerable. We present refinements to previous sanitization synthesis algorithms that reduce the runtime sanitization cost significantly. We evaluate our approach on open source web applications using common input and attack patterns, demonstrating the effectiveness of our approach.

Probabilistic models are widely deployed in various systems. To ensure their correctness, verification techniques have been developed to analyze probabilistic systems. We propose the first sound and complete learning-based compositional verification technique for probabilistic safety properties on concurrent systems where each component is an Markov decision process. Different from previous works, weighted assumptions are introduced to attain completeness of our framework. Since weighted assumptions can be implicitly represented by multiterminal binary decision diagrams (MTBDDs), we give an >i /i<*-based learning algorithm for MTBDDs to infer weighted assumptions. Experimental results suggest promising outlooks for our compositional technique.

We propose the first sound and complete learning-based compositional verification technique for probabilistic safety properties on concurrent systems where each component is an Markov decision process. Different from previous works, weighted assumptions are introduced to attain completeness of our framework. Since weighted assumptions can be implicitly represented by multi-terminal binary decision diagrams (MTBDD's), we give an L*-based learning algorithm for MTBDD's to infer weighted assumptions. Experimental results suggest promising outlooks for our compositional technique.

By combining algorithmic learning, decision procedures, predicate abstraction and simple templates for quantified formulae, we present an automated technique for finding loop invariants. Theoretically, this technique can find arbitrary first-order invariants (modulo a fixed set of atomic propositions and an underlying satisfiability modulo theories solver) in the form of the given template and exploit the flexibility in invariants by a simple randomized mechanism. In our study, the proposed technique was able to find quantified invariants for loops from the Linux source and other realistic programs. Our contribution is a simpler technique than the previous works yet with a reasonable derivation power.

We describe a learning-based approach for verifying recursive functions. The Boolean formula learning algorithm CDNF is used to automatically infer function summaries for recursive functions. In contrast to traditional iterative fix point computation-based approaches, ours can quickly guess summaries and verify purported summaries. When purported summaries are incorrect, the learning algorithm refines them by posing queries. We solve examples that are unattainable by a mature model checker for recursive programs.

This paper presents results on formal verification of high-speed cryptographic software. We consider speed-record-setting hand-optimized assembly software for Curve25519 elliptic-curve key exchange presented by Bernstein et al. at CHES 2011. Two versions for different microarchitectures are available. We successfully verify the core part of the computation, and reproduce detection of a bug in a previously published edition. An SMT solver supporting array and bit-vector theories is used to establish almost all properties. Remaining properties are verified in a proof assistant with simple rewrite tactics. We also exploit the compositionality of Hoare logic to address the scalability issue. Essential differences between both versions of the software are discussed from a formal-verification perspective.

Both symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the other hand, infers contextual assumptions by inspecting spurious erroneous traces. One would expect that their integration could further improve the capacity of model checking. Yet examining numerous erroneous traces to deduce contextual assumptions can be very time-consuming. The integration of symbolic model checking and assume-guarantee reasoning is thus far from clear. In this paper, we present a progressive witness analysis algorithm for automated assume-guarantee reasoning to exploit a multitude of traces from BDD-based symbolic model checkers. Our technique successfully integrates symbolic model checking with automated assume-guarantee reasoning by directly inferring BDD's as implicit assumptions. It outperforms monolithic symbolic model checking in four benchmark problems and an industrial case study in experiments.

Dynamic data-structures with pointer links, which are heavily used in real-world software, cause extremely difficult verification problems. Currently, there is no practical framework for the efficient verification of such software systems. We investigated symmetry reduction techniques for the verification of software systems with C-like indirect reference chains like x/spl rarr/y/spl rarr/z/spl rarr/w. We formally defined the model of software with pointer data structures and developed symbolic algorithms to manipulate conditions and assignments with indirect reference chains using BDD technology. We relied on two techniques, inactive variable elimination and process-symmetry reduction in the data-structure configuration, to reduce time and memory complexity. We used binary permutation for efficiency, but we also identified the possibility of an anomaly of false image reachability. We implemented the techniques in tool Red 5.0 and compared performance with Mur/spl phi/ and SMC against several benchmarks.

Model checking is a practical tool for automated debugging of embedded software. In model checking, a high-level description of a system is compared against a logical correctness requirement to discover inconsistencies. Since model checking is based on exhaustive state-space exploration and the size of the state space of a design grows exponentially with the size of the description, scalability remains a challenge. We have thus developed techniques for exploiting modular design structure during model checking, and the model checker jMocha (Java MOdel-CHecking Algorithm) is based on this theme. Instead of manipulating unstructured state-transition graphs, it supports the hierarchical modeling framework of reactive modules. jMocha is a growing interactive software environment for specification, simulation and verification, and is intended as a vehicle for the development of new verification algorithms and approaches. It is written in Java and uses native C-code BDD libraries from VIS. jMocha offers: (1) a GUI that looks familiar to Windows/Java users; (2) a simulator that displays traces in a message sequence chart fashion; (3) requirements verification both by symbolic and enumerative model checking; (4) implementation verification by checking trace containment; (5) a proof manager that aids compositional and assume-guarantee reasoning; and (6) SLANG (Scripting LANGuage) for the rapid and structured development of new verification algorithms. jMocha is available publicly at; it is a successor and extension of the original Mocha tool that was entirely written in C.