Computer-Aided Verification and Software Safety Certification
This collection covers topics such as computer-aided verification, systems software, concurrency libraries, security checks for Java applets, certification of safety-critical software, and the quest for bug-free software. It explores challenges in verifying complex systems and ensuring the correctness of critical software applications.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Introduction to Computer-Aided Verification Rajeev Alur University of Pennsylvania CAV Mentoring Workshop, July 2015
Systems Software do{ KeAcquireSpinLock(); nPacketsOld = nPackets; if(request){ request = request->Next; KeReleaseSpinLock(); nPackets++; } }while(nPackets!= nPacketsOld); KeReleaseSpinLock(); Can Microsoft Windows version X be bug-free? Millions of lines of code Types of bugs that cause crashes well-known Enormous effort spent on debugging/testing code Certifying third-party code (e.g. device drivers) Do lock operations, acquire and release strictly alternate on every program execution?
Concurrency Libraries Exploiting concurrency efficiently and correctly dequeue(queue_t *queue, value_t *pvalue) { node_t *head; node_t *tail; node_t *next; while (true) { head = queue->head; tail = queue->tail; next = head->next; if (head == queue->head) { if (head == tail) { if (next == 0) return false; cas(&queue->tail, tail, next); } else { *pvalue = next->value; if (cas(&queue->head, head, next)) break; } } } delete_node(head); return true; } Concurrent Queue (MS 92) Can the code deadlock? Is sequential semantics of a queue preserved? (Sequential consistency)
Security Checks for Java Applets https://java.sun.com/javame/ public Vector<String> phoneBook; public String number; public int Selected; public void sendEvent() { phoneBook = getPhoneBook(); selected = chhoseReceiver(); number=phoneBook.elementAt(selected); if ((number==null)|(number= )){ //output error } else{ String message = inputMessage(); sendMessage(number, message); } } How to certify applications for data integrity / confidentiality ? EventSharingMidlet from J2ME By listening to messages, can one infer whether a particular entry is in the addressbook?
Certification of Safety-Critical Software How to verify that a pacemaker meets all the correctness requirements published by the FDA ?
In Search of the Holy Grail yes/proof software/model Verifier correctness specification no/bug Correctness is formalized as a mathematical claim to be proved or falsified rigorously Always with respect to the given specification Challenge: Impossibility results for automated verifier Verification problem is undecidable Even approximate versions are computationally intractable (model checking is Pspace-hard)
This Talk History of CAV (not comprehensive ) Some guidelines for choosing a research problem
1970s: Proof calculi for program correctness Key to proof: Finding suitable loop invariants BubbleSort (A : array[1..n] of int) { B = A : array[1..n] of int; for (i=0; i<n; i++) { Permute(A,B) Sorted(B[n-i,n]) for 0<k<=n-i-1 and n-i<=k <=n B[k]<=B[k ] BubbleSort (A : array[1..n] of int) { B = A : array[1..n] of int; for (i=0; i<n; i++) { for (j=0; j<n-i; j++) { Permute(A,B), Sorted(B[n-i,n], for 0<k<=n-i-1 and n-i<=k <=n B[k]<=B[k ] for 0<k<j B[k] <= B[j] for (j=0; j<n-i; j++) { }; return B; } } }; return B; } } if (B[j]>B[j+1]) swap(B,j,j+1) if (B[j]>B[j+1]) swap(B,j,j+1)
Deductive Program Verification Powerful mathematical logic (e.g. first-order logic, Higher- order logics) needed for formalization Great progress in decision procedures Finding proof decomposition requires expertise, but modern tools support many built-in proof tactics Contemporary theorem provers: Coq, PVS, ACL2, ESC-Java In practice User partially annotates the program with invariants, and the tool infers remaining invariants needed to complete the proof Success story: CompCert: Fully verified optimizing compiler for a subset of C Current research: Automatic synthesis of loop invariants
1980s: Finite-state Protocol Analysis Automated analysis of finite-state protocols with respect to temporal logic specifications Network protocols, Distributed algorithms Specs: Is there a deadlock? Does every req get ack? Does a buffer overflow? Tools: SPIN, Murphi, CADP
Battling State-space Explosion Analysis is basically a reachability problem in a HUGE graph Size of graph grows exponentially as the number of bits required for state encoding Graph is constructed only incrementally, on-the-fly Many techniques for exploiting structure: symmetry, data independence, hashing, partial order reduction Great flexibility in modeling: Scale down parameters (buffer size, number of network nodes ) State Transition Bad states
1990s: Symbolic Model Checking Constraint-based analysis of Boolean systems Symbolic Boolean representations (propositional formulas, OBDDs) used to encode system dynamics Success in finding high-quality bugs in hardware applications (VHDL/Verilog code) Global bus Deadlock found in cache coherency protocol Gigamax by model checker SMV UIC UIC UIC Cluster bus P M P M Read-shared/read-owned/write-invalid/write-shared/
Symbolic Reachability Problem Model variables X ={x1, xn} Each var is of finite type, say, boolean Initialization: I(X): a formula over X e.g. (x1 && ~x2) Update: T(X,X ) How new vars X are related to old vars X as a result of executing one step of the program: Disjunction of clauses obtained by compiling individual instructions e.g. (x1 && x1 = x1 && x2 = ~x2 && x3 = x3) Target set: F(X) e.g. (x2 && x3) Computational problem: Can F be satisfied starting with I by repeatedly applying T ? K-step reachability reduces to propositional satisfiability (SAT): Bounded Model Checking I(X0) && T(X0,X1) && T(X1,X2) && --- && T(Xk-1,Xk) && F(Xk)
The Story of SAT Propositional Satisfiability: Given a formula over Boolean variables, is there an assignment of 0/1 s to vars which makes the formula true Canonical NP-hard problem (Cook 1973) Enormous progress in tools that can solve instances with thousands of variables and millions of clauses Extensions to richer classes of constraints (SMT solvers) 1960 DP 10 var 1994 Hannibal 3k var 1996 GRASP 1k var 2002 Berkmin 10k var 1988 SOCRATES 3k var 1996 St lmarck 1000 var 1996 SATO 1k var 1986 BDDs 100 var 1992 GSAT 300 var 2001 Chaff 10k var 1952 Quine 10 var 1962 DLL 10 var
2000s: Model Checking of C code Phase 1: Given a program P, build an abstract finite-state (Boolean) model A such that set of behaviors of P is a subset of those of A (conservative abstraction) Phase 2: Model check A wrt specification: this can prove P to be correct, or reveal a bug in P, or suggest inadequacy of A do{ KeAcquireSpinLock(); nPacketsOld = nPackets; if(request){ request = request->Next; KeReleaseSpinLock(); nPackets++; } }while(nPackets!= nPacketsOld); KeReleaseSpinLock(); Shown to be effective on Windows device drivers in Microsoft Research project SLAM (follow-up: SDV) Do lock operations, acquire and release, strictly alternate on every program execution?
Software Model Checking Tools for verifying source code combine many techniques Program analysis techniques such as slicing, range analysis Abstraction Model checking Refinement from counter-examples (CEGAR) New challenges for model checking (beyond finite-state reachability analysis) Recursion gives pushdown control Pointers, dynamic creation of objects, inheritence . Active research area Abstraction-based tools: SLAM, BLAST, Direct state encoding: F-SOFT, CBMC, CheckFence
SMT Success Story CBMC SAGE VCC Spec# SMT-LIB Standardized Interchange Format (smt-lib.org) Problem classification + Benchmark repositories LIA, LIA_UF, LRA, QF_LIA, + Annual Competition (smt-competition.org) Z3 Yices CVC4 MathSAT5
Since 1990s: Cyber-Physical Systems Discrete software interacting with a continuously evolving physical system Need to model physical world using differential equations/timing delays Models: Timed automata, Hybrid automata Symbolic reachability analysis over sets of real-valued variables Finite-state abstractions Beyond correctness: Stability, Timely response Fruitful collaboration between control theory and formal methods
Formal Methods for Cyber-Physical Systems Tools for verifying timed/hybrid systems models Uppaal, Taliro, Keymaera, dReal, Space-Ex Applications Medical devices (infusion pump, pacemaker) Autonomous driving (collision avoidance protocols) Industrial technology transfer Model-based design tools (e.g. Hybrid automata as Simulink domain) Simulink Design Verifier (model-based testing, static analysis) Industry research groups (Toyota, Ford )
How to choose a research problem ? Common Themes in CAV Success Stories Phase 1: Initial demonstration of a compelling match between the capability of a research prototype and real-world need Phase 2: Sustained research on improving scalability But the path to the promised land is unclear
Incremental vs. Transformative Symbolic model checking using binary decision diagrams (McMillan et al, 1990) Importance was immediately obvious and celebrated Critical for industrial adoption of hardware model checking Chaff: Engineering an efficient SAT solver (Malik etal,2001) Low-level optimization exploiting cache perforamce Played critical role in boosting performance of SAT solvers Don t keep searching for big ideas by dismissing research problems as incremental
Source: Existing Literature vs. Real-world Problems? Hybrid automata (Alur, Henzinger et al, 1991) Started as a theoretical extension of timed automata Now with significant research and adoption in CPS community SAGE (Godefroid et al, CACM 2012) A response to pressing industrial need for effective testing for discovering security vulnerabilities Integration of many research ideas into a highly successful tool Keep looking everywhere!
Theoretical Results vs. Prototype Tools Nested depth-first search (CVWY, CAV 1990) Beautiful algorithm for on-the-fly detection of fair cycles Key ingredient of all explicit-state LTL model checkers SLAM (Ball and Rajamani, 2001) Integration of predicate abstraction, symbolic model checking, and counter-example guided abstraction refinement Prototype tool and evaluation essential to demonstrate utility CAV offers many options for research: theoretical, practical, and theory in practice!
Advice 1: Be sure of the motivation If you were to succeed in finding a good solution to the problem you are studying, what would be the consequence? Tool: who is a potential user? Algorithm: which tool can use and why should it use? Method: which design/analysis task can be done better? Be convinced of the answer yourself first, and worry about reviewers later
Advice 2: Know the related work Is your idea new? How does it fit into what people know and have tried earlier? Vast literature, but there is no way around this question Be an expert on work related to your thesis Caution: this is not an excuse for inaction!
Advice 3: Dont live in a silo! Computer science is rapidly expanding in exciting directions Need to know at a high level what s happening around you Organization into conferences/sub-disciplines is artificial Other fields can be a source of new ideas, applications, solution techniques How can statistical machine learning help CAV? Can CAV techniques be applied to problems in system biology? Goal: Become an expert in Formal Methods AND X
