The Importance of Verifying Software: Horror Stories and Costly Failures

1. 1 Software Model Checking Andrey Rybalchenko Slides partly by Rupak Majumdar

2. 2 Why verify software? Most complicated artifact routinely built today difficult to get right Horror stories

3. 3

4. 4

5. 5

6. 6 Why verify software? Most complicated artifact routinely built today difficult to get right Employed everywhere Failures are costly cost $59.5 billion annually (US) 0.6% gross domestic product (US) 80% of development costs on identifying and correcting defects [NIST, 2002]

7. 7 Formal Verification Formal verification means to apply mathematical arguments to prove the correctness of systems Systems have bugs Formal verification aims to find and correct such bugs

8. 8 What is formal verification? Build a mathematical model of the system: what are possible behaviors? Write correctness requirements in a specification language: what are desirable behaviors? Analysis: (Automatically) check that model satisfies specification Formal ) Correctness claim is a precise mathematical statement Verification ) Analysis either proves or disproves the correctness claim

9. 9 Alternative Approaches Testing: Run the system on select inputs Simulation: Simulate a model of the system on select inputs Interactive theorem proving: Formulate system correctness as a theorem in a suitable logic

10. 10 Algorithmic Analysis Algorithmic analysis (computer-aided verification) Analysis is performed by an algorithm (tool) Analysis gives counterexamples for debugging Typically requires exhaustive search of state-space Limited by high computational complexity Interactive verification Analysis reduces to proving a theorem in a logic Uses interactive theorem prover Requires more expertise

11. 11 Model Checking Coined by Clarke and Emerson (1981) to mean checking a concurrent finite state model with respect to properties in CTL More generally, denotes algorithmic analysis to check that a model (not necessarily finite state) satisfies a specified property In logic, model denotes a structure over which formulas are interpreted Model checking checks (preferably automatically) whether a given formula holds in a given model

12. 12 Why study verification? General approach to improving reliability of systems Hardware, systems software, embedded control systems, network protocols, networked embedded systems, Increasing industrial interest All major hardware companies employ in-house verification groups: Intel, Motorola, AMD, Lucent, IBM, Fujitsu, Tools from major EDA players: Synopsys Magellan, FormalCheck Bunch of start-ups: Calypto, Jasper, 0-In SDV tool from Microsoft http://research.microsoft.com/slam

13. 13 Why study verification? Interesting theoretical issues Automata theory and formal languages Logics and decidability Algorithms and data structures Mathematical foundations for concurrency and semantics Interesting practical and engineering issues Better heuristics to combat high complexity Scale to real systems Integrating reliability with design

14. 14 Where is Verification Used? Hardware verification Success in verifying microprocessor designs, ISAs, cache coherence protocols Fits in design flow Tools: SMV, nuSMV, VIS, Mocha, FormalCheck Protocol verification Network/Communications protocol implementations Tools: Spin Software verification Apply directly to source code (e.g., device drivers) Tools: SLAM, Blast, Magic Embedded and real time systems Tools: Uppaal, HyTech, Kronos, Charon

15. 15 ARMC (Abstraction Refinement Model Checker) Experimental prototype at MPI for Software Systems Termination proofs for arithmetic programs Used in industrial/academic projects: termination of Vamos kernel functions (bmbf Verisoft) termination of list/tree manipulating programs (Paris 7, Verimag)

16. 16 ARMC (Abstraction Refinement Model Checker) Experimental prototype at MPI for Software Systems Safety proofs for arithmetic programs Used in industrial/academic projects: memory safety of heap-manipulating programs (CMU, MSR Cambridge) collision avoidance in European Train Control System (SFB AVACS) parameterized hardware designs (Brno Tech. University)

17. 17 Limitations of Software Verification Tools Appropriate for control-intensive applications with interesting interaction among components Data remains a problem Decidability and complexity remains an obstacle Falsification rather than verification Model, and not system, is verified Only stated requirements are checked: how to capture correctness in a formal language? Bugs in the model checker Finding suitable abstractions require expertise

18. 18 The Methodology Answer Formal verification does not aim to produce mathematical certainty of correctness, but to provide a methodology that, when followed, produces more reliable and robust systems

19. 19 A Brief History of FV 1930s: Formal verification of programs is undecidable. Oops 1960s: [Floyd,McCarthy] Program verification Partial vs total correctness 1970s: [Hoare, Dijkstra] Logics for programs, axiomatic semantics (connect programs to logic), logical transformations for program constructs Small tricky programs, manually annotated and proved

20. 20 A Brief History of FV 1970s: Progress in automated deduction related to program verification Boyer Moore Computational Lisp Nelson Oppen: Decision procedures for combination theories Higher Order Logic theorem proving (LCF)

21. 21 A Brief History of FV 1977: Pnueli introduces (linear) temporal logics as a formalism to reason about reactive programs 1981: Clarke, Emerson and Quielle Sifakis independently discover finite state temporal logic model checking Applied to digital circuits Vardi and Wolper develop automata theoretic techniques Mid 1980s: Gerard Holzmann writes SPIN to check telecommunication protocols

22. 22 A Brief History of FV Then came State Explosion 1987 Ken McMillan suggests symbolic model checking using BDDs 10 7 -> 10 20 states and more Late 80s and early 90s: Deal with state explosion BDD hacks Abstraction, modularity, symmetry

23. 23 A Brief History of FV By 1990s: Basic theoretical questions (but one!) worked out 1990s: Emphasis on infinite state Real time systems (timed automata) Embedded systems (hybrid automata) Models with stacks, queues, 2000s: Emphasis on abstraction, implementation level checking Back to software (SLAM, Blast) But without or with few annotations

24. 24 What has changed? Ambitions are lower Look at simpler properties Use model checking as a better testing tool Computers are faster

25. 25 Model Checking, simplified program state: x = 10, y = 20, a[0] = 1, a[1] = 3, ... program transition: x = x+1 defects safety violation: path to defect effect liveness violation: path w/o effects Programs and properties: defects and effects

26. 26 Model Checking, Simplified Model checking Graph traversal What makes it interesting: The graph is huge, possibly infinite Properties can be complicated Central Theme: Make it symbolic

27. 27 Outline of Topics Representative software analysis and verification tools. Testing, symbolic execution, bug finding. Verification conditions, extended static checking. Invariant and ranking function generation. Abstract interpretation. Data flow analysis over finite domains. Pointer and alias analysis. Decision procedures. Predicate abstraction. Counterexample-guided abstraction refinement. Interpolation. Termination checking. Context-free reachability, summarization. Concurrency, race detection, atomicity.

28. 28 Lecture notes Algorithms will be presented on the blackboard (+slides) Pointers to relevant papers will appear online

29. 29 Prerequisites and Grading Prerequisites: Familiarity with basic algorithms and data structures, finite automata Grading based on homework project (30%), paper presentation (10%) and final exam (60%)

30. 30 Projects Implementation of various components ! software model checker Implementation environment: OCaml functional language Prolog declarative language with constraint solving support Try to see if formal verification has a role in your research!