VS3: SMT Solvers for Program Verification

Complete decision procedure for the theory of bounded pointer arithmetic based on quantifier instantiation and SMT

Proceedings of the Institute for System Programming of RAS ◽

10.15514/ispras-2021-33(4)-13 ◽

2021 ◽

Vol 33 (4) ◽

pp. 177-194

Author(s):

Rafael Faritovich Sadykov ◽

Mikhail Usamovich Mandrykin

Keyword(s):

Program Verification ◽

Source Code ◽

Decision Procedures ◽

C Programs ◽

Smt Solver ◽

Smt Solvers ◽

Relevant Logics ◽

Soundness And Completeness ◽

C Program ◽

Quantifier Instantiation

The process of developing C programs is quite often prone to errors related to the uses of pointer arithmetic and operations on memory addresses. This promotes a need in developing various tools for automated program verification. One of the techniques frequently employed by those tools is invocation of appropriate decision procedures implemented within existing SMT-solvers. But at the same time both the SMT standard and most existing SMT-solvers lack the relevant logics (combinations of logical theories) for directly and precisely modelling the semantics of pointer operations in C. One of the possible ways to support these logics is to implement them in an SMT solver, but this approach can be time-consuming (as requires modifying the solver’s source code), inflexible (introducing any changes to the theory’s signature or semantics can be unreasonably hard) and limited (every solver has to be supported separately). Another way is to design and implement custom quantifier instantiation strategies. These strategies can be then used to translate formulas in the desired theory combinations to formulas in well-supported decidable logics such as QF_UFLIA. In this paper, we present an instantiation procedure for translating formulas in the theory of bounded pointer arithmetic into the QF_UFLIA logic. We formally proved soundness and completeness of our instantiation procedure in Isabelle/HOL. The paper presents an informal description of this proof of the proposed procedure. The theory of bounded pointer arithmetic itself was formulated based on known errors regarding the correct use of pointer arithmetic operations in industrial code as well as the semantics of these operations specified in the C standard. Similar procedure can also be defined for a practically relevant fragment of the theory of bit vectors (monotone propositional combinations of equalities between bitwise expressions). Our approach is sufficient to obtain efficient decision procedures implemented as Isabelle/HOL proof methods for several decidable logical theories used in C program verification by relying on the existing capabilities of well-known SMT solvers, such as Z3 and proof reconstruction capabilities of the Isabelle/HOL proof assistant.

Download Full-text

Formal Replay of Translation Validation for Highly Optimised C

10.29007/dw2m ◽

2018 ◽

Author(s):

Thomas Sewell

Keyword(s):

Gold Standard ◽

Program Verification ◽

Theorem Prover ◽

Worked Example ◽

Translation Validation ◽

Smt Solvers ◽

Ongoing Effort ◽

Formal Rule ◽

Standard Level ◽

Rule Set

In previous work [Sewell, Myreen and Klein, 2013] we have implemented atranslation validation mechanism for checking that a C compiler is adheringto the expected semantics of a verified program. We used this apparatus tocheck the compilation of the seL4 verified operating systemkernel [Klein et.al. 2009] by GCC 4.5.1. To get this result, wecarefully chose a problem representation that worked well with certain highlyoptimised SMT solvers. This raises a question of correctness. While we areconfident the result is correct, we still aim to replay this result with themost dependable tools available.In this work we present a formalisation of the proof rules needed to replaythe translation check within the theorem prover Isabelle/HOL. This is part ofan ongoing effort to bring the entire translation validation result within asingle trusted proof engine and derive a single correctness theorem, thusreaching the gold standard level of trustworthiness for program verification.We had hoped to present the formal rule set in action through a worked example.Unfortunately while we have all the theory we need, the mechanisms forselecting and applying the rules and discharging certain side conditions remaina work in progress, and our example proof is incomplete.

Download Full-text