Static Analysis and Verification of C Programs

Static Analysis and Veriﬁcation of C Programs Subash Shankar Hunter College (CUNY) September 17, 2015 Acknowledgements: This work was partially funded by a grant from Digiteo, and is based on the Frama-C tool developed at the CEA LIST Institute, Saclay, France. It includes contributions from Zachary Hutchinson (Hunter College) and Gilbert Pajela (CUNY Graduate Center).

What is V & V? Validation: The software specification does what the user wants. Verification: The software does what the specification says it does.

What is V & V? Validation: The software specification does what the user wants. Verification: The software does what the specification says it does. Verification = Testing Testing can be used to show the presence of bugs, but never their absence! (Dijkstra, 1970)

Why bother with V & V? Software failure ⇒ loss of $$$ or human life (for safety-critical systems) A few infamous examples: AT&T long-distance: network communication code bug ⇒ 60000 customers shut down Faulty guidance systems: Mariner spacecraft: punctuation error ⇒ craft exploded (by ground control) Ariane 5 rocket: overflow due to 64-to-16 bit conversion ⇒ craft exploded (self-destruct) Mars Climate Orbiter: Metric-English unit inconsistency (Newtons vs. pounds) ⇒ Lost orbiter Radiation therapy machines: Therac-25: buggy shield/filter code ⇒ 6 documented deaths, hundreds(?) with longer-term effects Multidata Systems Cobalt-60: undocumented data entry leads to improper shielding ⇒ dozens dead Toyota acceleration bug: firmware error ⇒ dead people (and we aren’t even including software susceptible to malicious bugs)

What is Static Analysis? The analysis of software based on information available at compile time, to prove its properties for all possible executions, preferably with [automatic or semi-automatic] tool support.

What is Static Analysis? The analysis of software based on information available at compile time, to prove its properties for all possible executions, preferably with [automatic or semi-automatic] tool support. 3 Common [Veriﬁcation Oriented] Techniques: Abstract Interpretation and Symbolic Evaluation Deductive Veriﬁcation (weakest preconditions) Model Checking

Abstract Interpretation (AI) A technique for approximation of program semantics based on mappings between concrete and abstract lattices (Cousot & Cousot, 1977) α: abstraction fct. γ: concretization fct.

Abstract Interpretation (AI) A technique for approximation of program semantics based on mappings between concrete and abstract lattices (Cousot & Cousot, 1977) α: abstraction fct. γ: concretization fct. Examples: evenx := ¬ evenx ⇑ α x := x+1 if xneg xzero := {T,F} else xzero := F (and similarly for xneg and xpos vars) ⇑ α x := x+1

Abstract Interpretation (AI) A technique for approximation of program semantics based on mappings between concrete and abstract lattices (Cousot & Cousot, 1977) α: abstraction fct. γ: concretization fct. Examples: evenx := ¬ evenx ⇑ α x := x+1 if xneg xzero := {T,F} else xzero := F (and similarly for xneg and xpos vars) ⇑ α x := x+1 Approach: Use theorem prover to identify eﬀect of each program statement in abstract space. Compute over-approximation of variable values at each point of program, based on selected abstraction α Symbolically evaluate concrete program to attain values of all variables at all points.

Applying Abstract Interpretation How do we pick the abstraction function α (and induced concretization γ)? Ex: boolean lattices on neg-zero-pos, intervals, modulus fields Abstract program is non-deterministic and loses information. But this information loss may make semantics decidable (in abstract space). Simple for loop-free code Loops require a fixed point computation that may take too long or not terminate. Approximation: unroll loop a fixed number of times First major application: automatically analyze Ariane 5 rocket software (after crash) ⇒ data conversion error from 64-bit float to 16-bit integer Value analysis embodied in Frama-C tool for verification of C programs.

Deductive Veriﬁcation What does it mean for a program (or statement) to be correct? The program enforces its contract; i.e., if the program is executed in a state where the precondition is true, the postcondition of the contract is true after execution.

Deductive Veriﬁcation What does it mean for a program (or statement) to be correct? The program enforces its contract; i.e., if the program is executed in a state where the precondition is true, the postcondition of the contract is true after execution. Two notions: 1 Partial Correctness: Contract enforcement is conditional on program’s termination. 2 Total Correctness: Contract is enforced unconditionally

Automating Deductive Veriﬁcation Theoretical Basis: Floyd-Hoare Logic (1969), Dijkstra (1975) Notation: The Hoare triple {P}S{Q} means if statement S is executed from a state in which predicate P is true and it terminates, predicate Q must be true on termination. Some valid triples: Assignment – {x > 2} y=x+1 {y > 3} Selection – {true} if x>0 then y=x else y=-x {y ≥ 0} Iteration – Identify loop invariant, and prove invariant preservation axioms: Invariant holds on loop entry The loop body preserves inv The invariant implies postcondition on loop termination No automated way to determine invariant!

Expressing Contracts Annotate programs with specifications written in ANSI/ISO C Specification Language (ACSL). Major features of ACSL: Function and statement contracts for pre/post conditions, with multiple named behaviors: /*@ requires n>0; ensures result == 5; */ Invariant specification: //@ loop invariant n>= 0; Support for both C and math types (e.g., Z and 32-bit ints) and data structures (pointer, array, struct, etc.), with typical C operators Logic (first order, higher-order, inductive) predicates Axiomatic definitions (types, functions, etc.) Ghost (i.e., auxiliary) and volatile variables Predefined functions for various real-world concerns (e.g., return values (result), pre-values (old), pointers and heap variables, separation)

Model Checking M (system being veriﬁed): Q P,Q Q Q Q Q Q P,Q Properties (in temporal logic): Q (’always Q’) ⇒ Yes P (’eventually P’) ⇒ Yes P ⇒ No! (with counterexample)

Model Checker Characteristics Completely automatic ’turnkey’ operation Counterexample (system trace) produced if property is false Scalable technology used widely in industry, especially chip manufacturers Mature (discovered independently by Clarke & Emerson and Queille & Sifakis in early 80s, Turing award 2007) Major problem: State space explosion One solution: Represent state space symbolically (McMillan etal, 1990) ⇒ can handle 10100 states and more in some cases.

Model Checking for Program Veriﬁcation Program Translate Prove: assert(x==y) statement at line 3 of the program is valid i.e., (PC = 3 → (x = y))

Model Checking for Program Veriﬁcation Program Translate Prove: assert(x==y) statement at line 3 of the program is valid i.e., (PC = 3 → (x = y)) But a program with v 32-bit variables and 2k points needs up to 232v+k states

Program Abstraction Partition concrete state space into abstract states γ(S) = {s|S = α(s)} where α(s) is the abstract state corresponding to s (note: α is not one-to-one) Determine transitions: A transition from abstract state a1 to a2 exists iﬀ ∃s1 : α(s1) = a1, ∃s2 : α(s2) = a2, and there is a transition s1 → s2 in the concrete machine. Note: abstract machine is non-deterministic Resulting abstract state machine is a conservative approximation: If property is provable in abstract machine, it must be true in the concrete machine. If property is false in abstract machine, either it is also false in the concrete machine, or the abstraction is not ﬁne enough.

Predicate Abstraction How do we pick the abstraction function α? One solution: ’Guess’ predicates that are likely to be suﬃcient to prove desired property Predicates selected based on property being veriﬁed, major predicates in program (e.g., conditions of loop, selection statements), arithmetic properties (e.g., {pos,zero,neg}, {odd,even}), control locations (e.g., {PC=4,PC=4}), various other heuristics Abstractions may be on control as well as data

Predicate Abstraction How do we pick the abstraction function α? One solution: ’Guess’ predicates that are likely to be suﬃcient to prove desired property Predicates selected based on property being veriﬁed, major predicates in program (e.g., conditions of loop, selection statements), arithmetic properties (e.g., {pos,zero,neg}, {odd,even}), control locations (e.g., {PC=4,PC=4}), various other heuristics Abstractions may be on control as well as data Ex (using an odd-even abstraction on y): y = 0; for (i=0; i<n; i++) y += 2; assert(y%2 == 0); ⇒ yeven ~yeven

Predicate Abstraction How do we pick the abstraction function α? One solution: ’Guess’ predicates that are likely to be suﬃcient to prove desired property Predicates selected based on property being veriﬁed, major predicates in program (e.g., conditions of loop, selection statements), arithmetic properties (e.g., {pos,zero,neg}, {odd,even}), control locations (e.g., {PC=4,PC=4}), various other heuristics Abstractions may be on control as well as data Ex (using an odd-even abstraction on y): y = 0; for (i=0; i<n; i++) y += 2; assert(y%2 == 0); ⇒ yeven ~yeven But . . . a pos-neg-zero abstraction on y (or any abstraction on i, n, PC ) would not have been helpful.

Counterexample Guided Abstraction Refinement CEGAR approach to prove that property P holds in program: Pick initial abstraction predicates α While true 1 Abstraction: Construct abstract machine M from concrete program using α 2 Verification: call model checker to check M |= P. If P was provable, abort(“P is verified”) 3 Validation: else simulate counterexample symbolically on [concrete] program If concrete trace is realizable, abort(“P is false”) Refinement: else (counterexample is spurious), add predicates to α heuristically based on predicates in counterexample

CEGAR Applications/Tools 2000 Concept introduced by Clarke/Grumberg/Jha/Lu/Veith 2000 Some similar concepts embodied in Java PathFinder (NASA) and Bandera 2001 SLAM tool developed at Microsoft Research and used to verify NT device drivers (part of Windows Driver Development Kit (WDK)) 2003 Part of Astrée Static Analyzer tool, used by Airbus (among others) 2005 BLAST tool improves on SLAM predicate identification and also introduces lazy abstraction; used to verify 50K line C program. 2005 SATABS tool for automatic verification of C programs 2011 BLAST extended and integrated into CPAchecker tool Our approach: interface SATABS and CPAchecker to Frama-C

Frama-C Architecture depends of registers in AST Manipulations Abstract Interpretation Lattices Utilities Memory States Extended Cil API Lexing, Parsing, Typing, Linking Extended Cil Kernel Extended Cil AST Project Plug−in 1 Plug−in nPlug−in 2 ...... Plug−in types m Plug−in types 1 Plug−in types 2 ...... Db Frama−C Plugins Frama−C Kernel Extended Cil Dynamic From Frama-C Plugin Manual

Frama-C Architecture depends of registers in AST Manipulations Abstract Interpretation Lattices Utilities Memory States Extended Cil API Lexing, Parsing, Typing, Linking Extended Cil Kernel Extended Cil AST Project Plug−in 1 Plug−in nPlug−in 2 ...... Plug−in types m Plug−in types 1 Plug−in types 2 ...... Db Frama−C Plugins Frama−C Kernel Extended Cil Dynamic From Frama-C Plugin Manual Plugins: Interfaces to abstract syntax tree (AST), C intermediate language (CIL), AI lattices, etc. provided by kernel Plugins used for either analysis (≥ 1 AST) or source-to-source transformation (> 1 AST) Kernel-integrated plugins include value and wp (statically linked) Extensible through user-written plugins, typically linked dynamically Common plugin interface allows for inter-plugin information sharing, along with a central mechanism for combining results. All programmed in OCAML

Combining Analyses Assumption: All analyses produce correct results Mark assertions with local status {True, False if reachable, False and reachable, Unknown} Frama-C kernel consolidation of statuses from diﬀerent tools to {Not checked, Unknown (i.e., no analyzer succeeded), Valid, Valid under hyp, Invalid, Invalid under hyp, Invalid but dead, Inconsistent} (and some others covering real-world engineering issues)

Integrating AI, WP, and MC Loose coupling: Use abstract interpretation and deductive veriﬁcation to improve model checking results. Examples: 1 AI to set initial values before model checking 2 Use WP/AI to pick “good”‘ initial abstractions? Use MC to improve WP results. Some examples: 1 Use MC to prove that inner loop preserves invariant of outer loop, and wp to prove outer loop 2 Use MC to determine loop invariant? Tight Coupling: Verify a progrram by using all 3 approaches in a tightly integrated manner. These are ongoing and future research projects!

Thank you. Questions? Frama-C: downloadable from www.frama-c.com MC Plugin: downloadable from http://www.compsci.hunter.cuny.edu/~sshankar/cmc.html

Static Analysis and Verification of C Programs

More Related Content

What's hot

Viewers also liked

Similar to Static Analysis and Verification of C Programs

More from New York City College of Technology Computer Systems Technology Colloquium

Recently uploaded

Static Analysis and Verification of C Programs