This paper 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.

FreeRTOS is a real-time operating system with configurable scheduling policies. Its portability and configurability make FreeRTOS one of the most popular real-time operating systems for embedded devices. We formally analyze the FreeRTOS scheduler on ARM Cortex-M4 processor in this work. Specifically, we build a formal model for the FreeRTOS ARM Cortex-M4 port and apply model checking to find errors in our models for FreeRTOS example applications. Intriguingly, several errors are found in our application models under different scheduling policies. In order to confirm our findings, we modify application programs distributed by FreeRTOS and reproduce assertion failures on the STM32F429I-DISC1 board.

C OQ C RYPTO L INE is an automatic certified verification tool for cryptographic programs. It is built on OC AML programs extracted from algorithms fully certified in C OQ with SS-R EFLECT . Similar to other automatic tools, C OQ C RYPTO - L INE calls external decision procedures during verification. To ensure correctness, all answers from external decision procedures are validated by certified certificate checkers in C OQ C RYPTO L INE . We evaluate C OQ C RYPTO L INE on cryptographic programs from B ITCOIN , BORING SSL, NSS , and O PEN SSL. The first certified verification of the reference implementation for number theoretic transform in the post-quantum key exchange mechanism K YBER is also reported.

Pufferfish is a Bayesian privacy framework for designing and analyzing privacy mechanisms. It refines differential privacy, the current gold standard in data privacy, by allowing explicit prior knowledge in privacy analysis. In practice, privacy mechanisms often need be modified or adjusted to specific applications. Their privacy risks have to be re-evaluated for different circumstances. Privacy proofs can thus be complicated and prone to errors. Such tedious tasks are burdensome to average data curators. In this paper, we propose an automatic verification technique for Pufferfish privacy. We use hidden Markov models to specify and analyze discrete mechanisms in Pufferfish privacy. We show that the Pufferfish verification problem in hidden Markov models is NP-hard. Using Satisfiability Modulo Theories solvers, we propose an algorithm to verify privacy requirements. We implement our algorithm in a prototypical tool called FAIER, and analyze several classic privacy mechanisms in Pufferfish privacy. Surprisingly, our analysis show that naïve discretization of well-established privacy mechanisms often fails, witnessed by counterexamples generated by FAIER. In discrete Above Threshold, we show that it results in absolutely no privacy. Finally, we compare our approach with state-of-the-art tools for differential privacy, and show that our verification technique can be efficiently combined with these tools for the purpose of certifying counterexamples and finding a more precise lower bound for the privacy budget ϵ .

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.

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.

This paper 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 edges of GSTE graphs. Based on these formalization, parameterized GSTE are verified. We moreover formalize our techniques in Isabelle. 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.

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. 2012 ACM Subject Classification Software and its engineering → Formal software verification

We adapt an existing preemptive scheduling model of RTOS kernel by eChronos from machine-assisted proof to Spin-based model checker. The model we constructed can be automatically verified rather than formulating proofs by hand. Moreover, we look into the designs of a Linux-like real-time kernel--Piko/RT and the specification of ARMv7-M architecture to reconstruct the model, and use LTL to specify a simple concurrent programs--consumer/producer problem during the development stage of the kernel. We show that under the preemptive scheduling and the mechanism of ARMv7-M, the program will not suffer from race condition, starvation, and deadlock.

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.

Spark is a new promising platform for scalable data-parallel computation. It provides several high-level application programming interfaces (APIs) to perform parallel data aggregation. Since execution of parallel aggregation in Spark is inherently non-deterministic, a natural requirement for Spark programs is to give the same result for any execution on the same data set. We present PureSpark, an executable formal Haskell specification for Spark aggregate combinators. Our specification allows us to deduce the precise condition for deterministic outcomes from Spark aggregation. We report case studies analyzing deterministic outcomes and correctness of Spark programs.

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.

Due to enormous resource consumption, model checking each revision of evolving systems repeatedly is impractical. To reduce cost in checking every revision, contextual assumptions are reused from assume-guarantee reasoning. However, contextual assumptions are not always reusable. We propose a fine-grained learning technique to maximize the reuse of contextual assumptions. Based on fine-grained learning, we develop a regressional assume-guarantee verification approach for evolving systems. We have implemented a prototype of our approach and conducted extensive experiments (with 1018 verification tasks). The results suggest promising outlooks for our incremental technique.

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.

In the Map-Reduce programming model for data parallel computation, a reducer computes an output from a list of input values associated with a key. The inputs however may not arrive at a reducer in a fixed order due to non-determinism in transmitting key-value pairs over the network. This gives rise to the reducer commutativity problem, that is, is the reducer computation independent of the order of its inputs? In this paper, we study the reducer commutativity problem formally. We introduce a syntactic subset of integer programs termed integer reducers to model real-world reducers. In spite of syntactic restrictions, we show that checking commutativity of integer reducers over unbounded lists of exact integers is undecidable. It remains undecidable even with input lists of a fixed length. The problem however becomes decidable for reducers over unbounded input lists of bounded integers. We propose an efficient reduction of commutativity checking to conventional assertion checking and report experimental results using various off-the-shelf program analyzers.

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.

Recursion can complicate program analysis significantly. Some program analyzers simply ignore recursion or even refuse to check recursive programs. In this paper, we propose an algorithm that uses a recursion-free program analyzer as a black box to check recursive programs. With extended program constructs for assumptions, assertions, and nondeterministic values, our algorithm computes function summaries from inductive invariants computed by the underlying program analyzer. Such function summaries enable our algorithm to check recursive programs. We implement a prototype using the recursion-free program analyzer CPAChecker and compare it with other program analyzers on the benchmarks in the 2014 Competition on Software Verification.