IA169 System Verification and Assurance CEGAR and Abstract Interpretation Jiří Barnat Program Analysis Goals of Program Analysis Deduce program properties from the program source code and ... ... employ them for program optimisation. ... employ them for program verification. Undecidability Validity of all interesting program properties written in general programming language is algorithmically undecidable. Henry Gordon Rice (1953) – Rice’s Theorems. Alan Turing (1936) – Halting Problem. IA169 System Verification and Assurance – 11 str. 2/27 Undecidable – So what now? Abstraction To hide details in order to simplify the analysis. Aims at correct, even if incomplete solution. Using Abstraction To build (typically finite state) model of system under verification. (Followed, e.g., by model checking approach to verification.) System execution within the context of abstraction – Abstract Interpretation. Recall Other Approaches Fixed input set of values (Testing). Limited exploration of the full state space (Bounded MC). Practical undecidability (Symbolic Execution). IA169 System Verification and Assurance – 11 str. 3/27 Section Data and Predicate Abstraction IA169 System Verification and Assurance – 11 str. 4/27 Data Abstraction Motivation State space explosion due to large data domains. Reduction employing principle of domain testing, i.e. replacing original data domain with a data domain with less number of members. Terminology Abstraction: mapping concrete states to abstract ones. Concretisation: mapping abstract states to set of concrete states. Example of Data Abstraction Int -> { Even, Odd } Concrete state: PC:12, A:15, B:0 Abstract state: PC:12, A:Odd, B:Even IA169 System Verification and Assurance – 11 str. 5/27 Abstract Transition System Transitions in Concrete and Abstract Semantics Statement in program code, line 12: A := A+A In concrete semantics: PC:12, A:15, B:0 −→ PC:13, A:30, B:0 in abstract semantics: PC:12, A:Odd, B:Even −→ PC:13, A:Even, B:Even Non-Determinism in Abstract Transition System Abstract state: PC:13, A:Even, B:Even Statement in program code, line 13: A := A div 2 PC:13, A:Even, B:Even −→ PC:14, A:Even, B:Even PC:14, A:Odd, B:Even IA169 System Verification and Assurance – 11 str. 6/27 Relation of Abstract and Concrete Transition Systems Over-Approximation Every run of concrete system is present in concretisation of some abstract run (run of abstracted transition system). There may exist runs that are present in concretisation of some abstract run, but are not allowed in concrete transition system. Under-Approximation Every run present in concretisation of any abstract run is an existing run of concrete transition system. There may exist runs of concrete transition systems that are not present in concretisation of any abstract run. IA169 System Verification and Assurance – 11 str. 7/27 Verification of Approximated Transition Systems Notation ATS – Abstract Transition System CTS – Concrete Transition System Verification of Over-Approximated Systems Absence of error in ATS proves absence of error in CTS. Error in ATS may, but need not indicate error in CTS. Error in ATS that is not an error in CTS, is referred to as false positive (spurious error, false alarm). Verification of Under-Approximated Systems Error in ATS proves presence of error in CTS. Absence of error in ATS does not prove absence of error in CTS. Error in CTS that is not present in ATS is referred to as false negative. IA169 System Verification and Assurance – 11 str. 8/27 Example – Concrete Semantics Task Is error state reachable in the following program? % denotes modulo operation, A in an integral variable Source-code Value ofA in concrete semantics after execution of program statement 1 read(A); 2 A = A % 2; 3 A = A + 1; 4 if (A==0) 5 error; 6 else 7 return; [int] [0] [1] [1] [2] IA169 System Verification and Assurance – 11 str. 9/27 Example – Data Abstraction Task Is error state reachable in the following program? A is abstracted into parity domain {even,odd}. Source-code Value of A in abstract semantics after execution of program statement 1 read(A); 2 A = A % 2; 3 A = A + 1; 4 if (A==0) 5 error; 6 else 7 return; [even] [odd] [even] [odd] [odd] [even] IA169 System Verification and Assurance – 11 str. 10/27 Predicate Abstraction Predicate Abstraction Predicates – Boolean expressions about variable values. Example of definition of abstract transition system: Program Counter, Validity of selected predicates Amount of Abstraction Amount of predicates influences the precision of abstraction. Less predicates big ambiguity, smaller state space. More predicates increased precision, bigger state space. IA169 System Verification and Assurance – 11 str. 11/27 Task Task For the given program code and set of predicates, draw the abstract transition system formed using predicate abstraction. Check if there is path in your ATS that is not a spurious run and leads to an error state. 1 read(A); 2 A = A % 2; 3 A = A + 1; 4 if (A==0) 5 error; 6 else 7 return; a) P1 ≡ A = 0 b) P1 ≡ A = 0, P2 ≡ A ≥ 0 IA169 System Verification and Assurance – 11 str. 12/27 Remarks on Predicate Abstraction Analysis of Abstract Runs Leading to Error Decision about validity of the run (Is it a false alarm?) Deduction of new predicates to make abstraction more precise. Size of Abstract Transition System The size of the state space grows exponentially with the number of predicates. Possible Solution Predicates are bound to particular program locations. IA169 System Verification and Assurance – 11 str. 13/27 Section CEGAR Approach IA169 System Verification and Assurance – 11 str. 14/27 Counter-Example Guided Abstraction Refinement Principle of CEGAR Approach Given an initial set of predicates, system is abstracted with predicate abstraction. Abstract transition system (over-approximation) is verified with a model checking procedure. In the case a reported counterexample is find spurious, it is analysed in order to deduce new predicates and refine predicate abstraction. Procedure repeats until real counterexample is find or system is successfully verified. Notes Deducing new predicates is very difficult. Often done within model checking procedure (on-the-fly). Berkeley Lazy Abstraction Software Verification Tool (BLAST). IA169 System Verification and Assurance – 11 str. 15/27 Schema of CEGAR Approach Abstract Is c−example spurious? Abstract Model Refined Model Counter Example Is property satisfied? System is valid No System is invalidRefine Model Yes System Property Yes No IA169 System Verification and Assurance – 11 str. 16/27 Section Basics of Abstract Interpretation and Static Analysis of Programs IA169 System Verification and Assurance – 11 str. 17/27 Program Analysis by Abstract Interpretation Program Representation – Flow Graph "Special version" of Control-Flow Graph. Every edge is either guarded with a single guard or defines a single assignment. Goal Compute properties of individual vertices of the flow-graph. Goal Examples Deduce range of values a particular variable may take in a given program location. Compute a set of live variables in a given program location. . . . IA169 System Verification and Assurance – 11 str. 18/27 A General View on Abstract Interpretation Property Decomposition The property to be verified by general program analysis procedure can be decomposed into local data values assigned to individual vertices of the (control-)flow graph. The result of verification is compound or deduced from the values local to the flow-graph vertices. Value Improvement It is defined how an edge of the (control-)flow graph improves (locally updates) the decomposed value of the property to be verified. Application of local update functions gradually (monotonously) improve (approximate) the overall solution. IA169 System Verification and Assurance – 11 str. 19/27 General Algorithm for Computing Abstract Interpretation Initialisation Initially, a suitable value is assigned to every vertex. Every edge of the graph is marked as unprocessed. Computation Pick an unprocessed edge of the graph and perform the local update relevant to the edge and associated vertices. If the update improved the solution, mark the edge as unprocessed again. Repeat until there are unprocessed edges, i.e. until overall fix-point is reached. IA169 System Verification and Assurance – 11 str. 20/27 Example – Computing Live Variables Setup Initial value associated with graph vertices is ∅. Every edge from vertex u to vertex v updates value associated with the vertex u as follows: V (u) = V (u) ∪ V (v) \ assigned(u, v) ∪ used(u, v) , where V (x) denotes value associated with vertex x, assigned(u, v) and used(u, v) denote variables redefined and used along the edge (u, v), respectively. Observation In every moment of computation there is some (approximating) solution to the verified property. Reaching a fix-point indicate, no more information can be deduced by program analysis in the current setup. IA169 System Verification and Assurance – 11 str. 21/27 Abstract Interpretation Observation The procedure presented on previous slides is quite general. Choosing proper setup may result in verification (computation) of many interesting program properties. Often this is combined with some data abstraction for variables. May be performed on partially unwinded graphs. Generally referred to as to abstract interpretation. Parameters What abstract domain is used. Direction of update function (forward, backward, both). What does update function do. How are the values merged over multiple incoming edges. Order of processing of unprocessed edges. Termination detection. IA169 System Verification and Assurance – 11 str. 22/27 Relevant Questions of Abstract Interpretation Is there a fix-point? Often the composition of domains of values associated to vertices forms a complete lattice. Knaster-Tarski theorem says that every monotonous function over such a domain has a fix point. Does computation terminates? If there is no infinitely ascending sequence of possible solutions in the composition of local domains, then yes. Otherwise, need not terminate. IA169 System Verification and Assurance – 11 str. 23/27 Abstract Interpretation and Widening Widening Auxiliary transformation of intermediate results such that it preserves correctness, and at the same times prevents existence of long (possibly infinite) ascending sequence of values in the corresponding domain. Example of widening Let be given boundaries of precision in which we want to know the range of possible values of some variable. Beyond the precision boundaries values will be extended to infinity, i.e. +∞ or −∞. Sequence [0,1] ⊂ [0,2] ⊂ [0,3] ⊂ [0,4] ⊂ [0,5] ⊂ [0,6] ... will for precision bound [0,3] turn into: [0,1] ⊂ [0,2] ⊂ [0,3] ⊂ [0,+∞] IA169 System Verification and Assurance – 11 str. 24/27 Abstract Interpretation and Narrowing Narrowing Using widening may lead to very imprecise results. Widening can be used to accelerate analysis of cycles. After widening-based analysis of cycle, the values are made more precised with narrowing (similar but dual technique). Example Interval [0,+∞] will after narrowing shrink to [0,n]. Commentary Precise usage of widening and narrowing is beyond the scope of this lecture. IA169 System Verification and Assurance – 11 str. 25/27 Other Notes Related to Abstract Interpretation Other Corners of Program Analysis Inter-procedural analysis. Analysis of parallel programs. Generation of invariants. Pointer analysis and analysis of dynamic memory structures. ... CPA checker The Configurable Software-Verification Platform http://cpachecker.sosy-lab.org/ Very successful competitor in Software Verification Competition. IA169 System Verification and Assurance – 11 str. 26/27 Homework Wanna Chalenge? Get acquainted with CPAchecker (https: //github.com/dbeyer/cpachecker/blob/trunk/README.txt) Comment counterexample report (http://cpachecker. sosy-lab.org/counterexample-report/ErrorPath.0.html) Homework Install and try BLAST verification tool. IA169 System Verification and Assurance – 11 str. 27/27