IA169 System Verification and Assurance Bounded Model Checking Jiří Barnat Reminder – SAT and SMT Satisfiability – SAT Finding a valuation of Boolean variables that makes a given formula of propositional logic true. Satisfiability Modulo Theory – SMT Deciding satisfiability of a first-order formula with equality, predicates and function symbols that encode one or more theories. Typical SMT Theories Unbounded integer and real arithmetic. Bounded integer arithmetic (bit-vectors). Theory of data structures (lists, arrays, . . . ). IA169 System Verification and Assurance – 09 str. 2/31 Reminder – SAT and SMT Solvers ZZZ aka Z3 Tool developed by Microsoft Research. WWW interface — http://www.rise4fun.com/Z3 Binary API for use in other tools and applications. SMT-LIB Standardised language for SMT queries. Freely available library with a SMT implementation. IA169 System Verification and Assurance – 09 str. 3/31 Reminder – Satisfiability and Validity Observation Formula is valid if and only if its negation is not satisfiable. Consequence SAT and SMT solvers can be used as tools for proving validity of formulated statements. Model Synthesis SAT solvers not only decide satisfiability of formulas, but for satisfiable formulas also give the valuation which makes the formula true. Unlike theorem provers, they give a "counterexample" in case the statement to be proven is false. IA169 System Verification and Assurance – 09 str. 4/31 Section Checking Safety Properties via SAT Reduction IA169 System Verification and Assurance – 09 str. 5/31 Bounded Model Checking (BMC) Hypothesis If the system contains an error, it can be reproduced with only a small number of controlled steps. Method Idea If we use model checking for error detection, it is sensible to check whether an error (a violation of specification) appears within first k steps of execution. Literature Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu: Symbolic Model Checking without BDDs. TACAS 1999: 193-207, LNCS 1579. Henry A. Kautz, Bart Selman: Planning as Satisfiability.Proceedings of the 10th European conference on Artificial intelligence (ECAI’92): 359-363, 1992, Kluwer. IA169 System Verification and Assurance – 09 str. 6/31 Reduction of BMC to SAT Prerequisites The set of prefixes of length k of all runs of a Kripke structure M can be encoded by a Boolean formula [M]k . Violation of a safety property which can be observed within k steps of the system can be encoded as [¬ϕ]k . Reduction to SAT We check the satisfiability of [M]k ∧ [¬ϕ]k . Satisfiability indicates the existence of a counterexample of length k. Unsatisfiability shows non-existence of a counterexample of length k. IA169 System Verification and Assurance – 09 str. 7/31 Kripkeho structure as a Boolean formula Prerequisites Let M = (S, T, I) be a Kripke structure with initial state s0 ∈ S. Arbitrary state s ∈ S can be represented by a bit vector of size n, that is state s = a0, a1, . . . , an−1 . Encoding M with Boolean Formulae Init(s) – formula which is satisfiable for the valuation of variables a1, a2, ..., an that describe the state s0. Trans(s, s ) – a formula which is satisfiable for a pair of state vectors s, s , iff the valuations a1, a2, ..., an, a1, a2, ..., an describe states between which a transition (s, s ) ∈ T exists. IA169 System Verification and Assurance – 09 str. 8/31 Encoding Finite Runs of M Description of System Runs of Length k Run of length k consists of k + 1 states s0, s1, . . . , sk. The set of all runs of size k of the structure M is designated [M]k and described by the following formula: [M]k ≡ Init(s0) ∧ k i=1 Trans(si−1, si ) Example[M]3 ∧ [¬ϕ]3 Init(s0)∧Trans(s0, s1)∧Trans(s1, s2)∧Trans(s2, s3)∧¬ϕ(s3) IA169 System Verification and Assurance – 09 str. 9/31 Section Completeness of BMC IA169 System Verification and Assurance – 09 str. 10/31 Completeness of BMC for Detecting Safety Violations Problem – Undetected Violation of a Safety Property The violation is not reachable using a path of length k. Paths shorter than k are not encoded in [M]k . Upper Bound on k If k ≥ d where d is the graph diameter, all possible error locations are covered. The diameter of the graph is bounded by 2n , where n is the number of bits of the state vector. Solution Executing BMC iteratively for each k ∈ [0, d]. IA169 System Verification and Assurance – 09 str. 11/31 Automated Detection of Graph Diameter Facts Asking the user is unrealistic. Safe upper bounds are extremely overstated. We would like the verification procedure itself to detect whether k should be increased further. Skeleton of an Algorithm for Complete BMC k = 0 while (true) do if (counterexample of length k exists) then return "Invalid" if (all states are reachable within k steps) then return "Valid" k = k + 1 od IA169 System Verification and Assurance – 09 str. 12/31 Notation I Prerequisites Kripke structure M = (S, T, I). States are described by bit vectors of fixed length. Trans is a SAT representation of a binary relation T. Path of Length n path(s[0..n]) ≡ 0≤i 0. Reformulating the Counterexample Test The original test for counterexample existence for a given k SAT Init(s0) ∧ path(s[0..k]) ∧ ¬ϕ(sk) needs to be changed so that we do not miss counterexamples shorter than the initial value of k. New test for the existence of a counterexample: SAT Init(s0) ∧ path(s[0..k]) ∧ ¬all.ϕ(s[0..k]) IA169 System Verification and Assurance – 09 str. 18/31 k-induction in BMC Observation The tests can be re-formulated so that they resemble the structure of mathematical induction. TAUT is a tautology test (unsatisfiability of negation). Base Case Test for counterexample existence. SAT ¬ Init(so) ∧ path(s[0..i]) =⇒ all.ϕ(s[0..i]) Inductive Step Test for completeness. TAUT ¬Init(s0) ⇐= all.¬Init(s[1..(i+1)]) ∧ loopFree(s[0..i+1]) ∨ TAUT loopFree(s[0..i+1]) ∧ all.ϕ(s[0..i]) =⇒ ϕ(si+1) IA169 System Verification and Assurance – 09 str. 19/31 Acyclic vs Shortest Paths in BMC Observation Graph diameter (d) is the length of the longest of the shortest paths between each pair of vertices in the graph. An acyclic path can be substantially longer than the graph diameter. BMC with Shortest Paths BMC is correct if loopFree is replaced with shortest. The shortest predicate, however, needs quantifiers and is as such not a purely SAT application. For more details, see ... Mary Sheeran, Satnam Singh, and Gunnar Stålmarck: Checking Safety Properties Using Induction and a SAT-Solver, FMCAD 2000, 108-125, LNCS 1954, Springer. IA169 System Verification and Assurance – 09 str. 20/31 Section LTL and BMC IA169 System Verification and Assurance – 09 str. 21/31 LTL Verification with BMC Observation 1 LTL is only well-defined for infinite runs. For evaluating LTL on finite paths, we use three-value logic (true, false, cannot say). Validity of some LTL formulas cannot be decided on any finite path (eg. GF a). Observation 2 Cycles that consist of only a few states are unrolled by BMC to acyclic paths of length k. We allow encoding lasso-shaped paths. That is, (k, l)-cyclic paths. IA169 System Verification and Assurance – 09 str. 22/31 (k,l)-cyclic paths (k,l)-cyclic runs A run π = s0s1s2 . . . of a Kripke structure M = (S, T, I, s0) is (k, l)-cyclic if π = (s0s1s2 . . . sl−1)(sl . . . sk)ω , where 0 < l ≤ k a sl−1 = sk. Observation If π is (k, l)-cyclic, π is also (k + 1, l + 1)-cyclic. Treating finite paths as (k, k)-cyclic is incorrect (could create a non-existent run in M). Every path of length k is either acyclic or (k, l)-cyclic. IA169 System Verification and Assurance – 09 str. 23/31 Semantics of LTL on Finite Prefixes of Runs Semantics of LTL for Finite Prefixes Let π be a run of a Kripke structure M. k is given. π = π0 πi |=nl X ϕ iff i < k ∧ πi+1 |=nl ϕ πi |=nl ϕ U ψ iff ∃j.i ≤ j ≤ k, πj |=nl ψ and ∀m.i ≤ m < j, πi |=nl ϕ Semantics of |=k for LTL in BMC For (k, l)-cyclic paths, π |=k ϕ ⇐⇒ π |= ϕ holds. For acyclic paths, π |=k ϕ ⇐⇒ π0 |=nl ϕ holds. |=k=⇒|=k+1, |=k approximates |= IA169 System Verification and Assurance – 09 str. 24/31 BMC for LTL Goal We construct a Boolean formula [M, ϕ, k] which is satisfiable iff Kripke structure M has a run π such that π |=k ϕ. [M, ϕ, k] ≡ [M]k ∧ [ϕ, k] Encoding [M]k encodes all paths of length k [ϕ, k] ≡ _[ϕ, k]0 ∨ k l=1 l [ϕ, k]0 _[ϕ, k]0 encodes that the path is acyclic and |=nl ϕ l [ϕ, k]0 encodes that the path is (k, l)-cyclic and |= ϕ IA169 System Verification and Assurance – 09 str. 25/31 LTL tricks in BMC Fragment LTL-X Reduces the number of transitions (smaller SAT instance). Similar to partial order reduction. For the Interested Keijo Heljanko: Bounded Model Checking for Finite-State Systems http://users.ics.aalto.fi/kepa/qmc/slides-heljanko-2.pdf Keijo Heljanko and Tommi Junttila: Advanced Tutorial on Bounded Model Checking http://users.ics.aalto.fi/kepa/acsd06-atpn06-bmc-tutorial/ lecture1.pdf IA169 System Verification and Assurance – 09 str. 26/31 Section Conclusions on BMC IA169 System Verification and Assurance – 09 str. 27/31 Advantages of BMC General Reduces to a standard SAT problem, advances in SAT solving help with BMC. Often finds counterexamples of minimal length (not always). Boolean formulas can be more compact than OBDD representation. Verification of HW Thanks to k-induction, a very successful method. Verification of SW Currently, according to Software Verification Competition (TACAS 2014), BMC in connection with SMT is currently among the best software verification methods (actually falsification). IA169 System Verification and Assurance – 09 str. 28/31 Downsides of BMC General Not complete in general. Large SAT instances are still unsolvable. Verification of SW Encoding an entire CFG as a SAT instance is currently unrealistic. K-induction cannot be used (the graph is incomplete, no back edges). Problems with dynamic data structure analysis. Loop analysis is hard. Inefficient for full arithmetic (partially solved by SMT). IA169 System Verification and Assurance – 09 str. 29/31 Tools and food for thought... Tools CBMC – BMC for ANSI-C. ESBMC – uses SMT, built on top of CBMC. LLBMC – BMC for LLVM bitcode. Food for Thought... What differentiates modern SMT-BMC from symbolic execution? Boundaries are not clear. IA169 System Verification and Assurance – 09 str. 30/31 Practicals and Homework – 09 Practicals Follow LLBMC tutorial (http://llbmc.org/usage.html) Work with and compare LLBMC and ESBMC. Write erroneous program in C such that the error is not discovered with bounded MC approach. Homework Study structure and results of Software Verification Competition (TACAS) IA169 System Verification and Assurance – 09 str. 31/31