IA169 System Verification and Assurance Course Intro & Fundaments of Testing http://www.testingeducation.org/BBST/ Section Course Organization IA169 System Verification and Assurance – 01 str. 2/50 Course Coverage Topics to be covered ... Introduction to Formal Verification and Testing Symbolic Execution Deductive Verification LTL (Linear Temporal Logic) Model Checking CTL (Computation Tree Logic) Model Checking Bounded Model Checking CEGAR and Abstract Interpretation Verification of Real-Time and Hybrid Systems Verification of Probabilistic Systems Assurance, Threat Models, Relevant Security Standards IA169 System Verification and Assurance – 01 str. 3/50 Prerequisites and Follow-Up Prerequisites Formally none, but we expect ... ... capability of basic math reasoning and abstractions. ... some experience with coding. ... you can handle Unix as a user. Mutual Exclusion with IV113 and IV101 Possible Follow-Up IA159 Formal Verification Methods IA169 System Verification and Assurance – 01 str. 4/50 Course Structure and Marking Structure 2/2/2 credits Lecture, Seminar, Homework Marking Final exam 70% (written test) Assignments 30% (five evaluated tasks) 50% for E or Colloquy or Credit 60% for D 70% for C 80% for B 90% for A Seminar schedule https://is.muni.cz/auth/el/1433/jaro2017/IA169/ op/IA169_2017_semestr_schedule.html IA169 System Verification and Assurance – 01 str. 5/50 Section Fundaments of Testing IA169 System Verification and Assurance – 01 str. 6/50 Testing Testing is an empirical technical investigation conducted to provide stakeholders with information about the quality of the product or service under test. Empirical Technical Conduct experimental measurements. Logic and math. Modelling. Employs SW tools. Investigation Organised and thorough. Self-reflecting. Challenging. IA169 System Verification and Assurance – 01 str. 7/50 Testing Product or Service Software. Hardware. Data. Documentation and specification. ... other parts that are delivered. Information Not know before. Has some value. Stakeholders Who has interest in the success of testing effort. Who has interest in the success of the product. IA169 System Verification and Assurance – 01 str. 8/50 Fundamental Questions of Testing Mission Why do we test? What we want to achieve? Strategy How to proceed to fulfil the mission efficiently? Oracle How to recognise success of the test. Incompletness Do we realise that testing cannot prove absence of error? Measure How much of of our testing plan has been completed? How far we are to complete the mission? IA169 System Verification and Assurance – 01 str. 9/50 Mission of Testing Most Typical Mission Bug hunting. Identification of factors that reduce quality. Other Missions Collect data to support manager decisions, such as: Is the product good enough to be released? How much different is the product from product available on market? Is the product complete with respect to specification? Are individual components logically and ergonomically connected. . . . IA169 System Verification and Assurance – 01 str. 10/50 Other Missions Other Missions – continued Support manager decision with empirical results. Evaluate the cost of support after release. To check compatibility with other products. Confirm accordance with the specification. Find safe scenarios of product usage. To acquire certification. Minimise consequences of low quality. Evaluate the product for third party. . . . IA169 System Verification and Assurance – 01 str. 11/50 Section Strategy IA169 System Verification and Assurance – 01 str. 12/50 Strategy Strategy is a plan, how to fulfil the mission in the given context. Example: Consider spreadsheet computation in four different contexts. a) Computer game. b) Early stage of development of database product. c) Late stage of development of database product. d) Driver for medical X-ray scanning device. Question: Will you proceed with the same strategy? IA169 System Verification and Assurance – 01 str. 13/50 Example – continued What factors influence strategy selection What is the mission? How aggressively we need to detect bugs. What bugs are less important than others? How thoroughly testing will be documented? Discussion Assume that a program has an enter field that is expecting numerical values. Is is meaningful to test the product for situation when we enter non-numeric value? (Not mentioned in specification at all.) IA169 System Verification and Assurance – 01 str. 14/50 Section Oracle IA169 System Verification and Assurance – 01 str. 15/50 Definition of Oracle Oracle (in the context of testing) is a detection mechanism or principle to learn that the product passed or failed a test. Facts If tester claims that the program passed a test, it does not mean the program is correct with respect to the tested property. It depends on the oracle used. Basically, any test may fail or pass with a suitable oracle. Example Does font sizes work properly in OpenOffice, WordPad, and MS Word text editors? IA169 System Verification and Assurance – 01 str. 16/50 Example – OpenOffice 1.0 IA169 System Verification and Assurance – 01 str. 17/50 Example – WordPad IA169 System Verification and Assurance – 01 str. 18/50 Example – WordPad versus MS Word IA169 System Verification and Assurance – 01 str. 19/50 Example – WordPad versus MS Word (highlighted) IA169 System Verification and Assurance – 01 str. 20/50 Example – Decisions Questions Is the observed difference in font sizes a bug in WordPad? Is the observed difference in font sizes a bug in MS Word? Is the observed difference in font sizes a bug at all? Possible Conclusions We do not know if sizes are correct, but we have tendency to believe MS Word rather than to WordPad. For WordPad it is not necessary to stick precisely to typographic standards. For WordPad it is possibly a bug, but definitely it is not a problem. IA169 System Verification and Assurance – 01 str. 21/50 Example – Risk-Based Testing Possible (Pragmatic) Position It is/isn’t a bug? =⇒ It is/isn’t a problem? It is necessary to know the context, to guess the metrics that the final consumer will use to judge the issue. With some risk we can achieve simplification of the decision. Simplification in Testing Process Avoid tests that obviously does not reveal any problems. Avoid tests that obviously reveal only uninteresting problems. IA169 System Verification and Assurance – 01 str. 22/50 Example – Judge Criteria How much do we actually know about typography? Point definition is unclear. (http://www.oberonplace.com/dtp/fonts/point.htm) Absolute sizes are difficult to measure. (http://www.oberonplace.com/dtp/fonts/fontsize.htm) From Uncertainty to Heuristics How precisely must the sizes agree in order to declare that the sizes are correct? Obtaining complete information and evaluation of all the facts is too complicated and costly. Heuristics are used instead. IA169 System Verification and Assurance – 01 str. 23/50 Oracle Problem – Heuristics Decision Heuristics Allows for simplification of decision problem. Advice, recommendation, or procedure to be used within the given context. Should not build on any hidden knowledge. Does not guarantee a good decision. Various heuristics may lead to contradictory decisions. Disadvantages Heuristics might be subjective. If misused, may cause more harm than good. IA169 System Verification and Assurance – 01 str. 24/50 Consistency as Heuristics Consistency Good heuristics for decision making. Consistency with ... other functions of the product, similar products, history, producer image, specifications, standards, user expectations, the purpose of the product, etc. Advantages Consistency is objective enough. Easily described in bug report. IA169 System Verification and Assurance – 01 str. 25/50 Imperfection in Decision Making Unintentional Blindness Human tester does not consider any test outputs that he/she does not pay attention to. Similarly, mechanical tester does not consider test outputs that it is not told to include into decision. Uncertainty Principle The presence of observer may affect what is observed. Consequence It is impossible to observe all possible outputs from a single test. IA169 System Verification and Assurance – 01 str. 26/50 Oracle and Automation Process Motivation Automation process eliminates human errors. Automation leads to repeatable procedures. Automation allows faster test evaluation. Problems of Automation It is necessary to automate the decision making (oracle) principle. Can we do it? Only partially. Standard Way of Oracle Automation A file of expected outputs, which is required to match precisely with the outputs of a test being executed. Example: MS Word could be used to define a the file of expected outputs for testing WordPad. IA169 System Verification and Assurance – 01 str. 27/50 Problems of Automated Oracle Amount of Agreement Assume MS Word to serve as the file of expected outputs for testing WordPad. How exactly is the expected output stored? Is 99% agreement still agreement? How is the percentage of agreement defined? False Alarms Using outdated expected output. Consequence of simplification of decision making. Undiscovered Errors Expected file exhibits the same error as test output. Unintentional Blindness. IA169 System Verification and Assurance – 01 str. 28/50 Section Measure Methods in Testing IA169 System Verification and Assurance – 01 str. 29/50 Coverage as a Measure Coverage A set of source code entities that has been checked with at least one test. Source-code entities: lines of code, conditions, function calls, branches, etc. Used to identify parts that have not been tested yet. Coverage as a Measure Possible test plan is to achieve a given percentage of coverage. The percentage than expresses how much of the final product has been tested. Numeric expression for managers to see how much of the product remains to be tested. IA169 System Verification and Assurance – 01 str. 30/50 Coverage as a Measure – Disadvantages Problems Could avoid testing of interesting input data. Does not properly test parts of the product that rely on external services. Using Coverage as a Measure The mission is to test all entities of the product, is that OK? Complete coverage does not guarantee quality of the product. Stimulates to prefer quantity rather than quality. Misleading satisfaction (shouldn’t feel safe). IA169 System Verification and Assurance – 01 str. 31/50 Coverage as a Measure – Disadvantages Example Input A // program accepts any Input B // integer into A and B Print A/B Observation Complete coverage is easy achievable. For example: input: 2,1 output: 2 There is of course a hidden bug in the program! IA169 System Verification and Assurance – 01 str. 32/50 Coverage Criteria for Control-Flow Graphs y:=y+1 x=y and z>w x:=x−1 true false There are various criteria for control-flow graph coverage. IA169 System Verification and Assurance – 01 str. 33/50 Coverage Criteria for Control-Flow Graphs y:=y+1 x=y and z>w x:=x−1 true false Statement coverage Every statement (assignment, input, output, condition) is executed in at least one test. Set of tests to achieve full coverage: (x = 2, y = 1, z = 4, w = 3) IA169 System Verification and Assurance – 01 str. 33/50 Coverage Criteria for Control-Flow Graphs y:=y+1 x=y and z>w x:=x−1 true false Edge coverage Every edge of CFG is executed in at least one test. Set of tests to achieve full coverage: (x = 2, y = 1, z = 4, w = 3), (x = 3, y = 3, z = 5, w = 7) IA169 System Verification and Assurance – 01 str. 33/50 Coverage Criteria for Control-Flow Graphs y:=y+1 x=y and z>w x:=x−1 true false Condition coverage Every condition is a Boolean combination of elementary conditions, for example x < y or even(x). If it is possible, every elementary condition is evaluated in at least one test to TRUE and in at least one test to FALSE. IA169 System Verification and Assurance – 01 str. 33/50 Coverage Criteria for Control-Flow Graphs y:=y+1 x=y and z>w x:=x−1 true false Condition coverage Set of tests to achieve full coverage: (x = 3, y = 2, z = 5, w = 7), (x = 3, y = 3, z = 7, w = 5) In both cases, only the FALSE branch of IF statement is taken. IA169 System Verification and Assurance – 01 str. 33/50 Coverage Criteria for Control-Flow Graphs y:=y+1 x=y and z>w x:=x−1 true false Edge/Condition coverage Edge and Condition coverage at the same time. Set of tests to achieve full coverage: (x = 2, y = 1, z = 4, w = 3), (x = 3, y = 2, z = 5, w = 7), (x = 3, y = 3, z = 7, w = 5) Is the set the smallest possible one? IA169 System Verification and Assurance – 01 str. 33/50 Coverage Criteria for Control-Flow Graphs y:=y+1 x=y and z>w x:=x−1 true false Multiple condition coverage Every Boolean combination of TRUE/FALSE values that may appear in some decision condition must occur in at least one test. IA169 System Verification and Assurance – 01 str. 33/50 Coverage Criteria for Control-Flow Graphs y:=y+1 x=y and z>w x:=x−1 true false Multiple condition coverage Set of tests to achieve full coverage: (x = 2, y = 1, z = 4, w = 3), (x = 3, y = 2, z = 5, w = 7), (x = 3, y = 3, z = 7, w = 5), (x = 3, y = 3, z = 5, w = 6) Exponential grow in the number of tests. IA169 System Verification and Assurance – 01 str. 33/50 Coverage Criteria for Control-Flow Graphs y:=y+1 x=y and z>w x:=x−1 true false Path coverage Every executable path is executed in at least one test. The number of paths is big, even infinite in case there is an unbounded cycle in the control-flow graph. IA169 System Verification and Assurance – 01 str. 33/50 Hierarchy of Coverage Criteria Criterion A includes criterion B, denoted with A → B, if after full coverage of type A we guarantee full coverage of type B. IA169 System Verification and Assurance – 01 str. 34/50 Hierarchy of Coverage Criteria Criterion A includes criterion B, denoted with A → B, if after full coverage of type A we guarantee full coverage of type B. path coverage  multiple condition coverage  edge/condition coverage uu  edge coverage  condition coverage statement coverage IA169 System Verification and Assurance – 01 str. 34/50 Cycle Coverage Coverage and Number of Cycle Iterations All criteria except the path criterion does not reflect the number of iterations over a cycle body. In case of nested cycles, systematic testing of all possible executable paths become complicated. Ad hoc Strategy for Testing Cycles Check the case when the cycle is completely skipped. Check the case when the cycle is executed exactly once. Check the case when the cycle is executed the expected number of times. If a boundary n is known for the number of cycle executions, try to design tests where the cycle is executed n − 1, n, and n + 1 times. IA169 System Verification and Assurance – 01 str. 35/50 Coverage for Data-Flow Graphs Motivation Detect usage of undefined variables. On some paths, a variable may be set for a specific purpose and later on its value misused for other purpose. Control Flow criteria do not guarantee inclusion of tests for above mentioned or likewise situations. Data Flow Coverage Cover paths through control flow graph that go through a location where a variable is used but it is not defined along all incoming paths through control-flow graph. IA169 System Verification and Assurance – 01 str. 36/50 Support for Code Coverage C/C++, Linux Tools gcov and lcov. Example: lcov gcc -fprofile-arcs -ftest-coverage foo.c -o foo lcov -d . -z lcov -c -i -d . -o base.info ./foo lcov -c -d . -o collect.info lcov -d . -a base.info -a collect.info -o result.info genhtml result.info IA169 System Verification and Assurance – 01 str. 37/50 Statistics on Found/Fixed Bugs per Time Unit Week statistics The number of newly discovered errors. The number of fixed errors. The ratio of found versus fixed errors. Visualisation IA169 System Verification and Assurance – 01 str. 38/50 Weibull Distribution Observation The number of discovered errors per time unit exhibits Weibull Distribution. Can be used as a measure for the remaining amount of testing. Software Engineering Method to set the release date. Using Weibull Distribution At the moment the curve reaches the peak, the remaining part of the curve may be predicted, hence, a moment in time may be set, when expected number of errors discovered per week drops below a given threshold. Parameters of Weibull distribution influence the “width” and “height/slope” of the peak. F(x) = 1 − e−ax−b for x > 0 IA169 System Verification and Assurance – 01 str. 39/50 Weibull Distribution – Imperfections Vague Precision Testing does not follow the typical usage of the product. The probability of error discovery is different for different errors. Fix may cause other new errors. Bugs are dependent. The number of errors in the product changes over time. Error insertion exhibits Weibull distribution itself. Testing epochs (various testing procedures) are independent. ... Conclusions Weibull Distribution is not very reliable. Can be used only with large projects for very rough estimation. IA169 System Verification and Assurance – 01 str. 40/50 Impact of following Weibull Distribution Assumption Software developers are aware of being measured. Phase one Reach the peak as quickly as possible. Double reporting of errors. Avoid fixing known errors. ... Phase two Stick to expected shape of the curve. Delay reporting of errors. Reporting outside bug-tracking system. ... IA169 System Verification and Assurance – 01 str. 41/50 Section Incompleteness of Testing IA169 System Verification and Assurance – 01 str. 42/50 Definition Observation The amount of tests to be run is extremely large. Resources for testing are always limited. What Is Not Complete Testing Complete Coverage Every line of code. Every branching point. ... When testers do not find more errors. Testing plan is finished. What Is Complete Testing There are no hidden or unknown errors in the product. If new issue is reported, testing could not be complete. IA169 System Verification and Assurance – 01 str. 43/50 Reasons for Incompletness of Testing The number of tests is too large (infinitely many). To perform all tests means: To test all possible input values of every input variable. To test all combinations of input variables. To test every possible run of a system. To test every combination of HW and SW, including future technology. To test every way a user may use the product. IA169 System Verification and Assurance – 01 str. 44/50 Impossibility to Test All Possible Inputs Data Bus-Width The number of tests grows exponentially with respect to bit used for data representation. n-bits requires 2n tests. Other Reasons Timing of actions. Invalid or unexpected inputs (buffer overflow). Edited inputs Easter egg [http://j-walk.com/ss/excel/eastereg.htm] Common Argumentation “This is not what the customer would do with our product.” IA169 System Verification and Assurance – 01 str. 45/50 Incapability to Test All Runs Assume the following system Questions How many different ways it is possible to reach EXIT ? How many different ways it is possible to reach EXIT , if A can be visited at most n-times? IA169 System Verification and Assurance – 01 str. 46/50 Incapability to Test All Runs Example In [F] is a memory leak, in [B] garbage collector. System will reach an invalid state, if [B] is avoided long enough. Observation Simplified testing of paths may not discover the error. The error manifests in circumstances that cannot be achieved with a simple test. IA169 System Verification and Assurance – 01 str. 47/50 Summary for Measure and Incompleteness Incompleteness Testing cannot prove absence of error. It is impossible to test all valid inputs. Existence of testing plan inhibits testing creativity. Measure There are methods to measure progress in testing phase. These are unreliable. Focusing strongly on a selected measure may influence the effectiveness of testing. IA169 System Verification and Assurance – 01 str. 48/50 Section Homework IA169 System Verification and Assurance – 01 str. 49/50 Homework Reading on MC/DC: http://www.faa.gov/aircraft/air_cert/design_approvals/air_ software/cast/cast_papers/media/cast-10.pdf List, and briefly describe as many black-box testing approaches as you can find or are aware of. http://www.testingeducation.org/BBST/ Optional: Learn about CMAKE and CTEST systems. IA169 System Verification and Assurance – 01 str. 50/50 IA169 System Verification and Assurance Symbolic Execution Jiří Barnat Section Testing Strategies IA169 System Verification and Assurance – 03 str. 2/38 Black-box Testing Black-box A product under test is viewed as a black box. It is analysed through the input-output behaviour. Inner details (such as source code) are hidden or not taken into account. IA169 System Verification and Assurance – 03 str. 3/38 White-box, Gray-box Testing White-box Testing (Glass-box) Inner details are taken into account. Tests are selected and executed with respect to the inner details of the product, e.g. code coverage. Error insertion, modification of the product for the purpose of testing. Basically only extends any Black-box approach. Gray-box Testing In between of Black-box and White-box. Sometimes the same as White-box, inconsistent terminology. IA169 System Verification and Assurance – 03 str. 4/38 Testing Techniques Primary Black-box Strategies Domain Testing Combinatory Testing Scenario Testing Risk-based Testing Functional Testing Fuzz Testing (Mutation Testing) Primary White-box Extensions Model-based Testing Unit Testing Support for Developers Regression Testing IA169 System Verification and Assurance – 03 str. 5/38 Section Symbolic Execution IA169 System Verification and Assurance – 03 str. 6/38 Motivation Problem To detect errors that systematically exhibit only for specific input values is difficult. Relates to incompleteness of testing. Still we would like to ... test the program on inputs that make program execute differently from what has already been tested. test the program for all inputs. IA169 System Verification and Assurance – 03 str. 7/38 Symbolic Execution Idea Execute a program so that values of input variables are referred to as to symbols instead of concrete values. Demo Program Selected concrete Symbolic values representation read(A) A = 3 A = α A = A * 2 A = 6 A = α ∗ 2 A = A + 1 A = 7 A = (α ∗ 2) + 1 output(A) IA169 System Verification and Assurance – 03 str. 8/38 Branching and Path Condition Observation Branching in the code put some restrictions on the data depending on the condition of a branching point. Example 1 if (A == 2) A = (α ∗ 2) + 1 2 then ... (α ∗ 2) + 1 = 2 3 else ... (α ∗ 2) + 1 = 2 Path Condition Formula over symbols referring to input values. Encodes history of computation, i.e. cumulative restrictions implied from all the branching points walked-through up to the curent point of execution. Initially set to true. IA169 System Verification and Assurance – 03 str. 9/38 Unfeasible Paths Observation The path condition may become unsatisfiable. If it is so, it means there are no input values that would make the program execute this way. Example 1 1 if (A == B) A = α, B = β 2 then α = β 3 if (A == B) 4 then ... α = β ∧ α = β 5 else ... α = β ∧ α = β is UNSAT 6 else ... α = β Example 2 % – operation modulo 1 A=A%2 A = α%2 2 if (A == 3) then ... α%2 = 3 is UNSAT 3 else ... α%2 = 3 IA169 System Verification and Assurance – 03 str. 10/38 Tree of Symbolic Execution Observation All possible executions of program may be represented by a tree structure – Symbolic Execution Tree. The tree is obtained by unfolding/unwinding the control flow graph of the program. Symbolic Execution Tree Node of the tree encodes program location, symbolic representation of variables, and a concrete path condition. location symbolic valuation path condition #12 A = α + 2, B = α + β − 2 α = 2 ∗ β − 1 An edge in the tree corresponds to a symbolic execution of a program instruction on a given location. Branching point is reflected as branching in the tree and causes updates of path conditions in individual branches. IA169 System Verification and Assurance – 03 str. 11/38 Example of Symbolic Execution Tree Program 1 input A,B 2 if (B<0) then 3 return 0 4 else 5 while (B > 0) 6 { B=B-1 7 A=A+B 8 } 9 return A Draw Yourself. IA169 System Verification and Assurance – 03 str. 12/38 Path Explosion Properties of Symbolic Tree Execution No nodes are merged, even if they are the same (the structure is a tree). A single program location may be contained in (infinitely) many nodes of the tree. Tree may contain infinite paths. Path Explosion Problem The number of branches in the symbolic execution tree may be large for non-trivial programs. The number of paths may grow exponentially with the number of branching points visited. IA169 System Verification and Assurance – 03 str. 13/38 Employing Symbolic Execution Tree for Verification Analysis of the Tree Breadth-first strategy, the tree may be infinite. Deduced Program Properties Identification of feasible and unfeasible paths. Proof of reachability of a given program location. Error detection (division by zero, out-of-array access, assertion violation, etc.). Synthesis of Test Input Data If the formula encoded as a path condition is satisfiable for a symbolic run, the model of the formula gives concrete input values that make the program to follow the symbolic run. Excellent for synthesis of tests that increase code coverage. IA169 System Verification and Assurance – 03 str. 14/38 Automated Test Generation Principle 1 Generate random input values (encode some random path). 2 Perform a walk through the Symbolic Execution Tree with the random input values and record the path condition. 3 Generate a new path condition from the recorded one by negating one of the restrictions related to a single branching point. 4 Find input values satisfying the new path condition. 5 Repeat from number 2 until desired coverage is reached. Practical Notes Heuristics for selection of branching point to be negated. Augmentation of the code to enable path condition recording. IA169 System Verification and Assurance – 03 str. 15/38 Limits of Symbolic Execution Undecidability Using complex arithmetic operations on unbounded domains implies general undecidability of the formula satisfaction problem. Symbolic Execution Tree is infinite (due to unwinding of cycles with unbound number of repetition). Computational Complexity Path explosion problem. Efficiency of algorithms for formula satisfiability on finite domains. Known Limits Symbolic operations on non-numerical variables. Not clear how to deal with dynamic data structures. Symbolic evaluation of calls to external functions. IA169 System Verification and Assurance – 03 str. 16/38 Section Tools for SAT Solving IA169 System Verification and Assurance – 03 str. 17/38 SAT Problem Satisfiability Problem – SAT Is to decide if there exists a valuation of Boolean variables of propositional logic formula that makes the formula hold true (be valid). SAT Problem Properties Famous NP-complete problem. Polynomial algorithm is unlikely to exist. Still there are existing SAT solvers that are very efficient and due to a plethora of heuristics can solve surprisingly large instances of the problem. IA169 System Verification and Assurance – 03 str. 18/38 Tool Z3 ZZZ aka Z3 Developed by Microsoft Research. SAT and SMT Solver. WWW interface — http://www.rise4fun.com/Z3 Standardised binary API for use within other verification tools. Decide using Z3 Is formula (a ∨ ¬b) ∧ (¬a ∨ b) satisfiable? IA169 System Verification and Assurance – 03 str. 19/38 Usage of Z3 – SAT Reformulate into language of Z3 (a ∨ ¬b) ∧ (¬a ∨ b) (declare-const a Bool) (declare-const b Bool) (assert (and (or a (not b)) (or (not a) b))) (check-sat) (get-model) Answer of Z3 sat (model (define-fun b () Bool false) (define-fun a () Bool false) ) IA169 System Verification and Assurance – 03 str. 20/38 Satisfiability Modulo Theory – SMT Satisfiability Modulo Theory – SMT Is to decide satisfiability of first order logic with predicates and function symbols that encode one or more selected theories. Typically used theories Arithmetic of integral and floating point numbers. Theories of data structures (lists, arrays, bit-vectors, . . . ). Other view (Wikipedia) SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalised approach to constraint programming. IA169 System Verification and Assurance – 03 str. 21/38 Examples of SMT in Z3 Solve using Z3 http://rise4fun.com/Z3/tutorial/guide Are there two integral non-zero numbers x and y such that y=x*(x-y)? (declare-const y Int) (declare-const x Int) (assert (= y (* x (- x y)))) (assert (not (= y 0))) (check-sat) (get-model) Are there two integral non-zero numbers x and y such that y=x*(x-(y*y))? (declare-const y Int) (declare-const x Int) (assert (= y (* x (- x (* y y))))) (assert (not (= x 0))) (check-sat) IA169 System Verification and Assurance – 03 str. 22/38 Satisfiability and Validity Observation A formula is valid if and only if its negation is not satisfiable. Consequence SAT and SMT solvers can be used as theorem provers to show validity of some theorems. Model Synthesis SAT solvers not only decide satisfiability of formulae but in positive case also give concrete valuation of variables for which the formula is valid. Unlike general theorem provers they provide a counterexample in case the theorem to be proved is invalid (negation is satisfiable). IA169 System Verification and Assurance – 03 str. 23/38 Section Concolic Testing IA169 System Verification and Assurance – 03 str. 24/38 Motivation Problem Efficient undecidability of path feasibility. In practice, unknown result often means unsatisfiability (no witness found). However, skipping paths that we only think are unfeasible, may result in undetected errors. On the other hand, executing unfeasible path may report unreal errors. Partial Solution Let us use concrete and symbolic values at the same time in order to support decisions that are practically undecidable by a SAT or SMT solver. Heuristics. An interesting case (correct): UNKNOWN =⇒ SAT Concrete and Symbolic Testing = Concolic Testing IA169 System Verification and Assurance – 03 str. 25/38 Hypothetical demo of concolic testing Program 1 input A,B 2 if (A==(B*B)%30) then 3 ERROR 4 else 5 return A Concolic Testing 1 A=22, B=7 (random values), test executed, no errors found. 2 (22==(7*7)%30) is False, path condition: α = (β ∗ β)%30 3 Synthesis of input data from negation of path condition: α = (β ∗ β)%30 – UNKNOWN 4 Employ concrete values: α = (7 ∗ 7)%30 – SAT, α = 19 5 A=19, B=7 6 Test detected error location on program line 3. IA169 System Verification and Assurance – 03 str. 26/38 Section SAGE Tool IA169 System Verification and Assurance – 03 str. 27/38 Story of SAGE Systematic Testing for Security: Whitebox Fuzzing Patrice Godefroid Michael Y. Levin and David Molnar http://research.microsoft.com/projects/atg/ Microsoft Research IA169 System Verification and Assurance – 03 str. 28/38 Story of SAGE Whitebox Fuzzing (SAGE tool)  Start with a well-formed input (not random)  Combine with a generational search (not DFS)  Negate 1-by-1 each constraint in a path constraint  Generate many children for each parent run  Challenge all the layers of the application sooner  Leverage expensive symbolic execution  Search spaces are huge, the search is partial… yet effective at finding bugs ! Gen 1 parent IA169 System Verification and Assurance – 03 str. 29/38 Story of SAGE Example: Dynamic Test Generation void top(char input[4]) { int cnt = 0; if (input[0] == ‘b’) cnt++; if (input[1] == ‘a’) cnt++; if (input[2] == ‘d’) cnt++; if (input[3] == ‘!’) cnt++; if (cnt > 3) crash(); } input = “good” IA169 System Verification and Assurance – 03 str. 30/38 Story of SAGE Dynamic Test Generation void top(char input[4]) { int cnt = 0; if (input[0] == ‘b’) cnt++; if (input[1] == ‘a’) cnt++; if (input[2] == ‘d’) cnt++; if (input[3] == ‘!’) cnt++; if (cnt > 3) crash(); } input = “good” I0 != „b‟ I1 != „a‟ I2 != „d‟ I3 != „!‟ Negate a condition in path constraint Solve new constraint  new input Path constraint: IA169 System Verification and Assurance – 03 str. 31/38 Story of SAGE Depth-First Search void top(char input[4]) { int cnt = 0; if (input[0] == ‘b’) cnt++; if (input[1] == ‘a’) cnt++; if (input[2] == ‘d’) cnt++; if (input[3] == ‘!’) cnt++; if (cnt > 3) crash(); } I0 != „b‟ I1 != „a‟ I2 != „d‟ I3 != „!‟ good input = “good” IA169 System Verification and Assurance – 03 str. 32/38 Story of SAGE Depth-First Search goo!good void top(char input[4]) { int cnt = 0; if (input[0] == ‘b’) cnt++; if (input[1] == ‘a’) cnt++; if (input[2] == ‘d’) cnt++; if (input[3] == ‘!’) cnt++; if (cnt > 3) crash(); } I0 != „b‟ I1 != „a‟ I2 != „d‟ I3 == „!‟ IA169 System Verification and Assurance – 03 str. 33/38 Story of SAGE Generational Search goo! godd gaod bood Fou Ge e atio test cases ! good void top(char input[4]) { int cnt = 0; if (input[0] == ‘b’) cnt++; if (input[1] == ‘a’) cnt++; if (input[2] == ‘d’) cnt++; if (input[3] == ‘!’) cnt++; if (cnt > 3) crash(); } I0 == „b‟ I1 == „a‟ I2 == „d‟ I3 == „!‟ IA169 System Verification and Assurance – 03 str. 34/38 Story of SAGE The Search Space void top(char input[4]) { int cnt = 0; if (input[0] == ‘b’) cnt++; if (input[1] == ‘a’) cnt++; if (input[2] == ‘d’) cnt++; if (input[3] == ‘!’) cnt++; if (cnt >= 3) crash(); } IA169 System Verification and Assurance – 03 str. 35/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000040h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 0 – seed file IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 00 00 00 00 00 00 00 00 00 00 00 00 ; RIFF............ 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000040h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 1 IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 00 00 00 00 ** ** ** 20 00 00 00 00 ; RIFF....*** .... 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000040h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 2 IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 3D 00 00 00 ** ** ** 20 00 00 00 00 ; RIFF=...*** .... 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000040h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 3 IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 3D 00 00 00 ** ** ** 20 00 00 00 00 ; RIFF=...*** .... 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 73 74 72 68 00 00 00 00 00 00 00 00 ; ....strh........ 00000040h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 4 IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 3D 00 00 00 ** ** ** 20 00 00 00 00 ; RIFF=...*** .... 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 73 74 72 68 00 00 00 00 76 69 64 73 ; ....strh....vids 00000040h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 5 IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 3D 00 00 00 ** ** ** 20 00 00 00 00 ; RIFF=...*** .... 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 73 74 72 68 00 00 00 00 76 69 64 73 ; ....strh....vids 00000040h: 00 00 00 00 73 74 72 66 00 00 00 00 00 00 00 00 ; ....strf........ 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 6 IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 3D 00 00 00 ** ** ** 20 00 00 00 00 ; RIFF=...*** .... 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 73 74 72 68 00 00 00 00 76 69 64 73 ; ....strh....vids 00000040h: 00 00 00 00 73 74 72 66 00 00 00 00 28 00 00 00 ; ....strf....(... 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 7 IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 3D 00 00 00 ** ** ** 20 00 00 00 00 ; RIFF=...*** .... 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 73 74 72 68 00 00 00 00 76 69 64 73 ; ....strh....vids 00000040h: 00 00 00 00 73 74 72 66 00 00 00 00 28 00 00 00 ; ....strf....(... 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 C9 9D E4 4E ; ............É•äN 00000060h: 00 00 00 00 ; .... Generation 8 IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 3D 00 00 00 ** ** ** 20 00 00 00 00 ; RIFF=...*** .... 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 73 74 72 68 00 00 00 00 76 69 64 73 ; ....strh....vids 00000040h: 00 00 00 00 73 74 72 66 00 00 00 00 28 00 00 00 ; ....strf....(... 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 01 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 9 IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE Zero to Crash in 10 Generations  “ta ti g ith ze o tes …  SAGE generates a crashing test for Media1 parser: 00000000h: 52 49 46 46 3D 00 00 00 ** ** ** 20 00 00 00 00 ; RIFF=...*** .... 00000010h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000020h: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ; ................ 00000030h: 00 00 00 00 73 74 72 68 00 00 00 00 76 69 64 73 ; ....strh....vids 00000040h: 00 00 00 00 73 74 72 66 B2 75 76 3A 28 00 00 00 ; ....strf²uv:(... 00000050h: 00 00 00 00 00 00 00 00 00 00 00 00 01 00 00 00 ; ................ 00000060h: 00 00 00 00 ; .... Generation 10 – crash bucket 1212954973! IA169 System Verification and Assurance – 03 str. 36/38 Story of SAGE  Since 1st i te al elease i Ap il : te s of e se u it ugs fou d  Apps: i age p o esso s, edia pla e s, file de ode s,… Confidential !  Bugs: W ite A/Vs, ‘ead A/Vs, C ashes,… Confidential !  Ma ugs fou d t iaged as se u it iti al, se e it , p io it Initial Experiences with SAGE IA169 System Verification and Assurance – 03 str. 37/38 Practicals and Homework Practicals Follow Klee tutorials 1 and 2 (http://klee.github.io/klee/Tutorials.html) Homework Solve The wolf, goat and cabbage problem with Klee Solve http://pex4fun.com/ IA169 System Verification and Assurance – 03 str. 38/38 IA169 System Verification and Assurance Deductive Verification Jiří Barnat Verification of Algorithms Validation and Verification A general goal of V&V is to prove correct behaviour of algorithms. Reminder Testing is incomplete. Testing can detect errors but cannot prove correctness. Conclusion Need for another different way of verification. IA169 System Verification and Assurance – 04 str. 2/30 Formal Verification Goal of formal Verification The goal is to show that system behaves correctly with the same level of confidence as it is given with a mathematical proof. Requirements Formally precise semantics of system behaviour. Formally precise definition of system properties to be shown. Methods of formal verification Deductive verification Model checking Abstract interpretation IA169 System Verification and Assurance – 04 str. 3/30 Section Deductive verification IA169 System Verification and Assurance – 04 str. 4/30 Notion of Correctness Program is correct if it terminates for a valid input and returns correct output. There is a need to show two parts – partial correctness and termination. Partial correctness (Correctness, Soundness) If the computation terminates for valid input values (i.e. values for which the program is defined) the resulting values are correct. Termination (Completness, Convergence) If executed on valid input values, the computation always terminates. IA169 System Verification and Assurance – 04 str. 5/30 Verification of Serial Programs Serial programs (sequential) Input-output-closed and finite programs. All input values are known prior program execution. All output values are stored in output variables. Examples: Quick sort, Greater common divider, . . . General Principle Program instructions are viewed as state transformers. The goal is to show that the mutual relation of input and output values is as expected or given by the specification. I.e. to verify the correctness of procedure of transformation of input values to output values. IA169 System Verification and Assurance – 04 str. 6/30 Expressing Program Properties State of Computation State of computation of a program is given by the value of program counter and values of all variables. Atomic predicates Basic statements about individual states of the computation. The validity is deduced purely from the values of variables given by the state of computation. Examples of atomic propositions: (x == 0), (x1 >= y3). Beware of the scope of variables. Set of States Can be described with a Boolean combination of atomic predicates. Example: (x == m) ∧ (y > 0) IA169 System Verification and Assurance – 04 str. 7/30 Expressing Program Properties – Assertions Assertion For a given program location defines a Boolean expression that should be satisfied with the current values of program variables in the given location. Invariant of a program location. Assertions – Proving Correctness Assigning properties to individual locations of Control Flow Graph. Robert Floyd: Assigning Meanings to Programs (1967) IA169 System Verification and Assurance – 04 str. 8/30 Error Detection — Assertion Violation Testing Assertion violation serves as a test oracle. Run-Time Checking Checking location invariants during run-time. Improved error localisation as the assertion violated relates to a particular program line. Undetected Errors If the error does not exhibit for given input data. If the program behaves non-deterministically (parallelism). IA169 System Verification and Assurance – 04 str. 9/30 Section Hoare Proof System IA169 System Verification and Assurance – 04 str. 10/30 Hoare Proof System Principle Programs = State Transformers. Specification = Relation between input and output state of computation. Hoare logic Designed for showing partial correctness of programs. Let P and Q be predicates and S be a program, then {P} S {Q} is the so called Hoare triple. Intended meaning of {P} S {Q} S is a program that transforms any state satisfying pre-condition P to a state satisfying post-condition Q. IA169 System Verification and Assurance – 04 str. 11/30 Pre- and Post- Conditions Example {z = 5} x = z ∗ 2 {x > 0} Valid triple, though post-condition could be more precise (stronger). Example of a stronger post-condition: {x > 5 ∧ x < 20}. Obviously, {x > 5 ∧ x < 20} =⇒ {x > 0}. The Weakest Pre-Condition P is the weakest pre-condition, if and only if {P}S{Q} is a valid triple and ∀P′ such that {P′}S{Q} is valid, P′ =⇒ P. Edsger W. Dijkstra (1975) IA169 System Verification and Assurance – 04 str. 12/30 Proving in Hoare System How to prove {P} S {Q} Pick suitable conditions P’ a Q’ Decomposition into three sub-problems: {P’} S {Q’} P =⇒ P’ Q’ =⇒ Q Use axioms and rules of Hoare system to prove {P’} S {Q’}. P =⇒ P’ and Q’ =⇒ Q are called proof obligations. Proof obligations are proven in the standard way. IA169 System Verification and Assurance – 04 str. 13/30 Hoare System – Axiom for Assignment Axiom Assignment axiom: {φ[x replaced with k]} x := k {φ} Meaning Triple {P}x := y{Q} is an axiom in Hoare system, if it holds that P is equal to Q in which all occurrences of x has been replaced with y. Examples {y+7>42} x:=y+7 {x>42} is an axiom {r=2} r:=r+1 {r=3} is not an axiom {r+1=3} r:=r+1 {r=3} is an axiom IA169 System Verification and Assurance – 04 str. 14/30 Hoare Logic – Example 1 Example Prove that the following program returns value greater than zero if executed for value of 5. Program: out := in ∗ 2 Proof 1) We built a Hoare triple: {in = 5} out := in ∗ 2 {out > 0} 2) We deduce/guess a suitable pre-condition: {in ∗ 2 > 0} 3) We prove Hoare triple: {in ∗ 2 > 0} out := in ∗ 2 {out > 0} (axiom) 4) We prove auxiliary statement: (in = 5) =⇒ (in ∗ 2 > 0) IA169 System Verification and Assurance – 04 str. 15/30 Hoare System – Example of a Rule Rule Sequential composition: {φ}S1{χ}∧{χ}S2{ψ} {φ}S1;S2{ψ} Meaning If S1 transforms a state satisfying φ to a state satisfying χ and S2 transforms a state satisfying χ to a state satisfying ψ then the sequence S1; S2 transforms a state satisfying φ to a state satisfying ψ. In the proof Should {φ}S1; S2{ψ} be used in the proof, an intermediate condition χ has to be found, and {φ}S1{χ} and {χ}S2{ψ} have to be proven. IA169 System Verification and Assurance – 04 str. 16/30 Hoare System – Partial Correctness Axiom for skip: {φ} skip {φ} Axiom for :=: {φ[x := k]}x:=k{φ} Composition rule: {φ}S1{χ}∧{χ}S2{ψ} {φ}S1;S2{ψ} Conditional rule: {φ∧B}S1{ψ}∧{φ∧¬B}S2{ψ} {φ}if B then S1 else S2 fi{ψ} While rule: {φ∧B}S{φ} {φ}while B do S od {φ∧¬B} Consequence rule: φ =⇒ φ′,{φ′}S{ψ′},ψ′ =⇒ ψ {φ}S{ψ} IA169 System Verification and Assurance – 04 str. 17/30 Hoare Logic – Example 2 Prove that for n ≥ 0 the following code computes n!. { r = 1; while (n= 0) { r = r * n; n = n - 1; } { Notes: IA169 System Verification and Assurance – 04 str. 18/30 Hoare Logic – Example 2 Prove that for n ≥ 0 the following code computes n!. { n ≥ 0 ∧ t=n } {P} r = 1; while (n= 0) { r = r * n; n = n - 1; } { r=t! } {Q} Notes: Reformulation in terms of Hoare logic. Note the use of auxiliary variable t. IA169 System Verification and Assurance – 04 str. 18/30 Hoare Logic – Example 2 Prove that for n ≥ 0 the following code computes n!. { n ≥ 0 ∧ t=n } {P} r = 1; { n ≥ 0 ∧ t=n ∧ r = 1 } {I1} while (n= 0) { r = r * n; n = n - 1; } { r=t! } {Q} Notes: {n ≥ 0 ∧ t=n ∧ 1=1} r=1 { n ≥ 0 ∧ t=n ∧ r=1 } (n ≥ 0 ∧ t=n) =⇒ (n ≥ 0 ∧ t=n ∧ 1=1) IA169 System Verification and Assurance – 04 str. 18/30 Hoare Logic – Example 2 Prove that for n ≥ 0 the following code computes n!. { n ≥ 0 ∧ t=n } {P} r = 1; { n ≥ 0 ∧ t=n ∧ r = 1 } {I1} while (n= 0) { r=t!/n! ∧ t ≥ n ≥ 0 } { {I2} r = r * n; n = n - 1; } { r=t! } {Q} Notes: Invariant of a cycle: {I2} ≡ { r=t!/n! ∧ t ≥ n ≥ 0 } I1 =⇒ I2 ( I2 ∧ ¬(n=0) ) =⇒ Q IA169 System Verification and Assurance – 04 str. 18/30 Hoare Logic – Example 2 Prove that for n ≥ 0 the following code computes n!. { n ≥ 0 ∧ t=n } {P} r = 1; { n ≥ 0 ∧ t=n ∧ r = 1 } {I1} while (n= 0) { r=t!/n! ∧ t ≥ n ≥ 0 } { {I2} r = r * n; { r=t!/(n-1)! ∧ t ≥ n > 0 } {I3} n = n - 1; } { r=t! } {Q} Notes: { r*n = t!/(n-1)! ∧ t ≥ n > 0 } r=r*n {I3} I2 ∧ (n=0) =⇒ ( r*n = t!/(n-1)! ∧ t ≥ n > 0 ) IA169 System Verification and Assurance – 04 str. 18/30 Hoare Logic – Example 2 Prove that for n ≥ 0 the following code computes n!. { n ≥ 0 ∧ t=n } {P} r = 1; { n ≥ 0 ∧ t=n ∧ r = 1 } {I1} while (n= 0) { r=t!/n! ∧ t ≥ n ≥ 0 } { {I2} r = r * n; { r=t!/(n-1)! ∧ t ≥ n > 0 } {I3} n = n - 1; } { r=t! } {Q} Notes: { r = t!/(n-1)! ∧ t ≥ (n-1) ≥ 0 } n=n-1 {I2} I3 =⇒ ( r = t!/(n-1)! ∧ t ≥ (n-1) ≥ 0 ) IA169 System Verification and Assurance – 04 str. 18/30 Hoare Logic and Completness Observation Hoare logic allowed us to reduce the problem of proving program correctness to a problem of proving a set of mathematical statements with arithmetic operations. Notice about correctness’s and (in)completeness Hoare logic is correct, i.e. if it is possible to deduce {P}S{Q} then executing program S from a state satisfying P may terminate only in a state satisfying Q. If a proof system is strong enough to express integral arithmetics, it is necessarily incomplete, i.e. there exists claims that cannot be proven or dis-proven using the system. Hoare system for proving correctness of programs is incomplete due to the proof obligations generated with the consequence rule. IA169 System Verification and Assurance – 04 str. 19/30 Hoare Logic and Proving Correctness in Practice Troubles with Proof Construction Often pre- and post- condition must be suitable reformulated for the purpose of the proof. It is very difficult to identify loop invariants. Partial Correctness in Practice Often reduced to formulation of all the loop invariants, and demonstration that they actually are the loop invariants. The proof of being an invariant is often achieved with math induction. IA169 System Verification and Assurance – 04 str. 20/30 Proving Termination Well-Founded Domain Partially ordered set that does not contain infinitely decreasing sequence of members. Examples: (N,<), (PowerSet(N),⊆) Proving Termination For every loop in the program a suitable well-founded domain and an expression over the domain is chosen. It is shown that the value associated with a location cannot grow along any instruction that is part of the loop. It is shown that there exists at least one instruction in the loop that decreases the value of the expression. IA169 System Verification and Assurance – 04 str. 21/30 Section Automating Deductive Verification IA169 System Verification and Assurance – 04 str. 22/30 Principles of Automation of Deductive Verification Pre-processing Transformation of program to a suitable intermediate language. Examples of IL: Boogie (Microsoft Research), Why3 (INRIA) Structural Analysis and Construction of the Proof Skeleton Identification of Hoare triples, loop invariants and suitable pre- and post-conditions (some of that might be given with the program to be verified). Generation of auxiliary proof obligations. Solving proof obligations Using tools for automated proving. May be human-assisted. IA169 System Verification and Assurance – 04 str. 23/30 Solving Proof Obligations Tools for Automated Proving User guides a tool to construct a proof. HOL, ACL2, Isabelle, PVS, Coq, ... Reduced to the satisfiability problem Employ SAT and SMT solvers. Z3, ... IA169 System Verification and Assurance – 04 str. 24/30 Automated Proving Proof A finite sequence of steps that using axioms and rules of a given proof system that transforms assumptions ψ into the conclusion ϕ. Observation For systems with finitely many axioms and rules, proofs may be systematically generated. Hence, for all provable claims the proof can be found in finite time. All reasonable proving systems has infinitely many axioms. Consider, e.g. an axiom x = x. This is virtually a shortcut (template) for axioms 1 = 1, 2 = 2, 3 = 3, etc. Semi-decidable with dove-tailing approach. IA169 System Verification and Assurance – 04 str. 25/30 Automated Proofing Searching for a Proof of Valid Statement The number of possible finite sequences of steps of rules and axiom applications is too many (infinitely many). In general there is no algorithm to find a proof in a given proof system even for a valid statement. Without some clever strategy, it cannot be expected that a tool for automated proof generation will succeed in a reasonable short time. The strategy is typically given by an experienced user of the automated proving tool. The user typically has to have appropriate mathematical feeling and education. At the end, the tool is used as a mechanical checker for a human constructed proof. IA169 System Verification and Assurance – 04 str. 26/30 Verification with Tools for Automated Proofing Theorem Provery The goal is find the proof within a given proof system. the proof is searched for in two modes: Algorithmic mode – Application of rules and axioms Guided by the user of the tool. Application of the general proving techniques, such as deduction, resolution, unification, . . . . Search mode – Looking for new valid statements Employs brute-force approach and various heuristics. Existing Tools The description of system (axioms, rules) as well as the claim to be proven is given in the language of the tool. IA169 System Verification and Assurance – 04 str. 27/30 Results of Proof Searching Possible Outputs a) Proof has been found and checked. b) Proof has not been found. The statement is valid, can be proven, but the proof has not yet been found. The statement is valid, but it cannot be proven in the system. The statement is invalid. Observation In the case that no proof has been found, there is no indication of why it is so. IA169 System Verification and Assurance – 04 str. 28/30 Dafny http://rise4fun.com/dafny IA169 System Verification and Assurance – 04 str. 29/30 Practicals and Homework – 04 Practicals Dafny (rise4fun.com) http://www.doc.ic.ac.uk/~scd/Dafny_Material/ Exercises_%20Arithm_Terms_Loops.docx Homework Prove correctness of the following program using Dafny method Count(N: nat, M: int, P: int) returns (R: int) { var a := M; var b := P; var i := 1; while (i <= N) { a := a+3; b := 2*a+b+1; i := i+1; } R := b; } Read and repeat: Jaco van de Pol: Automated verification of Nested DFS IA169 System Verification and Assurance – 04 str. 30/30 IA169 System Verification and Assurance LTL Model Checking Jiří Barnat Motivation Checking Quality Testing is incomplete, gives no guarantees of correctness. Deductive verification is expensive. Typical reasons for system failure Unexpected or boundary input values. Interaction of system components. Parallelism (difficult to test). Model Checking Automated verification process for ... ... parallel and distributed systems. IA169 System Verification and Assurance – 05 str. 2/45 Section Verification of Parallel and Reactive Programs IA169 System Verification and Assurance – 05 str. 3/45 Parallel Programs Parallel Composition Components concurrently contribute to the transformation of a computation state. The meaning comes from interleaving of actions (transformation steps) of individual components. Meaning Functions Do Not Compose Meaning function of a composition cannot be obtain as composition of meaning functions of participating components. The result depends on particular interleaving. IA169 System Verification and Assurance – 05 str. 4/45 Example of Incomposability Parallel System System: (y=x; y++; x=y) (y=x; y++; x=y) Input-output variable x Meaning function of both processes is λx->x+1. The composition is: (λx->x+1)·(λx->x+1). (λx->x+1)·(λx->x+1) 0 = 2 Two Different System Runs State = (x, y1, y2) (0,-,-) y1=x −→ (0,0,-) y2=x −→ (0,0,0) y1++ −→ x=y1 −→ (1,1,0) y2++ −→ x=y2 −→ (1,1,1) (0,-,-) y1=x −→ (0,0,-) y1++ −→ x=y1 −→ (1,1,-) y2=x −→ (1,1,1) y2++ −→ x=y2 −→ (2,1,2) IA169 System Verification and Assurance – 05 str. 5/45 Properties of Parallel Programs Observation Specific timing of events related to interaction of components is a form of (part of) input. Asynchronous parallel system can be viewed as reactive as there are unknown inputs at the time of execution. Consequence For parallel and reactive systems it is difficult to specify the intended behaviour using pre- and post-conditions. IA169 System Verification and Assurance – 05 str. 6/45 Properties of Parallel/Reactive Programs Examples of Specification Events A and B happens before event C. User is not allowed to enter a new value until the system processes the previous one. Procedure X cannot be executed simultaneously by processes P and Q (mutual exclusion). Every action A is immediately followed by a sequence of actions B,C and D. Turning into Formal Language Use of Modal and Temporal Logics. Amir Pnueli, 1977 IA169 System Verification and Assurance – 05 str. 7/45 Deductive Verification for Modal and Temporal Logic Observation Systems similar to Hoare Logic may be built for modal and temporal logic. Even more demanding on personal. For parallel and reactive systems exhibits similar disadvantages as techniques built on top of pre- and post-conditions. Model checking Alternative way of formal verification of systems. Specification given with formulae of some temporal logic. Based on state-space exploration. IA169 System Verification and Assurance – 05 str. 8/45 Section Model Checking IA169 System Verification and Assurance – 05 str. 9/45 Model Checking Model Checking – Overview Build a formal model M of the system under verification. Express specification as a formula ϕ of selected temporal logic. Decide, if M |= ϕ. That is, if M is a model of formula ϕ. (Hence the name.) Optionally As a side effect of the decision a counterexample may be produced. The counterexample is a sequence of states witnessing violation (in the case the system is erroneous) of the formula. Model checking (the decision process) can be fully automated for all finite (and some infinite) models of systems. IA169 System Verification and Assurance – 05 str. 10/45 Model Checking – Schema Requirements Specification Property Formalization System System Model Model Checking Simulation Counterexample Invalid Valid ErrorModelling IA169 System Verification and Assurance – 05 str. 11/45 Automated Tools for Model Checking Model Checkers Software tools that can decide validity of a formula over a model of system under verification. SPIN, UppAal, SMV, Prism, DIVINE . . . Modelling Languages Processes described as extended finite state machines. Extension allows to use shared or local variables and guard execution of a transition with a Boolean expression. Optionally, some transitions may be synchronised with transitions of other finite state machines/processes. IA169 System Verification and Assurance – 05 str. 12/45 Section Modelling and Formalisation of Verified Systems IA169 System Verification and Assurance – 05 str. 13/45 Atomic Proposition Reminder System can be viewed as a set of states that are walked along by executing instructions of the program. State = valuation of modelled variables. Atomic Propositions Basic statements describing qualities of individual states, for example: max(x, y) ≥ 3. Validity of atomic proposition for a given state must be decidable with information merely encoded by the state. Amount of observable events and facts depends on amount of abstraction used during the system modelling. IA169 System Verification and Assurance – 05 str. 14/45 Kripke Structure Kripke Structure Let AP be a set of atomic propositions. Kripke structure is a quadruple (S, T, I, s0), where S is a (finite) set of states, T ⊆ S × S is a transition relation, I : S → 2AP is an interpretation of AP. s0 ∈ S is an initial state. Kripke Transition System Let Act be a set of instructions executable by the program. Kripke structure can be extended with transition labelling to form a Kripke Transitions System. Kripke Transition System is a five-tuple (S, T, I, s0, L), where (S, T, I, s0) is Kripke Structure, L : T → Act is labelling function. IA169 System Verification and Assurance – 05 str. 15/45 Kripke Structure – Example Kripke Structure P P,S,B P,S,C Beer Coke Payment Choice AP={P – Paid, S – Served, C – Coke, B – Beer} IA169 System Verification and Assurance – 05 str. 16/45 Kripke Structure – Example Kripke Transition System P P,S,B P,S,C Takes Beer Takes Coke Chooses Coke Chooses BeerGives Coin Beer Coke Payment Choice AP={P – Paid, S – Served, C – Coke, B – Beer} IA169 System Verification and Assurance – 05 str. 16/45 System Run Run Maximal path (such that it cannot be extended) in the graph induced by Kripke Structure starting at the initial state. Let M = (S, T, I, s0) be a Kripke structure. Run is a sequence of states π = s0, s1, s2, . . . such that ∀i ∈ N0.(si , si+1) ∈ T. Finite Paths and Runs Some finite path π = s0, s1, s2, . . . , sk cannot be extended if ∄sk+1 ∈ S.(sk, sk+1) ∈ T. Technically, we will turn maximal finite path into infinite by repeating the very last state. Maximal path s0, . . . , sk will be understood as infinite run s0, . . . , sk, sk, sk, . . .. IA169 System Verification and Assurance – 05 str. 17/45 Implicit and Explicit System Description Observation Usually, Kripke structure that captures system behaviour is not given by full enumeration of states and transitions (explicitly), but it is given by the program source code (implicitly). Implicit description tends to be exponentially more succinct. State-Space Generation Computation of explicit representation from the implicit one. Interpretation of implicit representation must be formally precise. Practise Programming languages do not have precise formal semantics. Model checkers often build on top of modelling languages. IA169 System Verification and Assurance – 05 str. 18/45 En Example of Modelling Language – DVE Finite Automaton States (Locations) Initial state Transitions (Accepting states) Transitions Extended with Guards Synchronisation and Value Passing Effect (Assignment) Local Variables integer, byte channel p1 p4 p2 p3 x==b b=0,x=0 sync c?x b=b+1 b=b+1 Process B byte b,x; IA169 System Verification and Assurance – 05 str. 19/45 Example of System Described in DVE Language channel {byte} c[0]; process A { byte a; state q1,q2,q3; init q1; trans q1→q2 { effect a=a+1; }, q2→q3 { effect a=a+1; }, q3→q1 { sync c!a; effect a=0; }; } process B { byte b,x; state p1,p2,p3,p4; init p1; trans p1→p2 { effect b=b+1; }, p2→p3 { effect b=b+1; }, p3→p4 { sync c?x; }, p4→p1 { guard x==b; effect b=0, x=0; }; } system async; IA169 System Verification and Assurance – 05 str. 20/45 Semantics Shown By Interpretation State: []; A:[q1, a:0]; B:[p1, b:0, x:0] 0 0.0 : q1 → q2 { effect a = a+1; } 1 1.0 : p1 → p2 { effect b = b+1; } Command:1 ————————————————————— State: []; A:[q1, a:0]; B:[p2, b:1, x:0] 0 0.0 : q1 → q2 { effect a = a+1; } 1 1.1 : p2 → p3 { effect b = b+1; } Command:1 ————————————————————— State: []; A:[q1, a:0]; B:[p3, b:2, x:0] 0 0.0 : q1 → q2 { effect a = a+1; } Command:0 ————————————————————— State: []; A:[q2, a:1]; B:[p3, b:2, x:0] 0 0.1 : q2 → q3 { effect a = a+1; } Command:0 ————————————————————— State: []; A:[q3, a:2]; B:[p3, b:2, x:0] 0 0.2&1.2 : q3 → q1 { sync c!a; effect a = 0; } p3 → p4 { sync c?x; } Command:0 ————————————————————— State: []; A:[q1, a:0]; B:[p4, b:2, x:2] IA169 System Verification and Assurance – 05 str. 21/45 Section Formalising System Properties IA169 System Verification and Assurance – 05 str. 22/45 Specification as Languages of Infinite Words Problem How to formally describe properties of a single run? How to mechanically check for their satisfaction? Solution Employ finite automaton as a mechanical observer of run. Runs are infinite. Finite automata for infinite words (ω-regular languages). Büchi acceptance condition – automaton accepts a word if it passes through an accepting state infinitely many often. IA169 System Verification and Assurance – 05 str. 23/45 Automata over infinite words Büchi automata Büchi automaton is a tuple A = (Σ, S, s, δ, F), where Σ is a finite set of symbols, S is a finite set f states, s ∈ S is an initial state, δ : S × Σ → 2S is transition relation, and F ⊆ S is a set of accepting states. Language accepted by a Büchi automaton Run ρ of automaton A over infinite word w = a1a2 . . . is a sequence of states ρ = s0, s1, . . . such that s0 ≡ s and ∀i : si ∈ δ(si−1, ai ). inf (ρ) – Set of states that appear infinitely many time in ρ. Run ρ is accepting if and only if inf (ρ) ∩ F = ∅. Language accepted with an automaton A is a set of all words for which an accepting run exists. Denoted as L(A). IA169 System Verification and Assurance – 05 str. 24/45 Shortcuts in Transition Guards Observation Let AP={X,Y,Z}. Transition labelled with {X} denotes that X must hold true upon execution of the transition, while Y and Z are false. If we want to express that X is true, Z is false, and for Y we do not care, we have to create two transitions labelled with {X} and {X, Y }. APs as Boolean Formulae Transitions between the two same states may be combined and labelled with a Boolean formula over atomic propositions. Example Transitions {X}, {Y}, {X,Y}, {X,Z}, {Y,Z} a {X,Y,Z} can be combined into a single one labelled with X ∨ Y . If there are no restrictions upon execution of the transition, it may be labelled with true ≡ X ∨ ¬X. IA169 System Verification and Assurance – 05 str. 25/45 Task: Express with a Büchi automaton System Vending machine as seen before. Σ = 2{P,S,C,B}, Paid = {A ∈ Σ | P ∈ A}, Served = {A ∈ Σ | S ∈ A}, . . . Express the following properties Vending machine serves at least one drink. Vending machine serves at least one coke. Vending machine serves infinitely many drinks. Vending machine serves infinitely many beers. Vending machine does not serve a drink without being paid. After being paid, vending machine always serve a drink. IA169 System Verification and Assurance – 05 str. 26/45 Section Linear Temporal Logic IA169 System Verification and Assurance – 05 str. 27/45 Linear Temporal Logic (LTL) Informally Formula ϕ Is evaluated on top of a single run of Kripke structure. Express validity of APs in the states along the given run. Temporal Operators of LTL F ϕ — ϕ holds true eventually (Future). G ϕ — ϕ holds true all the time (Globally). ϕ U ψ — ϕ holds true until eventually ψ holds true (Until). X ϕ — ϕ is valid after execution of one transition (Next). ϕ R ψ — ψ holds true until ϕ ∧ ψ holds true (Release). ϕ W ψ — until, but ψ may never become true (Weak Until). IA169 System Verification and Assurance – 05 str. 28/45 Graphical Representation of LTL Temporal Operators X ϕ : •−→ ϕ •−→•−→•−→•−→• · · · ϕ U ψ : ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ψ •−→• · · · F ϕ : •−→•−→•−→•−→ ϕ •−→• · · · G ϕ : ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ϕ • · · · ϕ R ψ : ψ •−→ ψ •−→ ψ •−→ ψ •−→ ϕ∧ψ • −→• · · · or ψ •−→ ψ •−→ ψ •−→ ψ •−→ ψ •−→ ψ • · · · ϕ W ψ : ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ψ •−→• · · · or ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ϕ •−→ ϕ • · · · IA169 System Verification and Assurance – 05 str. 29/45 Syntax of LTL Let AP be a set of atomic propositions. If p ∈ AP, then p is an LTL formula. If ϕ is an LTL formula, then ¬ϕ is an LTL formula. If ϕ and ψ are LTL formulae, then ϕ ∨ ψ is an LTL formula. If ϕ is an LTL formula, then X ϕ is an LTL formula. If ϕ and ψ are LTL formulae, then ϕ U ψ is an LTL formula. Alternatively ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | X ϕ | ϕ U ϕ IA169 System Verification and Assurance – 05 str. 30/45 Syntactic shortcuts Propositional Logic ϕ ∧ ψ ≡ ¬(¬ϕ ∨ ¬ψ) ϕ ⇒ ψ ≡ ¬ϕ ∨ ψ ϕ ⇔ ψ ≡ (ϕ ⇒ ψ) ∧ (ψ ⇒ ϕ) Temporal operators F ϕ ≡ true U ϕ G ϕ ≡ ¬F ¬ϕ ϕ R ψ ≡ ¬(¬ϕ U ¬ψ) ϕ W ψ ≡ ϕ U ψ ∨ G ϕ Alternative syntax Fϕ ≡ ⋄ϕ Gϕ ≡ ϕ Xϕ ≡ ◦ϕ IA169 System Verification and Assurance – 05 str. 31/45 Models of LTL Formulae Model of an LTL formula Let AP be a set of atomic propositions. Model of an LTL formula is a run π of Kripke structure. Notation Let π = s0, s1, s2, . . .. Suffix of run π starting at sk is denoted as πk = sk, sk+1, sk+2, . . .. K-th state of the run, is referred to as π(k) = sk. IA169 System Verification and Assurance – 05 str. 32/45 Semantics of LTL Assumptions Let AP be a set of atomic propositions. Let π be a run of Kripke structure M = (S, T, I, s0). Let ϕ, ψ be syntactically correct LTL formulae. Let p ∈ AP denote atomic proposition. Semantics π |= p iff p ∈ I(π(0)) π |= ¬ϕ iff π |= ϕ π |= ϕ ∨ ψ iff π |= ϕ or π |= ψ π |= X ϕ iff π1 |= ϕ π |= ϕ U ψ iff ∃k.0 ≤ k, πk |= ψ and ∀i.0 ≤ i < k, πi |= ϕ IA169 System Verification and Assurance – 05 str. 33/45 Semantics of Other Temporal Operators π |= F ϕ iff ∃k.k ≥ 0, πk |= ϕ π |= G ϕ iff ∀k.k ≥ 0, πk |= ϕ π |= ϕ R ψ iff (∃k.0 ≤ k, πk |= ϕ ∧ ψ and ∀i.0 ≤ i < k, πi |= ψ) or (∀k.k ≥ 0, πk |= ψ) π |= ϕ W ψ iff (∃k.0 ≤ k, πk |= ψ and ∀i.0 ≤ i < k, πi |= ϕ) or (∀k.k ≥ 0, πk |= ϕ) IA169 System Verification and Assurance – 05 str. 34/45 LTL Model Checking Verification Employing LTL System is viewed as a set of runs. System is satisfies LTL formula if and only if all system runs satisfy the formula. In other words, any run violating the formula is a witness that the system does not satisfy the formula. Lemma If a finite state system does not satisfy an LTL formula then this may be witnessed with a lasso-shaped run. Run π is lasso-shaped if π = π1 · (π2)ω, where π1 = s0, s1, . . . , sk π2 = sk+1, sk+2, . . . , sk+n, where sk ≡ sk+n. Note that πω denotes infinite repetition of π. IA169 System Verification and Assurance – 05 str. 35/45 Section Automata-Based Approach to LTL Model Checking IA169 System Verification and Assurance – 05 str. 36/45 Languages of infinite words Observation One System is a set of (infinite) runs. Also referred to as formal language of infinite words. Observation Two Two different runs are equal with respect to an LTL formula if they agree in the interpretation of atomic propositions (need not agree in the states). Let π = s0, s1, . . ., then I(π) def ⇐⇒ I(s0), I(s1), I(s2), . . .. Observation Three Every run either satisfies an LTL formula, or not. Every LTL formula defines a set of satisfying runs. IA169 System Verification and Assurance – 05 str. 37/45 Reduction to Language Inclusion Problem Formulation Let the system under verification be given as Kripke structure M = (S, T, I, s0) and system specification as LTL formula ϕ. Does system M satisfies specification ϕ? (M ? |= ϕ) Reformulation as Language Problem Let Σ = 2AP be an alphabet. Language Lsys of all runs of system M is defined as follows. Lsys = {I(π) | π is a run in M}. Language Lϕ of runs satisfying ϕ is defined as follows. Lϕ = {I(π) | π |= ϕ}. Observation System M satisfies specification ϕ if and only if Lsys ⊆ Lϕ. IA169 System Verification and Assurance – 05 str. 38/45 Lsys and Lϕ expressed by Büchi automaton Theorem For every LTL formula ϕ there exists (and can be efficiently constructed) Büchi automaton Aϕ such that Lϕ = L(Aϕ). Vardi and Wolper, 1986 Theorem For every Kripke structure M = (S, T, I, s0) we can construct Büchi automaton Asys such that Lsys = L(Asys). Construction of Asys Let AP be a set of atomic propositions. Then Asys = (S, 2AP , s0, δ, S), where q ∈ δ(p, a) if and only if (p, q) ∈ T ∧ I(p) = a. IA169 System Verification and Assurance – 05 str. 39/45 Synchronous Product of Büchi Automata Theorem Let A = (SA, Σ, sA, δA, FA) and B = (SB, Σ, sB, δB, FB) be Büchi automata over the same alphabet Σ. Then we can construct Büchi automaton A × B such that L(A × B) = L(A) ∩ L(B). Construction of A × B A×B = (SA ×SB ×{0, 1}, Σ, (sA, sB, 0), δA×B, FA ×SB ×{0}) (p′, q′, j) ∈ δA×B((p, q, i), a) for all p′ ∈ δA(p, a) q′ ∈ δB(q, a) j = (i + 1) mod 2 if (i = 0 ∧ p ∈ FA) ∨ (i = 1 ∧ q ∈ FB) j = i otherwise IA169 System Verification and Assurance – 05 str. 40/45 Synchronous Product of Büchi Automata – Task Let L1 = {w ∈ {a, b, c}ω | a ∈ inf (w)} L2 = {w ∈ {a, b, c}ω | inf (w) = {b}} L3 = L1 ∩ L2 Find Büchi automata for L1, L2 and L3. IA169 System Verification and Assurance – 05 str. 41/45 Synchronous Product of Büchi Automata – Simplification Observation For the purpose of LTL model checking, we do not need general synchronous product of Büchi automata, since Büchi automaton Asys is constructed in such a way that FA = SA, i.e. it has all states accepting. For such a special case the construction of product automata can be significantly simplified. Construction of A × B when FA = SA A × B = (SA × SB, Σ, (sA, sB), δA×B, SA × FB) (p′, q′) ∈ δA×B((p, q), a) for all p′ ∈ δA(p, a) q′ ∈ δB(q, a) IA169 System Verification and Assurance – 05 str. 42/45 Reduction to Büchi Emptiness Problem Theorem For every LTL formula ϕ it holds that co−L(Aϕ) = L(A¬ϕ). By co−M we denote complement to the set of all words over the alphabet of M. Reduction of M |= ϕ to the emptiness of L(Asys × A¬ϕ) M |= ϕ ⇐⇒ Lsys ⊆ Lϕ M |= ϕ ⇐⇒ L(Asys) ⊆ L(Aϕ) M |= ϕ ⇐⇒ L(Asys) ∩ co−L(Aϕ) = ∅ M |= ϕ ⇐⇒ L(Asys) ∩ L(A¬ϕ) = ∅ M |= ϕ ⇐⇒ L(Asys × A¬ϕ) = ∅ IA169 System Verification and Assurance – 05 str. 43/45 Reduction to Accepting Cycle Detection Theorem Büchi automaton A = (S, Σ, s0, δ, F) accepts a non-empty language if and only if there is a state s ∈ F and words w1, w2 ∈ Σ∗ such that s ∈ ˆδ(s0, w1) a s ∈ ˆδ(s, w2). That is, the graph of Büchi automaton contains a reachable accepting cycle (cycle through an accepting state). Decision Procedure for M |= ϕ? Build a product automaton (Asys × A¬ϕ). Check the automaton for presence of an accepting cycle. If there is a reachable accepting cycle then M |= ϕ. Otherwise M |= ϕ. IA169 System Verification and Assurance – 05 str. 44/45 Practicals and Homework – 05 Practicals Specifying properties with Büchi Automata. Specify properties using LTL. Model-based verification using DIVINE model checker. Homework Model Peterson’s mutual exclusion protocol in ProMeLa. State expected LTL properties of Peterson’s protocol. Verify them using SPIN model checker. IA169 System Verification and Assurance – 05 str. 45/45 IA169 System Verification and Assurance LTL Model Checking (continued) Jiří Barnat Reminder Problem Kripke structure M LTL formula ϕ M |= ϕ ? Solution Based on Büchi Automata Asys – automaton accepting all system runs A¬ϕ – automaton accepting all runs violating ϕ L(Asys) ∩ L(A¬ϕ) = L(Asys × A¬ϕ) L(Asys × A¬ϕ) = ∅ ⇐⇒ system exhibits invalid run L(Asys × A¬ϕ) = ∅ ⇐⇒ M |= ϕ IA169 System Verification and Assurance – 06 str. 2/38 Algorithm for Detection of Accepting Cycles Algorithm Input Product Büchi automaton given implicitly |F|_init() — Returns initial state of automaton. |F|_succs(s) — Gives immediate successors of a given state. |Accepting|(s) — Gives whether a state is accepting or not. Algorithm Output Present/ Not present Counterexample. Algorithm Two nested depth-first search procedures – Nested DFS. Outer procedure detects accepting states, inner procedure checks for each accepting state if it is self-reachable (lies on a cycle). IA169 System Verification and Assurance – 06 str. 3/38 Section Detection of Accepting Cycles IA169 System Verification and Assurance – 06 str. 4/38 Detection of Accepting Cycles Problem Let A = (S, Σ, δ, s0, F) be a Büchi automaton. Is the language accepted by A non-empty? Reduction to Accepting Cycle Detection Problem Let G = (S, E), where E = {(u, v) ∈ S × S | ∃a ∈ Σ such that v ∈ δ(u, a)} be a graph of a Büchi automaton. L(A) is non-empty if and only if the graph of the automaton A contains reachable accepting cycle, i.e. a cycle whose at least one vertex v corresponds to an accepting state (v ∈ F), and is, at the same time, reachable from the initial state ((s0, v) ∈ E∗ ). IA169 System Verification and Assurance – 06 str. 5/38 Detection of Accepting Cycles Algorithmic Solution 1) Identify all reachable accepting states in the graph of Büchi automaton. (Outer procedure.) 2) Check for every such the state that is not self-reachable (Inner procedure.) Reachability in Directed Graph The standard graph algorithm. To compute the set of reachable vertices (or accepting vertices) can be done in in time O(|V | + |E|). Using the standard algorithm, accepting cycle detection can be done in time O(|V | + |E| + |F|(|V | + |E|)). Clever techniques can employ depth-first search post-order to reduce the time complexity to O(|V | + |E|). IA169 System Verification and Assurance – 06 str. 6/38 Depth-First Search Procedure proc Reachable(V ,E,v0) Visited = ∅ DFS(v0) return (Visited) end proc DFS(vertex) if vertex ∈ Visited then /∗ Visits vertex ∗/ Visited := Visited ∪ {vertex} foreach { v | (vertex,v)∈ E } do DFS(v) od /∗ Backtracks from vertex ∗/ fi IA169 System Verification and Assurance – 06 str. 7/38 Colour Notation in DFS Observation When running DFS on a graph all vertices can be classified into one of the three following categories (denoted with colours). Colour Notation for Vertices White vertex – Has not been visited yet. Gray vertex - Visited, but yet not backtracked. Black vertex - Visited and backtracked. Recursion Stack Gray vertices form a path from the initial vertex to the vertex that is currently processed by the outer procedure. IA169 System Verification and Assurance – 06 str. 8/38 Properties of DFS, G = (V , E) a v0 ∈ V Observation If two distinct vertices v1, v2 satisfy that (v0, v1) ∈ E∗ , (v1, v1) ∈ E+ , (v1, v2) ∈ E+ . Then procedure |DFS|(v0) backtracks from vertex v2 before it backtracks from vertex v1. DFS post-order If (v, v) ∈ E+ and (v0, v) ∈ E∗ , then upon the termination of sub-procedure |DFS|(v), called within procedure |DFS|(v0), all vertices u such that (v, u) ∈ E+ are visited and backtracked. IA169 System Verification and Assurance – 06 str. 9/38 Detection of Accepting Cycles in O(|V | + |E|) Observation If a sub-graph reachable from a given accepting vertex does not contain accepting cycle, then no accepting cycle starting in an accepting state outside the sub-graph can reach the sub-graph. The Key Idea Execute the inner procedures in a bottom-up manner. The inner procedures are called in the same order in which the outer procedure backtracks from accepting states, i.e. the ordering of calls follows a DFS post-order. IA169 System Verification and Assurance – 06 str. 10/38 Detection of Accepting Cycles in O(|V | + |E|) proc Detection_of_accepting_cycles Visited := ∅ DFS(v0) end proc DFS(vertex) if (vertex) ∈ Visited then Visited := Visited ∪ {vertex} foreach {s | (vertex,s) ∈ E} do DFS(s) od if IsAccepting(vertex) then DetectCycle(vertex) fi fi end IA169 System Verification and Assurance – 06 str. 11/38 Detection of Accepting Cycles in O(|V | + |E|) Assumption On Early Termination The inner procedure reports the accepting cycle and terminates the whole algorithm if called for an accepting vertex that lies on an accepting cycle. Consequences If the inner procedure called for an accepting vertex v reports no accepting cycle, then there is no accepting cycle in the graph reachable from vertex v. IA169 System Verification and Assurance – 06 str. 12/38 Detection of Accepting Cycles in O(|V | + |E|) Linear Complexity of Nested DFS Algorithm Employing DFS post-order it follows that vertices that have been visited by previous invocation of inner procedure may be safely skipped in any later invocation of the inner procedure. O(|V | + |E|) Algorithm 1) Nested procedures are called in DFS post-order as given by the outer procedure, and are limited to vertices not yet visited by inner procedure. 2) All vertices are visited at most twice. IA169 System Verification and Assurance – 06 str. 13/38 Detecting Cycles in Inner Procedures Theorem If the immediate successor to be processed by an inner procedure is grey (on the stack of the outer procedure), then the presence of an accepting cycle is guaranteed. Application It is enough to reach a vertex on the stack of the outer procedure in the inner procedure in order to report the presence of an accepting cycle. IA169 System Verification and Assurance – 06 str. 14/38 O(|V | + |E|) Algorithm proc Detection_of_accepting_cycles Visited := Nested := in_stack := ∅ DFS(v0) Exit("Not Present") end proc DFS(vertex) if (vertex) ∈ Visited then Visited := Visited ∪ {vertex} in_stack := in_stack ∪ {vertex} foreach {s | (vertex,s) ∈ E} do DFS(s) od if IsAccepting(vertex) then DetectCycle(vertex) fi in_stack := in_stack \ {vertex} fi end proc DetectCycle (vertex) if vertex ∈ Nested then Nested := Nested ∪ {vertex} foreach {s | (vertex,s) ∈ E} do if s ∈ in_stack then WriteOut(in_stack) Exit("Present") else DetectCycle(s) fi of fi end IA169 System Verification and Assurance – 06 str. 15/38 Time and Space Complexity Outer Procedure Time: O(|V | + |E|) Space: O(|V |) Inner Procedures Time (overall): O(|V | + |E|) Space: O(|V |) Complexity Time: O(|V | + |E| + |V | + |E|) = O(|V | + |E|) Space: O(|V | + |V |) = O(|V |) IA169 System Verification and Assurance – 06 str. 16/38 Nested DFS – Example IA169 System Verification and Assurance – 06 str. 17/38 Section Classification of Büchi Automata IA169 System Verification and Assurance – 06 str. 18/38 Sub-Classes of Büchi Automata Terminal Büchi Automata All accepting cycles are self-loops on accepting states labelled with true. Weak Büchi Automata Every strongly connected component of the automaton is composed either of accepting states, or of non-accepting states. IA169 System Verification and Assurance – 06 str. 19/38 Impact on Verification Procedure Automaton A¬ϕ For a number of LTL formulae ϕ is A¬ϕ terminal or weak. A¬ϕ is typically quite small. Type of A¬ϕ can be pre-computed prior verification. Types of components of A¬ϕ Non-accepting – Contains no accepting cycles. Strongly accepting – Every cycle is accepting. Partially accepting – Some cycles are accepting and some are not. Product Automaton The graph to be analysed is a graph of product automaton AS × A¬ϕ. Types of components of AS × A¬ϕ are given by the corresponding components of A¬ϕ. IA169 System Verification and Assurance – 06 str. 20/38 Impact on Verification Procedure – Terminal BA A¬ϕ is terminal Büchi automaton For the proof of existence of accepting cycle it is enough to proof reachability of any state that is accepting in A¬ϕ part. Verification process is reduced to the reachability problem. „Safety” Properties Those properties ϕ for which A¬ϕ is a terminal BA. Typical phrasing: „Something bad never happens.” Reachability is enough to proof the property. IA169 System Verification and Assurance – 06 str. 21/38 Impact on Verification Procedure – Weak BA A¬ϕ is weak Büchi automaton Contains no partially accepting components. For the proof of existence of accepting cycle it is enough to proof existence of reachable cycle in a strongly accepting component. Can be detected with a single DFS procedure. Time-optimal algorithm exists that does not rely on DFS. „Weak” LTL Properties Those properties ϕ for which A¬ϕ is a weak BA. Typically, responsiveness: G (a =⇒ F (b)). IA169 System Verification and Assurance – 06 str. 22/38 Classification of LTL Properties Classification Every LTL formula belongs to one of the following classes: Reactivity, Recurrence, Persistance, Obligation, Safety, Guarantee Interesting Relations Guarantee class properties can be described with a terminal Büchi automaton. Persistance, Obligation, and Safety class properties can be described with a weak Büchi automaton. Negation in Verification Process (ϕ → A¬ϕ) ϕ ∈ Safety ⇐⇒ ¬ϕ ∈ Guarantee. ϕ ∈ Recurrence ⇐⇒ ¬ϕ ∈ Persistance. IA169 System Verification and Assurance – 06 str. 23/38 Classification of LTL Properties Guarantee Obligation Safety PersistenceRecurrence Reactivity General BA Weak BA Terminal BA IA169 System Verification and Assurance – 06 str. 24/38 Section Fighting State Space Explosion IA169 System Verification and Assurance – 06 str. 25/38 State Space Explosion Problem What is State Space Explosion System is usually given as a composition of parallel processes. Depending on the order of execution of actions of parallel processes various intermediate states emerge. The number of reachable states may be up to exponentially larger than the number of lines of code. Consequence Main memory cannot store all states of the product automaton as they are too many. Algorithms for accepting cycle detection suffer for lack of memory. IA169 System Verification and Assurance – 06 str. 26/38 Some Methods to Fight State Space Explosion State Compression Lossless compression. Lossy compression – Heuristics. On-The-Fly Verification Symbolic Representation of State Space Reduced Number of States the Product Automaton Introduction of atomic blocks. Partial order on execution of process actions. Avoid exploration of symmetric parts. Parallel and Distributed Verification IA169 System Verification and Assurance – 06 str. 27/38 On-The-Fly Verification Observation Product automaton graph is defined implicitly with: |F|_init() — Returns initial state of automaton. |F|_succs(s) — Gives immediate successors of a given state. |Accepting|(s) — Gives whether a state is accepting or not. On-The-Fly Verification Some algorithms may detect the presence of accepting cycle without the need of complete exploration of the graph. Hence, M |= ϕ can be decided without the full construction of Asys × A¬ϕ. This is referred to as to on-the-fly verification. IA169 System Verification and Assurance – 06 str. 28/38 Partial Order Reduction Example Consider a system made of processes A and B. A can do a single action α, while B is a sequence of actions β, e.g. β1, . . . , βm. Unreduced State Space: βm α α α β1 β2 βm α β1 β2 s r Property to be verifed: Reachability of state r. IA169 System Verification and Assurance – 06 str. 29/38 Partial Order Reduction Observation Runs (αβ1β2 . . . βm), (β1αβ2 . . . βm), . . . , (β1β2 . . . βmα) are equivalent with respect to the property. It is enough to consider only a representative from the equivalence class, say, e.g. (β1β2 . . . βmα). βm α α α β1 β2 βm α β1 β2 s r The representative is obtained by postponing of action α. IA169 System Verification and Assurance – 06 str. 30/38 Partial Order Reduction Reduction Principle Do not consider all immediate successor during state space exploration, but pick carefully only some of them. Some states are never generated, which results in a smaller state space graph. Technical Realisation To pick correct but optimal subset of successors is as difficult as to generate the whole state space. Hence, heuristics are used. The reduced state space must contain an accepting cycle if and only if the unreduced state space does so. LTL formula must not use X operator (subclass of LTL). IA169 System Verification and Assurance – 06 str. 31/38 Distributed and Parallel Verification Principle Employ aggregate power of multiple CPUs. Increased memory and computing power. Problem of Nested DFS Typical implementation relies on hashing mechanism, hence, the main memory is accessed extremely randomly. Should memory demands exceeds the amount of available memory, thrashing occurs. Mimicking serial Nested DFS algorithm in a distributed-memory setting is extremely slow. (Token-based approach). It unknown whether the DFS post-order can be computed by a time-optimal scale-able parallel algorithm (Still an open problem.) IA169 System Verification and Assurance – 06 str. 32/38 Parallel Algorithms for Distributed-Memory Setting Observation Instead of DFS other graph procedures are used. Tasks such as breadth-first search, or value propagation can be efficiently computed in parallel. Parallel algorithms do not exhibit optimal complexity. Complexity Optimal On-The-Fly Nested DFS O(V+E) Yes Yes OWCTY general Büchi automata O(V.(V+E)) No No weak Büchi automata O(V+E) Yes No MAP O(V.V.(V+E)) No Partially OWCTY+MAP general Büchi automata O(V.(V+E)) No Partially weak Büchi automata O(V+E) Yes Partially IA169 System Verification and Assurance – 06 str. 33/38 Section Model Checking – Summary IA169 System Verification and Assurance – 06 str. 34/38 Decision Procedure and State Space Explosion Properties Validity Property to be verified may be violated by a single particular (even extremely unlikely) run of the system under inspection. The decision procedure relies on exploration of state space graph of the system. State Space Explosion Unless thee are other reasons, all system runs have to be considered. The number of states, that system can reach is up to exponentially larger than the size of the system description. Reasons: Data explosion, asynchronous parallelism. IA169 System Verification and Assurance – 06 str. 35/38 Advantages of Model Checking General Technique Applicable to Hardware, Software, Embedded Systems, Model-Based Development, . . . Mathematically Rigorous Precision The decision procedure results with M |= ϕ, if and only if, it is the case. Tool for Model Checking – Model Checkers The so called "Push-Button" Verification. No human participation in the decision process. Provides users with witnesses and counterexamples. IA169 System Verification and Assurance – 06 str. 36/38 Disadvantages of Model Checking Not Suitable for Everything Not suitable to show that a program for computing factorial really computes n! for a given n. Though it is perfectly fine to check that for a value of 5 it always returns the value of 120. Often Relies on Modelling Need for model construction. Validity of a formula is guaranteed for the model, not the modelled system. Size of the State Space Applicable mostly to system with finite state space. Due to state space explosion, practical applicability is limited. Verifies Only What Has Been Specified Issues not covered with formulae need not be discovered. IA169 System Verification and Assurance – 06 str. 37/38 Practicals and Homework – 06 Practicals Code-based reachability analysis with DIVINE model checker. Verify ring.cpp. Find error in fifo.cpp. Homework Analysis with DIVINE model checker on a more complex example (some homework from previous course on secure coding). IA169 System Verification and Assurance – 06 str. 38/38 IA169 System Verification and Assurance CTL Model Checking Jiří Barnat Liner vs. Branching Time Pnueli, 1977 System is viewed as a set of state sequences — Runs. System properties are given as properties of runs, ... and can be described with a linear-time logic. Clarke & Emerson, 1980 System is viewed as a branching structure of possible executions from individual system states — Computation Tree. System properties are given as properties of the tree, ... and can be described with a branching-time logic. IA169 System Verification and Assurance – 07 str. 2/34 System and Computation Tree 1 2 1 1 1 1 2 2 2 2 2 2 2 2 IA169 System Verification and Assurance – 07 str. 3/34 Section Computation Tree Logic (CTL) IA169 System Verification and Assurance – 07 str. 4/34 CTL Informally Possible Future Computations For a given node of a computation tree, the sub-tree rooted in the given node describes all possible runs the system can still take. Every such a run is possible future computation. CTL Formulae Allow For Specification of state qualities with atomic propositions. Quantify over possible future computations. Restrict the set of possible future computations with (quantified) LTL operators. Example ϕ ≡ EF(a) It is possible to take a future computation such that a will hold true in the computation eventually. IA169 System Verification and Assurance – 07 str. 5/34 Syntax of CTL Let AP by a set of atomic propositions. If p ∈ AP, then p is a CTL formula. If ϕ is a CTL formula, then ¬ϕ is a CTL formula. If ϕ and ψ are CTL formulae, then ϕ ∨ ψ is a CTL formula. If ϕ is a CTL formula, then EX ϕ is a CTL formula. If ϕ and ψ are CTL formulae, then E[ϕ U ψ] is a CTL formula. If ϕ and ψ are CTL formulae, then A[ϕ U ψ] is a CTL formula. Alternatively (Backus-Naur Form) ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | A[ϕ U ϕ] IA169 System Verification and Assurance – 07 str. 6/34 Syntactic Shortcuts Already Known The standard shortcuts from the propositional logic. Syntactic shortcuts from LTL F ϕ ≡ true U ϕ G ϕ ≡ ¬F ¬ϕ Deduced CTL Operators EF ϕ ≡ E[true U ϕ] AF ϕ ≡ A[true U ϕ] EG ϕ ≡ ¬AF ¬ϕ AG ϕ ≡ ¬EF ¬ϕ AX ϕ ≡ ¬EX ¬ϕ IA169 System Verification and Assurance – 07 str. 7/34 Models of CTL formulae Model of a CTL formula Let AP be a set of atomic propositions. Model of a CTL formula is a state s ∈ S of Kripke structure M = (S, T, I, s0). Reminder Run of a Kripke structure is maximal path starting at the initial state of the structure. Finite maximal paths are viewed as infinite runs due to infinite repetition of the last state on the path. Notation Let s ∈ S be a state of Kripke structure M = (S, T, I, s0). PM(s) = {π | π is a run initiated at state s} IA169 System Verification and Assurance – 07 str. 8/34 Semantics of CTL Assumptions Let AP be a set of atomic propositions. Let p ∈ AP be an atomic proposition. Let s ∈ S be a state of Kripke structure M = (S, T, I, s0). Let ϕ, ψ denote syntactically correct CTL formulae. Semantics s |= p iff p ∈ I(s) s |= ¬ϕ iff ¬(s |= ϕ) s |= ϕ ∨ ψ iff s |= ϕ or s |= ψ s |= EX ϕ iff ∃π ∈ PM(s).π(1) |= ϕ s |= E[ϕ U ψ] iff ∃π ∈ PM(s).(∃k ≥ 0.(π(k) |= ψ and ∀0 ≤ i < k.π(i) |= ϕ)) s |= A[ϕ U ψ] iff ∀π ∈ PM(s).(∃k ≥ 0.(π(k) |= ψ and ∀0 ≤ i < k.π(i) |= ϕ)) IA169 System Verification and Assurance – 07 str. 9/34 Task Atomic Propositions AP={a, b, Req, Ack, Restart} Express with CTL Formulae A state where a is true, but b is not, is reachable. If system receives a request Req then it generates acknowledgement eventually. In every run there are infinitely many b. There is always an option to reset the system (reach state Restart). IA169 System Verification and Assurance – 07 str. 10/34 Section Model Checking CTL IA169 System Verification and Assurance – 07 str. 11/34 Problem Statements Model Checking CTL Let M = (S, T, I, s0) be a Kripke structure. Let ϕ be a CTL formula. Does initial state of M satisfies ϕ? Alternatively Let M = (S, T, I, s0) be a Kripke structure. Let ϕ be a CTL formula. Compute a set of states of M satisfying ϕ. Above mentioned approaches are also referred to as to Local model checking problem — M, s0 |= ϕ. Global model checking problem — {s | M, s |= ϕ}. IA169 System Verification and Assurance – 07 str. 12/34 Algorithm for CTL Model Checking — Idea Observation If the validity of formulae ϕ and ψ is known for all states, it is easy to deduce validity of formulae ¬ϕ, ϕ ∨ ψ, EX ϕ, . . . . CTL Model Checking – Sketch Let M = (S, T, I) be a Kripke structure and ϕ a CTL Formula. A labelling function label : S → 22ϕ is computed such that it gives validity of all sub-formulae of ϕ for all states of Kripke structure M. Obviously, s0 |= ϕ ⇐⇒ ϕ ∈ label(s0). Function label is computed gradually for individual sub-formulae of ϕ, starting with the simplest sub-formula and proceeding towards more complex sub-formulae, ending with ϕ itself. IA169 System Verification and Assurance – 07 str. 13/34 Sub-formulae of a CTL Formula Sub-formulae of formula ϕ Let ϕ be a CTL formula. The set of all sub-formulae of formula ϕ is denoted by 2ϕ. 2ϕ is defined inductively according to the structure of ϕ. Inductive Definition of 2ϕ 1) ϕ ∈ 2ϕ (ϕ is a sub-formula of ϕ) 2) If η ∈ 2ϕ and η ≡ ¬ψ, then ψ ∈ 2ϕ η ≡ ψ1 ∨ ψ2, then ψ1, ψ2 ∈ 2ϕ η ≡ EX ψ, then ψ ∈ 2ϕ η ≡ E[ψ1 U ψ2], then ψ1, ψ2 ∈ 2ϕ η ≡ A[ψ1 U ψ2], then ψ1, ψ2 ∈ 2ϕ 3) Nothing else. IA169 System Verification and Assurance – 07 str. 14/34 Equivalent Existential Form of CTL Observation Is is easier to proof validity of existential quantified modal operators than validity of universally quantified ones. For the purpose of verification of CTL-specified properties, it is possible to express the CTL formula in an equivalently expressive existential form of CTL. Equivalent CTL Syntax ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | EG ϕ Task Express formula EG ϕ in the original syntax of CTL. Give accordingly modified definition of the set of sub-formulae of ϕ for the above mentioned equivalent syntax. IA169 System Verification and Assurance – 07 str. 15/34 Algorithm for CTL Model-Checking INPUT: Kripke structure M = (S, T, I, s0), CTL formula ϕ. OUTPUT: True, if s0 |= ϕ; False otherwise. proc CTLMC(ϕ, M) label := I Solved := AP ∩ 2ϕ while ϕ ∈ Solved do foreach ( η ∈ {¬ψ1, ψ1 ∨ ψ2, EX ψ1, E[ψ1 U ψ2], EG ψ1 | ψ1, ψ2 ∈ Solved})do if (η ∈ 2ϕ and η ∈ Solved) then label := updateLabel(η, label, M) Solved := Solved ∪ {η} fi od od return (ϕ ∈ label(s0)) end IA169 System Verification and Assurance – 07 str. 16/34 Algorithm for CTL Model-Checking updateLabel() proc updateLabel(η, label, M) if (η ≡ E[ψ1 U ψ2]) then return checkEU(ψ1, ψ2, label, M) fi if (η ≡ EG ψ) then return checkEG(ψ, label, M) fi foreach ( s ∈ S)do if (η ≡ ¬ψ and ψ ∈ label(s)) or (η ≡ ψ1 ∨ ψ2 and (ψ1 ∈ label(s) ∨ ψ2 ∈ label(s))) or (η ≡ EX ψ and (∃t ∈ {t | (s, t) ∈ T} such that ψ ∈ label(t))) then label(s) := label(s) ∪ {η} fi od return label end IA169 System Verification and Assurance – 07 str. 17/34 Algorithm for CTL Model-Checking E[ψ1 U ψ2] INPUT: Kripke structure M = (S, T, I), Labelling function label : S → 2ϕ , correct w.r.t validity of ψ1 and ψ2 OUTPUT: Labelling function label : S → 2ϕ , correct w.r.t E[ψ1 U ψ2] proc checkEU(ψ1, ψ2, label, M) Q := {s | ψ2 ∈ label(s)} foreach ( s ∈ Q)do label(s) := label(s) ∪ {E[ψ1 U ψ2]} od while (Q = ∅) do choose s ∈ Q Q := Q {s} foreach ( t ∈ {t | T(t, s)}) do /* all immediate predecessors */ if (E[ψ1 U ψ2] ∈ label(t) ∧ ψ1 ∈ label(t)) then label(t) := label(t) ∪ {E[ψ1 U ψ2]} Q := Q ∪ {t} fi od od return label end IA169 System Verification and Assurance – 07 str. 18/34 Strongly Connected Components Sub-graph Let G = (V , E) be a graph, ie. E ⊆ V × V . Graph G′ = (V ′, E′) is called sub-graph of G if it holds that V ′ ⊆ V and E′ = E ∩ V ′ × V ′. Sub-graph C = (V ′, E′) of G = (V , E) is called Strongly Connected Component, if ∀u, v ∈ V ′ it holds that (u, v) ∈ E′∗ and (v, u) ∈ E′∗. Maximal Strongly Connected Component (SCC), if C is strongly connected component and for every v ∈ (V V ′) it is the case that (V ′ ∪ {v}, E ∩ (V ′ ∪ {v} × V ′ ∪ {v})) is not. Non-trivial SCC, if C is Strongly Connected Component and E′ = ∅. IA169 System Verification and Assurance – 07 str. 19/34 Algorithm for CTL Model-Checking EG ψ INPUT: Kripke structure M = (S, T, I, s0), Labelling function label : S → 2ϕ , correct w.r.t. ψ OUTPUT: Labelling function label : S → 2ϕ , correct w.r.t. EG ψ proc checkEG(ψ, label, M) S’ := {s | ψ ∈ label(s)} SCC := {C | C is non-trivial SCC G′ = (S′ , T ∩ S′ × S′ )} Q := C∈SCC {s | s ∈ C} foreach ( s ∈ Q)do label(s) := label(s) ∪ {EG ψ} od while Q = ∅ do choose s ∈ Q Q := Q {s} foreach ( t ∈ (S′ ∩ {t | T(t, s)}))do /* all immediate predecessors in S′ */ if EG ψ ∈ label(t) then label(t) := label(t) ∪ {EG ψ} Q := Q ∪ {t} fi od od end IA169 System Verification and Assurance – 07 str. 20/34 Complexity of Algorithm for CTL Model Checking Observation Every CTL formula ϕ is made of at most | ϕ | sub-formulae. Decomposition of every sub-graph of G = (S, T) into SCCs can be done in time O(| S | + | T |). Every call to updateLabel terminates in time O(| S | + | T |). Overall complexity Algorithm CTLMC exhibits O(| ϕ || S |) space and O(| ϕ | (| S | + | T |)) time complexity. IA169 System Verification and Assurance – 07 str. 21/34 Example: Microwave oven AG(Start =⇒ AF(Heat)) IA169 System Verification and Assurance – 07 str. 22/34 Example: Microwave oven AG(Start =⇒ AF(Heat)) Transformation of formula ϕ ≡ AG(Start =⇒ AF(Heat)) AG(Start =⇒ AF(Heat)) AG(¬(Start ∧ ¬AF(Heat))) AG(¬(Start ∧ EG(¬Heat))) ¬EF(Start ∧ EG(¬Heat)) ¬E[true U (Start ∧ EG(¬Heat))] Validity of sub-formulae [S(ϕ) = {s | s |= ϕ}] S(Start) = {2, 5, 6, 7} S(Heat) = {4, 7} S(¬Heat) = {1, 2, 3, 5, 6} S(EG(¬Heat)) = {1, 2, 3, 5} S(Start ∧ EG(¬Heat)) = {2, 5} S(E[true U (Start ∧ EG(¬Heat))]) = {1, 2, 3, 4, 5, 6, 7} S(¬E[true U (Start ∧ EG(¬Heat))]) = ∅ IA169 System Verification and Assurance – 07 str. 23/34 Section CTL∗ IA169 System Verification and Assurance – 07 str. 24/34 CTL∗ as Extension of CTL Observation Every use of temporal operator in a formula of CTL must be immediately preceded with a quantifier, i.e. use of a modal operator without quantification is not possible. Logic CTL∗ Branching time logic. Similar to CTL. Unlike CTL, allows for standalone use of modal operators. Example A[p ∧ X(¬p)] is CTL∗, but is not CTL formula. IA169 System Verification and Assurance – 07 str. 25/34 Syntax of CTL∗ Types of CTL∗ formulae Quantifiers E and A are standalone operators in syntax construction rules. As a result there are two types of formulae in CTL: path and state formulae. Application of E and A operators on a path formula (formula of which model is a run of Kripke structure) results in a state formula (formula of which model is a state of Kripke structure) Syntax of CTL∗ state formula ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | E ψ path formula ψ ::= ϕ | ¬ψ | ψ ∨ ψ | X ψ | ψ U ψ IA169 System Verification and Assurance – 07 str. 26/34 Semantics of CTL∗ Assumption Let AP be a set of atomic propositions, and p ∈ AP. Let M = (S, T, I) be a Kripke structure. Let ϕi denote CTL∗ state formulae, and ψi denote CTL∗ state formulae. Semantics M, s |= p iff p ∈ I(s) M, s |= ¬ϕ1 iff ¬(M, s |= ϕ1) M, s |= ϕ1 ∨ ϕ2 iff M, s |= ϕ1 or M, s |= ϕ2 M, s |= E ψ1 iff ∃π ∈ PM (s).π |= ψ1 M, π |= ϕ1 iff M, π(0) |= ϕ1 M, π |= ¬ψ1 iff ¬(M, π |= ψ1) M, π |= ψ1 ∨ ψ2 iff M, π |= ψ1 or M, π |= ψ2 M, π |= X ψ1 iff M, π1 |= ψ1 M, π |= ψ1 U ψ2 iff ∃k ≥ 0.(M, πk |= ψ2 and ∀0 ≤ i < k.M, πi |= ψ1) IA169 System Verification and Assurance – 07 str. 27/34 Section Comparison of Expressive Power of LTL, CTL and CTL∗ IA169 System Verification and Assurance – 07 str. 28/34 Model Unification Observation Every LTL formula is a CTL∗ path formula. Every CTL formula is a CTL∗ state formula. Model of a path formula is a run of Kripke structure. Model of a state formula is a state of Kripke structure. Not very suitable for comparison. Model Unification For the purpose of comparison we define how a CTL∗ path formula is evaluated in a state of Kripke structure. Let ψ be CTL∗ path formula, then M, s |= ψ iff M, s |= A ψ IA169 System Verification and Assurance – 07 str. 29/34 Motivation Goal We intend to find out whether there are properties (formulae) that can be expressed in one of the logic, but cannot be expressed in another one. We intend to find out in which logic more properties can be expressed. We intend to identify concrete properties, that cannot be expressed in some other logic, i.e. to find out a formula of logic L1, for which an equivalent formula of logic L2 does not exist. Formula Equivalence Formulae ϕ and ψ are equivalent if and only if for any possible Kripke structure M = (S, T, I, s0) and any state s ∈ S it is true that M, s |= ϕ iff M, s |= ψ. IA169 System Verification and Assurance – 07 str. 30/34 Equivalent Expressive Power Equivalently Expressive Temporal logic L1 and L2 have the same expressive power, if for all Kripke structures M = (S, T, I, s0) and states s ∈ S it holds that ∀ϕ ∈ L1.(∃ψ ∈ L2.(M, s |= ϕ ⇐⇒ M, s |= ψ)) (1) ∧ ∀ψ ∈ L2.(∃ϕ ∈ L1.(M, s |= ϕ ⇐⇒ M, s |= ψ)). (2) Less Expressiveness If only statement (1) is valid, then logic L1 is less expressive than logic L2, and vice versa. IA169 System Verification and Assurance – 07 str. 31/34 Comparison of LTL, CTL, and CTL∗ Theorem LTL and CTL are incomparable in expressive power. 1) AG(EF(q)) is a CTL formula that cannot be expressed in LTL. 2) FG(q) is an LTL formula that cannot be expressed in CTL. Example – Proof Sketch for 1) Find two different Kripke structures and identify two states that can be differentiated with CTL formula AG(EF(q)), but cannot be differentiated with any LTL formula (they generate the same set of runs). Example – Intuition behind 2) [proof is too complex] Show that CTL formula AF(AG(q)) is not equivalent to LTL formula FG(q). IA169 System Verification and Assurance – 07 str. 32/34 Comparison of LTL, CTL, and CTL∗ Consequence CTL∗ is strictly more expressive than LTL. Every LTL formula is a CTL∗ formula. CTL∗ formula AG(EFq) is not expressible in LTL. Consequence 2 CTL∗ is strictly more expressive than CTL. Every CTL formula is a CTL∗ formula. CTL∗ formula FG(q) is not expressible in CTL. Observation There are properties expressible on both LTL and CTL. CTL formula A[p U q] is equivalent to LTL formula p U q. IA169 System Verification and Assurance – 07 str. 33/34 Practicals & Homework – 07 Practicals System modelling and property specification for NuSMV (NuXmv) model checker. Follow the NuSMV 2.5 tutorial Homework Solve The wolf, goat and cabbage problem with NuSMV Moshe Vardi: Branching vs. Linear Time: Final Showdown IA169 System Verification and Assurance – 07 str. 34/34 IA169 System Verification and Assurance Symbolic Representations Jiří Barnat State Space Explosion Problem and Model Checking Requirements Specification Property System System Model Model Checking Simulation Counterexample Invalid Valid ErrorModelingFormalization IA169 System Verification and Assurance – 08 str. 2/32 State Space Explosion Problem and Model Checking Verification Failure Requirements Specification Property System System Model Model Checking Simulation Counterexample Invalid Valid ErrorModelingFormalization IA169 System Verification and Assurance – 08 str. 2/32 Motivation Observation Computation state is given by valuation of state variables. Every variable has a finite domain, its value may be stored using a fixed number of bits. Computation state represented as a bit vector (a1, . . . , an) of fixed length n. Set of States Algorithms for verification store set of states. Set of state can be viewed as a set of binary vectors. Set of binary vectors may be described with a Boolean function. IA169 System Verification and Assurance – 08 str. 3/32 Boolean Functions Boolean Functions These are formulae in propositional logic over a given set of Boolean variables. Task Let system state be given by valuation of four bit variables (a1, b1, a2, b2). A state is erroneous if the values of a1 and b1 and values of a2 and b2 agree. Describe a set of erroneous states with Boolean function. Some Possible Solutions IA169 System Verification and Assurance – 08 str. 4/32 Boolean Functions Boolean Functions These are formulae in propositional logic over a given set of Boolean variables. Task Let system state be given by valuation of four bit variables (a1, b1, a2, b2). A state is erroneous if the values of a1 and b1 and values of a2 and b2 agree. Describe a set of erroneous states with Boolean function. Some Possible Solutions (a1 ∧ b1 ∧ a2 ∧ b2) ∨ (a1 ∧ b1 ∧ ¬a2 ∧ ¬b2)∨ (¬a1 ∧ ¬b1 ∧ ¬a2 ∧ ¬b2) ∨ (¬a1 ∧ ¬b1 ∧ a2 ∧ b2) a1 ⇔ b1 ∧ a2 ⇔ b2 IA169 System Verification and Assurance – 08 str. 4/32 Representation of Boolean Functions Binary Decision Trees (BDTs) Directed tree with a single root state. Every inner node is denoted with a Boolean variable (v) and lead to exactly two successors referred to as to (low(v), high(v)). Every leaf is assigned a binary value, i.e. 0 or 1. Coding of Boolean Functions with BDTs Every combination of values of input variables corresponds to exactly one path from the root of BDT to a leaf. Values stored at leaves give the the value of the function for the corresponding input values. IA169 System Verification and Assurance – 08 str. 5/32 Binary Decision Tree ψ = (a1 ⇔ b1) ∧ (a2 ⇔ b2) IA169 System Verification and Assurance – 08 str. 6/32 Representation of Boolean Functions Disadvantage of BDTs BDTs are uselessly space demanding (contain redundant information). Task Identify isomorphic sub-trees of the BDT from the previous slide. Binary Decision Diagrams (BDD) Acyclic directed graph, of which vertices have output degree either zero (leaf) or two (inner vertex). Vertices of BDD have otherwise the same properties as BDT nodes. IA169 System Verification and Assurance – 08 str. 7/32 Computing (minimal) BDD Initialisation For a given Boolean function take arbitrary BDD or BDT. Eliminate unreachable vertices Eliminate duplicate 1) Remove all but one leaves with the same value. 2) All edges incident with eliminated leaves reconnect to the the remaining leaf with the same value. Repeat Until Fixpoint Eliminate duplicate inner vertices. If there are two inner vertices u, v with the same label such that low(v) = low(u) a high(v) = high(u), then remove u and reconnect edges originally leading to u to v. Eliminate useless tests Eliminate inner vertex v if low(v) = high(v). Reconnect edges originally leading to v to low(v). IA169 System Verification and Assurance – 08 str. 8/32 BDD pro ψ = (a1 ⇔ b1) ∧ (a2 ⇔ b2) IA169 System Verification and Assurance – 08 str. 9/32 Coding of Boolean Functions with BDDs Observation Every vertex v of BDD encodes some Boolean function Fv (x1, . . . , xn). Computing Fv (x1, . . . , xn) for values h1, . . . , hn. If v is a leaf then Fv (h1, . . . , hn) = 1, if v is labelled with value 1. Fv (h1, . . . , hn) = 0, if v is labelled with value 0. If v is an inner vertex then Fv (h1, . . . , hn) = Flow(v)(h1, . . . , hn), if hi == 0. Fv (h1, . . . , hn) = Fhigh(v)(h1, . . . , hn), if hi == 1. IA169 System Verification and Assurance – 08 str. 10/32 Ordering Variables in BDD — OBDD Observation Some intermediate representation computed during minimisation of a BDD are also valid BDDs. A given Boolean function may be represented with multiple different BDDs. Canonical Form for BDD Minimal BDD computed from a BDD, or BDT with a fixed ordering on variables in inner vertices is unique. BDD with a fixed variable ordering is referred to as to Ordered BDD (OBDD). Computing Canonical Form Apply algorithm for minimal BDD. If performed in a bottom-up manner, obtained in linear time w.r.t. the size of initial BDT or BDD. IA169 System Verification and Assurance – 08 str. 11/32 OBDDs for Different Variable Ordering IA169 System Verification and Assurance – 08 str. 12/32 Restriction Operator for OBDDs Observation Every OBDD represents some Boolean function. Boolean functions can be combined/composed using unary and binary logic operators such as ¬, ∧, ∨, =⇒ , XOR, . . .. OBDDs can be composed similarly. Application of Logic Operators on OBDD Let O and O′ be OBDDs corresponding to functions f and f ′ , respectively. We will refer to function Apply(O, O′ , ⋆), as to function that computes OBDD that represents result of application of logic operator ⋆ to functions f and f ′ . IA169 System Verification and Assurance – 08 str. 13/32 Operation of Restriction Operation of Restriction Fxi ←b(x1, . . . , xn) = F(x1, . . . , xi−1, b, xi+1, . . . , xn) Produces Boolean function with all but one free variables. Realisation for OBDD If root r is denoted with the restricted variable xi , the resulting OBDD will have new root low(r) if b = 0 high(r) if b = 1 Any edge leading to a inner vertex t that is denoted with the restricted variable xi is reconnected to low(t) if b = 0 high(t) if b = 1 OBDD is minimised (contains unreachable nodes). IA169 System Verification and Assurance – 08 str. 14/32 Shannon expansion Shannon expansion Any binary logic operator can be applied on OBDDs using Shannon expansion: F = (¬x ∧ Fx←0) ∨ (x ∧ Fx←1) If F = f ⋆ f ′ , for any binary logic operation ⋆, then f ⋆ f ′ = (¬x ∧ (fx←0 ⋆ f ′ x←0)) ∨ (x ∧ (fx←1 ⋆ f ′ x←1)) IA169 System Verification and Assurance – 08 str. 15/32 Algorithm for Application of Binary Operators on OBDDs Apply(O, O′ , ⋆) Let v, v′ be root nodes of O, O′ , denoted with x, x′ , respectively. If v and v′ are leaves denoted with values h and h′ , respectively, then return a leave denoted with h ⋆ h′ . Otherwise, if x = x′ then return a new node w denoted with variable x, where low(w) = Apply(low(v), low(v′ ), ⋆) high(w) = Apply(high(v), high(v′ ), ⋆) x < x′ then return a new node w denoted with variable x, where low(w) = Apply(low(v), O′ , ⋆) high(w) = Apply(high(v), O′ , ⋆) x′ < x then return a new node w denoted with variable x, where low(w) = Apply(O, low(v), ⋆) high(w) = Apply(O, high(v), ⋆) IA169 System Verification and Assurance – 08 str. 16/32 Negation Operation and Emptiness Check Observation Let OBDD X encodes function FX , then OBDD Y encoding negation function ¬FX is created as a copy of OBDD X in which values of leaves are switched. Emptiness Check OBDDs have canonical form. Canonical OBDD representing an empty set is made of a single leaf denoted with 0. Test for a Presence of Set Member (complicated way) Create an OBDD describing the tested member. Apply operation ∧ on tested and newly created OBDDs. Employ emptiness check on the resulting OBDD. IA169 System Verification and Assurance – 08 str. 17/32 Section Symbolic Representation of Kripke Structure IA169 System Verification and Assurance – 08 str. 18/32 Encoding of Transitions of Kripke Structure Observation A state of Kripke structure M = (S, T, I) is given by n binary variables a1, . . . , an. Every set of states of Kripke structure can be encoded by an OBDD with n variables. Similarly, transition relation T ⊆ S × S can be encoded by Boolean function with 2n variables. Simplification of OBDD Edges leading to zero leaf can be omitted. Non-existence of an edge indicates an edge to zero leaf. IA169 System Verification and Assurance – 08 str. 19/32 Task M = ({00, 01, 11}}, {(11, 00), (11, 01), (01, 00)}, I) 11 01 00 T can be encoded as F(a, b, a′ , b′ ) F(a, b, a′ , b′ ) = (a∧b ∧¬a′ ∧b′ )∨(a∧b ∧¬a′ ∧¬b′ )∨(¬a∧b ∧¬a′ ∧¬b′ ) Assume variable ordering a < b < a′ < b′ and draw OBDD for F. IA169 System Verification and Assurance – 08 str. 20/32 Successors of States Observation Assume M = (S, T, I) and OBDDT (a, b, a′ , b′ ). Let X be a set of states given with OBDDX (a, b). Using OBDDT and OBDDX , OBDDX′ (a′ , b′ ) representing set of successors of states in X can be computed, i.e. X′ = {v ∈ S | u ∈ X ∧ (u, v) ∈ T}. IA169 System Verification and Assurance – 08 str. 21/32 Successors of States – Algorithm Idea Computing OBDDX′ (intuitively) OBDDX′ = Apply(OBDDT , OBDDX , ∧) Modify OBDD′ X so that every path of it contains vertex labelled with a′ . In OBDDX′ erase all vertices labelled with a and b. Iterate over all a′ vertices, consider them as root and compute respective minimal OBDDs. The computed set of OBDDs combine with operation ∨. Minimise the resulting OBDD. Rename primed variables to unprimed. Task Compute OBDD representing successors of states {00, 11}. IA169 System Verification and Assurance – 08 str. 22/32 Predecessors of States Computing Predecessors (intuitively). Modify all vertices of OBDDX to be labelled with primed variables. OBDDX′ = Apply(OBDDT , OBDDX , ∧) Modify OBDD′ X so that every path contains vertex labelled with a′ . Those a′ that cannot reach leaf labelled with 1 replace with a new zero leaf. Other a′ vertices replace with the other leaf. Remove all primed nodes and old leaves, and minimise OBDD. Task Compute OBDD representing predecessor of state {00}. IA169 System Verification and Assurance – 08 str. 23/32 Section Symbolic Approach to Model Checking CTL IA169 System Verification and Assurance – 08 str. 24/32 Reminder Observation If validity of formulae ϕ and ψ is known for all states of Kripke structure, validity of formulae ¬ϕ, ϕ ∨ ψ, EX ϕ, etc., can be easily deduced. Algorithm Idea for Model Checking CTL Let M = (S, T, I) be a Kripke structure and ϕ a CTL formula. Labelling function label : S → 2ϕ is computed, stating which sub-formulae of ϕ are valid in which states of M. Obviously, s0 |= ϕ ⇐⇒ ϕ ∈ label(s0). Function label is computed gradually for every sub-formula of ϕ starting with the simplest sub-formulae (atomic propositions) and terminating after computing the validity of ϕ. IA169 System Verification and Assurance – 08 str. 25/32 Symbolic Approach Idea Set of states in which particular sub-formulae hold can be efficiently represented with OBDDs. Computation of label function for more complex sub-formulae employs manipulation with respective OBDDs. Realisation Set of states represented with OBDDs. Boolean functions to evaluate atomic proposition form initial OBDDs. According to the structure of the verified formula OBDDs for more complex sub-formulae are computed. Test membership of initial state of Kripke structure in the set of states satisfying verified formula. IA169 System Verification and Assurance – 08 str. 26/32 Atomic Propositions and Logic Operators Recall Syntax of CTL ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | EG ϕ Computing Set of States Satisfying CTL Formula Notation F(ψ) denotes (a function describing) set of states satisfying ψ. Succ(X) denotes immediate successors of states in the set X. Pred(X) denotes immediate predecessors of states in the set X. Boolean Functions for Atomic Proposition Atomic propositions describe properties of state variables. Atomic Propositions can be encoded as Boolean functions. Computing Boolean Operators ¬ and ∨ F(¬ψ1) = ¬(Fψ1) F(ϕ ∨ ψ) = F(ϕ) ∨ F(ψ) IA169 System Verification and Assurance – 08 str. 27/32 Temporal operators EX(ϕ), E[ϕ U ψ] and EG(ϕ) Operator EX(ϕ) F(EX(ϕ)) = Pred(F(ϕ)) Operator E(ϕ U ψ) F(E(ϕ U ψ)) = X, where X is the least fix-point of recursive rule X = F(ψ) ∪ (F(ϕ) ∩ EX(X)) Operator EG (ϕ) F(EG ϕ) = X, where X is the greatest fix-point of recursive rule X = F(ϕ) ∩ EX(X) IA169 System Verification and Assurance – 08 str. 28/32 Computing Fix-Points of Function f The Least Fix-Point proc LFP(f ) X = ∅ Xold = ∅ do Xold = X X := f (X) while (X = Xold) end The Greatest Fix-Point proc GFP(f ) X = S Xold = S do Xold = X X := f (X) while (X = Xold) end IA169 System Verification and Assurance – 08 str. 29/32 Section Model Checking – Summary IA169 System Verification and Assurance – 08 str. 30/32 Model Checking – Summary Enumerative × Symbolic Approach Enumerative – focused on "control-flow" Symbolic – focused on "data-flow" Pros w.r.t. Testing No source-code necessary (can be applied on models). Suitable for testing of parallel programs. Pros w.r.t. Static Analysis Complete for systems with a finite state space. Verification of temporal properties. Cons State space explosion problem. IA169 System Verification and Assurance – 08 str. 31/32 Practicals and Homework – 08 Practicals Construct BDD for multiplication of 2-bit wide integers. Consider extension to n-bit integers. Other symbolic representations: SAT and SMT solvers Z3 (rise4fun.com) Homework Explore Z3 tutorial (rise4fun.com). IA169 System Verification and Assurance – 08 str. 32/32 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, a′ 1, a′ 2, ..., a′ n 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 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 – 10 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 – 10 str. 3/27 Section Data and Predicate Abstraction IA169 System Verification and Assurance – 10 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 – 10 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 – 10 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 – 10 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 – 10 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 – 10 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 – 10 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 – 10 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 – 10 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 – 10 str. 13/27 Section CEGAR Approach IA169 System Verification and Assurance – 10 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 – 10 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 – 10 str. 16/27 Section Basics of Abstract Interpretation and Static Analysis of Programs IA169 System Verification and Assurance – 10 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 – 10 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 – 10 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 – 10 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 – 10 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 unwind 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 – 10 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 – 10 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 – 10 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 – 10 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 – 10 str. 26/27 Practicals and Homework – 10 Practicals Catch-up time. 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 – 10 str. 27/27 IA169 System Verification and Assurance Verification of Real-Time and Hybrid systems Jiří Barnat Verification in Model-Based Development Software Engineering Experience Employing V&V techniques too late in the development process significantly increases the cost of poor quality. The sooner a bug is detected the cheaper is the fix. Model-Based Development Model-Based Verification Model-Based Development Consider models of the target system in order to ,e.g., simulate its behaviour in the design phase prior implementation. Behavioural models can be used for verification. IA169 System Verification and Assurance – 11 str. 2/48 Hybrid Systems Hybrid Systems Systems that combine multiple kinds of dynamics. Continuous systems driven by discrete events. Areas of existence Mechanical systems Continuous movement and contact with physical obstacle. Electrical systems Continuous nature of electric charge in circuit driven by discrete switches. Embedded systems Computer-driven systems in analogue environment. IA169 System Verification and Assurance – 11 str. 3/48 Example – Bouncing Ball System Description A ball released at height h bounces on a hard surface. The ball is under continuous influence of the gravity (9.8m/s). When bounces some energy is consumed by friction and elasticity and turns into heat. Physics Acceleration = First derivative of speed with respect to time. Speed = First derivative of height with respect to time. Abstraction and simplification Modelled with a mass point. Instant (time-less) bounce. IA169 System Verification and Assurance – 11 str. 4/48 Bouncing Mass Point – Hybrid Automaton Automaton Description x1 — height x2 — vertical speed (+ means up, − means down) c ∈ [0, 1] — loss of energy (elasticity and heat) Schema IA169 System Verification and Assurance – 11 str. 5/48 Analyses and Control of Hybrid Systems Questions What time elapses between the fourth and fifth bounce? If given horizontal speed, will the ball jump over an obstacle? . . . Searching for Answers Need for precise formal description of hybrid system. Algorithmic analysis of properties of hybrid systems and controller synthesis. IA169 System Verification and Assurance – 11 str. 6/48 Section Hybrid Automata IA169 System Verification and Assurance – 11 str. 7/48 Hybrid Automata Hybrid Automaton is a tuple Q = {q1, q2, . . .} — Set of discrete states. X = Rn — Set of continuous states. f : Q × X → Rn — System dynamics. Init ⊆ Q × X — Set of initial states. Dom : Q → PowerSet(X) — State invariants. E ⊆ Q × Q — Set of discrete transitions G : E → PowerSet(X) — Map of transition guards. R : E × X → PowerSet(X) — Map of transition resets. IA169 System Verification and Assurance – 11 str. 8/48 State of Hybrid Automaton State of Hybrid Automaton Given by the discrete state and the current value of continuous variables: (q, −→x ) ∈ Q × X. Initial State Set of initial states in both the discrete and continuous part. (q0, −→x0 ) ∈ I IA169 System Verification and Assurance – 11 str. 9/48 Transitions of Hybrid Automaton Transition by Time Passing Let (q, −→x ) be origin state. Continuous part for every variable x follows the system dynamics dx(t) dt = f (q, x), where x(0) = x Discrete part does not change: q(t) = q Time may pass only if the state invariant is valid: x(t) ∈ Dom(q) IA169 System Verification and Assurance – 11 str. 10/48 Transitions of Hybrid Automaton Discrete Transition Let (q, −→x ) be origin state. It is possible (but not necessary) to perform a transition (q, q′ ) ∈ E, if transition guard is valid, i.e. −→x ∈ G(q, q′ ). If the transition is taken, the continuous part of the state is updated accordingly: −→ x′ := R((q, q′ ), −→x ) The target state after a discrete transition is (q′, −→ x′ ). IA169 System Verification and Assurance – 11 str. 11/48 Reasonable restrictions of Hybrid Automata Restrictions in Continuous Part f (q, −→x ) is Lipschitz continuous for ∀q ∈ Q, (solution of differential equations is well defined) ∀e ∈ E we assume non-empty G(e) ∀e ∈ E and ∀x ∈ Q we assume non-empty R(e, x) Restrictions in Discrete Part The set of discrete state is finite. IA169 System Verification and Assurance – 11 str. 12/48 Example 2 – Water Tank System Description Two water tanks, volume of water denoted with x1 and x2. There is a constant speed leak from both tanks, v1 and v2. A hose can fill one of the tanks with speed w. The hose is always in exactly one of the tanks. IA169 System Verification and Assurance – 11 str. 13/48 Example 2 – Water Tank Goal Keep water level above the necessary minimum r1 and r2. Initially, there is enough water in both tanks. The hose is switched to a tank at the moment the water level in the tank drops to the required minimum. IA169 System Verification and Assurance – 11 str. 13/48 Water Tanks — Formal Definition of the System Q = {q1, q2} X = R × R f (q1, x) = w − v1 −v2 f (q2, x) = −v1 w − v2 IA169 System Verification and Assurance – 11 str. 14/48 Water Tanks — Formal Definition of the System Init = {q1, q2} × {x ∈ R × R | x1 ≥ r1 ∧ x2 ≥ r2} Dom(q1) = {x ∈ R × R | x2 ≥ r2} Dom(q2) = {x ∈ R × R | x1 ≥ r1} IA169 System Verification and Assurance – 11 str. 14/48 Water Tanks — Formal Definition of the System E = {(q1, q2), (q2, q1)} G(q1, q2) = {x ∈ R × R | x2 ≤ r2} G(q2, q1) = {x ∈ R × R | x1 ≤ r1} R(q1, q2, x) = R(q2, q1, x) = {x} IA169 System Verification and Assurance – 11 str. 14/48 Hybrid Time Sequence (HTS) Informally A run of hybrid automaton proceeds in a sequence of continuous time intervals. Discrete transitions happen on the boundaries of the intervals in instant time. The time characteristic of a run of hybrid automaton is formalised with the usage of the so called Hybrid Time Sequence. Definitions Hybrid Time Sequence is a (finite or infinite) sequence of intervals τ = {I0, I1, . . . , IN} = {Ii }N i=0 such that: Ii = [τi , τ′ i ] for all i < N If N < ∞ then either IN = [τN, τ′ N] or IN = [τN, τ′ N) τi ≤ τ′ i = τi+1 for all 0 ≤ i < N. IA169 System Verification and Assurance – 11 str. 15/48 Graphical Representation of Hybrid Time Sequence IA169 System Verification and Assurance – 11 str. 16/48 Ordering of Time Moments Observation If every time moment is related with an interval of HTS ... ... then time moments can be linearly ordered. Ordering ≺ t1 ∈ Ii , t2 ∈ Ij t1 ≺ t2 def = (t1 < t2) ∨ (t1 = t2 ∧ i < j) Generalisation Every hybrid time sequence is linearly ordered with ≺ relation. IA169 System Verification and Assurance – 11 str. 17/48 Ordering of Hybrid Time Sequence Prefix Of Hybrid Time Sequence τ = {Ii }N i=0 ˆτ = {ˆIi }M i=0 We say that τ is a prefix of ˆτ (denoted with τ ⊑ ˆτ), if τ = ˆτ, or N is finite ∧ IN ⊆ ˆIN ∧ ∀i ∈ [0, N) : Ii = ˆIi Proper Prefix τ ⊏ ˆτ ≡ τ ⊑ ˆτ ∧ τ = ˆτ Relation ⊑ is a Partial Ordering There exist τ and τ such that τ ⊑ τ and τ ⊑ τ. IA169 System Verification and Assurance – 11 str. 18/48 Task Task – Find τ, τ and τ such that τ ⊑ τ τ ⊑ τ τ ⊑ τ ∧ τ ⊑ τ Solution IA169 System Verification and Assurance – 11 str. 19/48 Hybrid Trajectories Definition Hybrid trajectory is a triple (τ, q, x), where τ is hybrid time sequence τ = {I}N 0 and q, x are two sequences of functions q = {qi }N 0 and x = {xi }N 0 such that qi : Ii → Q and xi : Ii → Rn, respectively. Intuition Continuous part flows within individual time intervals of hybrid time sequence. Discrete state within a single interval does not change. Discrete transitions realise transitions from the end of one interval to the beginning of the succeeding interval. IA169 System Verification and Assurance – 11 str. 20/48 Run of Hybrid Automaton Run of Hybrid Automaton Let H = (Q, X, f , Init, Dom, E, G, R) be hybrid automaton. Let (τ, q, x) be hybrid trajectory. Trajectory (τ, q, x) is a run of automaton H, if it is compliant with H in: initial condition, discrete behaviour and continuous behaviour. Initial Condition (q0(0), x0(0)) ∈ Init Discrete Behaviour – For all i < N it holds that (qi (τ′ i ), qi+1(τi+1)) ∈ E xi (τ′) ∈ G(qi (τ′ i ), qi+1(τi+1)) xi+1(τi+1) ∈ R(qi (τ′ i ), qi+1(τi+1), xi (τ′ i )) IA169 System Verification and Assurance – 11 str. 21/48 Run of Hybrid Automaton Run of Hybrid Automaton Let H = (Q, X, f , Init, Dom, E, G, R) be hybrid automaton. Let (τ, q, x) be hybrid trajectory. Trajectory (τ, q, x) is a run of automaton H, if it is compliant with H in: initial condition, discrete behaviour and continuous behaviour. Continuous Behaviour – For all i ≤ N it holds that qi : Ii → Q is constant over t ∈ Ii , xi : Ii → X is a solution to differential equation dxi (t) dt = f (qi (t), xi (t)) over Ii beginning in xi (τi ), For all t ∈ [τi , τ′ i ) it holds that xi (t) ∈ Dom(qi (t)). IA169 System Verification and Assurance – 11 str. 21/48 Water Tanks – Example Specification τ = {[0, 2], [2, 3], [3, 3.5]} Constants r1 = r2 = 0, v1 = v2 = 0.5, w = 0.75 Initial state q = q1, x1 = 0, x2 = 1. IA169 System Verification and Assurance – 11 str. 22/48 Water Tanks – Trajectories IA169 System Verification and Assurance – 11 str. 23/48 Classification of Runs (τ, q, x) Finite If τ is finite and the last interval of τ is closed. Infinite If τ is infinite sequence, or the sum of time intervals in τ is infinite, i.e. ΣN i=0(τ′ i − τi ) = ∞. Zeno If τ is infinite, but ΣN i=0(τ′ i − τi ) < ∞. Maximal If τ is no proper suffix of any other run τ′ of H. IA169 System Verification and Assurance – 11 str. 24/48 Classification of Runs τA finite; τC and τD infinite; τE and τF Zeno. What class is run τB? IA169 System Verification and Assurance – 11 str. 25/48 Examples of ZENO Runs IA169 System Verification and Assurance – 11 str. 26/48 Examples of ZENO Runs Let Then the following hybrid system has infinitely many intersections with x axis in the interval (−ǫ, 0]. IA169 System Verification and Assurance – 11 str. 27/48 Modelling Hybrid Systems Observation Hybrid automata are meant to describe real hybrid systems. Due to abstraction and simplification, it is possible to specify unrealistic situation. Risk of Modelling Can create system that have no solutions. Can create system that have only unrealistic solutions. Can create system that have non-deterministic solutions. Terminology System that has no solution (no run exist) is called blocking system. IA169 System Verification and Assurance – 11 str. 28/48 Unrealistic Runs Observation Non-blocking system does not guarantee that some runs are realistic. Non-blocking system does not guarantee that some runs are time divergent. Unrealistic Runs Runs that perform infinitely many discrete transitions in finite time are called ZENO runs. Created by abstraction and simplification in modelling. Discussion Why the ball does not bounce forever? It is important to see which simplification lead to ZENO runs. IA169 System Verification and Assurance – 11 str. 29/48 Non-determinism Non-determinism In general can be described as absence of unique solutions, i.e. that a hybrid automaton accepts multiple different runs emanating from the same initial conditions. When limited to Lipschitz continuous functions with unique solution, reason for non-determinism comes from discrete transitions. Non-deterministic on Purpose Can be used to model uncertainty. Modeller should make difference between non-determinism due to simplification, and non-determinism used on purpose. Observation Non-determinism is a real cause of troubles in both analysis and controller synthesis of hybrid systems. IA169 System Verification and Assurance – 11 str. 30/48 Problems of Simulations and Analysis of Hybrid Systems Existence of Solution How to detect existence of non-blocking run? How to detect ZENO behaviour? Uniqueness How to perform simulation of non-deterministic system? Discrete transition vs. continuous time evolution. Discrete transition vs. discrete transition. As-soon-as semantics. Discontinuity How to detect satisfiability of transition guards? What if state invariant ends with open interval [a, b) and the succeeding transition is allowed to execute at time [b]? Composition How to compose hybrid automata? IA169 System Verification and Assurance – 11 str. 31/48 Non-blocking and Deterministic Hybrid Automaton Non-blocking Hybrid Automaton Hybrid automaton H is called non-blocking if for all initial states (ˆq, ˆx) ∈ Init there exist an infinite run emanating from (ˆq, ˆx). Deterministic Hybrid Automaton Hybrid automaton H is called deterministic, if for all initial states (ˆq, ˆx) ∈ Init there exist at most one maximal run emanating from (ˆq, ˆx). IA169 System Verification and Assurance – 11 str. 32/48 Section Using Hybrid Automata IA169 System Verification and Assurance – 11 str. 33/48 Analysis and Synthesis Hybrid Systems (HS) Motivation for Modelling The goal of modelling of HS is to deduce properties of, or synthesise controllers for real HS from properties of, or controllers for modelled HS. Verification Does hybrid system exhibits declared behaviour (does it satisfy specification)? Synthesis There are number of choices to build a HS, using models it is possible to decide which choices are good and which are bad prior the construction of the real HS. IA169 System Verification and Assurance – 11 str. 34/48 Validation Validation Check that the design described as a hybrid automaton and the real product produced behave accordingly. Some system modelled with hybrid automata may be unrealistic (and cannot be built) due to simplifications and abstractions used during modelling phase. Usual Work-flow Synthesis (of model) Verification (of model) Validation (equivalence of model and real product) IA169 System Verification and Assurance – 11 str. 35/48 Specification Stability Typical property of purely continuous systems. To request stability for hybrid systems requires to specify what does the stability means with respect to the discrete part of the system. Specification by Set of States Specification of safety and forbidden areas. Specification by Set of Trajectories Properties of hybrid systems that can be expressed as properties of runs. Set of allowed runs of a hybrid automaton. Formally described using modal and temporal logic, such as (CTL, LTL, CTL∗). IA169 System Verification and Assurance – 11 str. 36/48 Methods of Analysis of HS Deductive Methods Using math reasoning, such as math induction, to deduce properties of hybrid systems. Can be automated. Model Checking Algorithmic procedure for deciding formally specified properties of hybrid systems. Decidable only for limited sub-classes of hybrid automata. Simulations Used to estimate the set of reachable states. The precision of estimation is difficult to say. IA169 System Verification and Assurance – 11 str. 37/48 Deductive Methods – Invariant Set Typical Goal Typical goal for deductive methods is to set boundaries of the reach set using the so called Invariant Set. Invariant set is a set of states for which it holds that if a run of hybrid system is initiated at the state of the set it only visits states that are in the set (i.e. never leaves invariant set). Formal Definition of Invariant Set Set of state M ⊆ Q × X of hybrid automaton H is called invariant if for all (ˆq, ˆx) ∈ M, all solutions (τ, q, x) starting from (ˆq, ˆx), all Ii ∈ τ and all t ∈ Ii it holds that (qi (t), xi (t)) ∈ M. IA169 System Verification and Assurance – 11 str. 38/48 Deductive Methods – Properties of Invariant Set Observation Union and Intersection of Invariant Sets of hybrid automaton H is also an invariant set for H. If M is an invariant set and Init ⊆ M, then Reach ⊆ M. Consequence To approximate the Reach set it is possible to deduce a number of invariant sets that contain initial state and are at the same time below the set of all states of hybrid automaton (here denoted by F) Init ⊆ M ⊆ F and intersect them. IA169 System Verification and Assurance – 11 str. 39/48 Model Checking Simplification For hybrid automata we restrict ourselves in the course to algorithmic test of reachability of a given state. Considered Sub-classes of Hybrid Automata Timed Automata (TA). Rectangular Hybrid Automata (RHA). Linear Hybrid Automata (LHA). Software Tools UPPAAL – Timed Automata PHaVer – RHA, partially LHA (HyTech) IA169 System Verification and Assurance – 11 str. 40/48 Timed Automata Restriction All derivations to drive continuous evolution of the automaton has the form of: dxi (t) dt = 1 Resets R of discrete transitions are allowed either to keep the value of the continuous variable, or to reset it to 0. Dom and G are defined only using relations ≤ and ≥ with respect to integral values. Intuition Finite automaton with a set of continuous variables to measure elapsed time. Measured time values may be reset to 0 using discrete transition. IA169 System Verification and Assurance – 11 str. 41/48 Example of Timed Automaton Example of Timed Automaton Exercise In two-dimensional graph with axes x1 and x2 show how the values of continuous variables change. IA169 System Verification and Assurance – 11 str. 42/48 Region Abstraction Key Observation With respect to the restriction that comparisons are made only against integral values, two floating point values that have the same integral part cannot be differentiated. Equivalence Classes on the Continuous Domain If c is the greatest integral number used in a guard of timed automaton then the continuous domain can be represented with a finite set of intervals as follows: [0], (0, 1), [1], (1, 2), [2], . . . [c − 1], (c − 1, c), [c], (c, ∞) Abstracted domain is finite for every continuous variable. It is possible to construct finite-state automaton that faithfully simulates behaviour of the timed automaton. This can be used for verification purposes. IA169 System Verification and Assurance – 11 str. 43/48 Region Abstraction IA169 System Verification and Assurance – 11 str. 44/48 Rectangular Hybrid Automata (RHA) Restriction All derivations to drive continuous evolution of the automaton has the form of: a ≤ dxi (t) dt ≤ b, where a and b are rational constants. When specifying RHA no derivation equations are given, just the boundary constants a and b. Exercise Consider a RHA with two continuous variables x1 and x2. On two-dimensional graph with axes x1 and x2 show the evolution of values of the continuous variables. Guess the origin of the name of this particular sub-class of hybrid automata. IA169 System Verification and Assurance – 11 str. 45/48 Reachability is Decidable for RHA Reachability Reachability problem for RHA is decidable if there are only finitely many values to which a continuous variable may be reset by a discrete transition. The most general sub-class of hybrid automata for which reachability is still decidable. Going Beyond Means Undecidability Relaxation from restriction of resets is known to result in sub-class of hybrid automata for which the reachability problem is undecidable. IA169 System Verification and Assurance – 11 str. 46/48 Linear Hybrid Automata (LHA) Definition Let k0, . . . , km be numeric constants and x1, . . . , xm variables. An expression in the form of k0 + k1x1 + k2x2 + · · · + kmxm is called a linear expression. Let t1, t2 be linear expressions. An expression of the form t1 ≤ t2 is called linear inequality. Hybrid automaton H is called linear hybrid automaton (LHA), if Init, Dom, G and f are defined as Boolean combinations of linear inequalities. Undecidability The reachability problem for LHA is undecidable. Algorithms implemented for the LHA sub-class are incomplete (HyTech). IA169 System Verification and Assurance – 11 str. 47/48 Practicals and Homework Practicals Modelling with timed automata. UPPAAL model checker. Follow the UPPAAL tutorial (http://www.it.uu.se/research/group/darts/papers/ texts/new-tutorial.pdf) Homework Will Lake Mead go dry? (SPACEex tool). http://spaceex.imag.fr/documentation/tutorials IA169 System Verification and Assurance – 11 str. 48/48 IA169 System Verification and Assurance Verification of Systems with Probabilities Vojtěch Řehák Motivation example Fail-repair system idle working done repair error start end bug service ok reset What are the properties of the model? G(working =⇒ F done) G(working =⇒ F error) FG(working ∨ error ∨ repair) IA169 System Verification and Assurance – 12 2/31 Motivation example Fail-repair system idle working done repair error start end bug service ok reset What are the properties of the model? G(working =⇒ F done) NO G(working =⇒ F error) FG(working ∨ error ∨ repair) IA169 System Verification and Assurance – 12 2/31 Motivation example Fail-repair system idle working done repair error start end bug service ok reset What are the properties of the model? G(working =⇒ F done) NO G(working =⇒ F error) NO FG(working ∨ error ∨ repair) IA169 System Verification and Assurance – 12 2/31 Motivation example Fail-repair system idle working done repair error start end bug service ok reset What are the properties of the model? G(working =⇒ F done) NO G(working =⇒ F error) NO FG(working ∨ error ∨ repair) NO IA169 System Verification and Assurance – 12 2/31 Motivation example Fail-repair system idle working done repair error start 0.95 end bug 0.05 service ok reset IA169 System Verification and Assurance – 12 3/31 Motivation example Fail-repair system idle working done repair error start 0.95 end bug 0.05 service ok reset What is the probability of reaching “done” from “working” with no visit of “error”? What is the probability of reaching “done” from “working” with at most one visit of “error”? What is the probability of reaching “done” from “working”? IA169 System Verification and Assurance – 12 3/31 Section Discrete-time Markov Chains (DTMC) IA169 System Verification and Assurance – 12 4/31 Probabilistic models Discrete-time Markov Chains (DTMC) Standard model for probabilistic systems. State-based model with probabilities on branching. Based on the current state, the succeeding state is given by a discrete probability distribution. Markov property (“memorylessness”) — only the current state determines the successors (the past states are irrelevant). Probabilities on outgoing edges sums to 1 for each state. Hence, each state has at least one outgoing edge (“no deadlock”). IA169 System Verification and Assurance – 12 5/31 DTMC examples Model of a queue 0 1 2 3 4 1/3 1/3 1/3 1/3 2/32/32/32/3 2/3 1/3 Queue for at most 4 items. In every time tick, a new item comes with probability 1/3 and an item is consumed with probability 2/3. IA169 System Verification and Assurance – 12 6/31 DTMC examples Model of a queue 0 1 2 3 4 1/3 1/3 1/3 1/3 2/32/32/32/3 2/3 1/3 Queue for at most 4 items. In every time tick, a new item comes with probability 1/3 and an item is consumed with probability 2/3. What if a new items comes with probability p = 1/2 and an item is consumed with probability q = 2/3? IA169 System Verification and Assurance – 12 6/31 DTMC examples Model of the new queue 0 1 2 3 4 p p(1 − q) p(1 − q) p(1 − q) qq(1 − p)q(1 − p)q(1 − p) 1 − p 1 − q(1 − p)(1 − q) (1 − p)(1 − q) (1 − p)(1 − q) IA169 System Verification and Assurance – 12 7/31 DTMC - formal definition Discrete-time Markov Chain is given by a set of states S, an initial state s0 of S, a probability matrix P : S × S → [0, 1], and an interpretation of atomic propositions I : S → AP. IA169 System Verification and Assurance – 12 8/31 DTMC - formal definition Discrete-time Markov Chain is given by a set of states S, an initial state s0 of S, a probability matrix P : S × S → [0, 1], and an interpretation of atomic propositions I : S → AP. 1 2 5 4 3 1 0.95 0.05 1 1 1 P =       0 1 0 0 0 0 0 0.05 0 0.95 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1       IA169 System Verification and Assurance – 12 8/31 Back to our questions Fail-Repair System idle working done repair error 1 0.95 0.05 1 1 1 What is the probability of reaching “done” from “working” with no visit of “error”? What is the probability of reaching “done” from “working” with at most one visit of “error”? What is the probability of reaching “done” from “working”? IA169 System Verification and Assurance – 12 9/31 Markov chain analysis Transient analysis distribution after k-steps reaching/hitting probability hitting time Long run analysis probability of infinite hitting stationary (invariant) distribution mean inter visit time long run limit distribution IA169 System Verification and Assurance – 12 10/31 Section Property Specification IA169 System Verification and Assurance – 12 11/31 Property specification languages Recall some non-probabilistic specification languages: LTL formulae ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | X ϕ | ϕ U ϕ CTL formulae ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | EG ϕ Syntax of CTL∗ state formula ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | E ψ path formula ψ ::= ϕ | ¬ψ | ψ ∨ ψ | X ψ | ψ U ψ IA169 System Verification and Assurance – 12 12/31 Property specification languages We need to quantify probability that a certain behaviour will occur. Probabilistic Computation Tree Logic (PCTL) Syntax of PCTL state formula ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | P⊲⊳bψ path formula ψ ::= X ϕ | ϕ U ϕ | ϕ U≤k ϕ where b ∈ [0, 1] is a probability bound, ⊲⊳∈ {≤, <, ≥, >}, and k ∈ N is a bound on the number of steps. IA169 System Verification and Assurance – 12 13/31 Property specification languages We need to quantify probability that a certain behaviour will occur. Probabilistic Computation Tree Logic (PCTL) Syntax of PCTL state formula ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | P⊲⊳bψ path formula ψ ::= X ϕ | ϕ U ϕ | ϕ U≤k ϕ where b ∈ [0, 1] is a probability bound, ⊲⊳∈ {≤, <, ≥, >}, and k ∈ N is a bound on the number of steps. A PCTL formula is always a state formula. α U≤k β is a bounded until saying that α holds until β within k steps. For k = 3 it is equivalent to β ∨ (α ∧ X β) ∨ (α ∧ X (β ∨ α ∧ X β)). Some tools also supports P=?ψ asking for the probability that the specified behaviour will occur. IA169 System Verification and Assurance – 12 13/31 PCTL examples We can also use derived operators like G, F, ∧, ⇒, etc. idle working done repair error 1 0.95 0.05 1 1 1 Probabilistic reachability P≥1( F done ) probability of reaching the state done is equal to 1 Probabilistic bounded reachability P>0.99( F≤6 done ) probability of reaching the state done in at most 6 steps is > 0.99 Probabilistic until P<0.96( (¬error) U (done) ) probability of reaching done with no visit of error is less than 0.96 IA169 System Verification and Assurance – 12 14/31 Qualitative vs. quantitative properties Qualitative PCTL properties P⊲⊳b ψ where b is either 0 or 1 Quantitative PCTL properties P⊲⊳b ψ where b is in (0, 1) IA169 System Verification and Assurance – 12 15/31 Qualitative vs. quantitative properties Qualitative PCTL properties P⊲⊳b ψ where b is either 0 or 1 Quantitative PCTL properties P⊲⊳b ψ where b is in (0, 1) In DTMC where zero probability edges are erased, it holds that P>0( X ϕ) is equivalent to EX ϕ there is a next state satisfying ϕ P≥1( X ϕ) is equivalent to AX ϕ the next states satisfy ϕ P>0( F ϕ) is equivalent to EF ϕ there exists a finite path to a state satisfying ϕ but P≥1( F ϕ) is not equivalent to AF ϕ IA169 System Verification and Assurance – 12 15/31 Qualitative vs. quantitative properties Qualitative PCTL properties P⊲⊳b ψ where b is either 0 or 1 Quantitative PCTL properties P⊲⊳b ψ where b is in (0, 1) In DTMC where zero probability edges are erased, it holds that P>0( X ϕ) is equivalent to EX ϕ there is a next state satisfying ϕ P≥1( X ϕ) is equivalent to AX ϕ the next states satisfy ϕ P>0( F ϕ) is equivalent to EF ϕ there exists a finite path to a state satisfying ϕ but P≥1( F ϕ) is not equivalent to AF ϕ There is no CTL formula equivalent to P≥1( F ϕ), and no PCTL formula equivalent to AF ϕ. IA169 System Verification and Assurance – 12 15/31 How the transient probabilities are computed? 1 2 5 4 3 1 0.95 0.05 1 1 1 P =        0 1 0 0 0 0 0 0.05 0 0.95 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1        Probability in the k-th state when starting in 1 IA169 System Verification and Assurance – 12 16/31 How the transient probabilities are computed? 1 2 5 4 3 1 0.95 0.05 1 1 1 P =        0 1 0 0 0 0 0 0.05 0 0.95 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1        Probability in the k-th state when starting in 1 1 0 0 0 0 × P = 0 1 0 0 0 IA169 System Verification and Assurance – 12 16/31 How the transient probabilities are computed? 1 2 5 4 3 1 0.95 0.05 1 1 1 P =        0 1 0 0 0 0 0 0.05 0 0.95 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1        Probability in the k-th state when starting in 1 1 0 0 0 0 × P = 0 1 0 0 0 1 0 0 0 0 × P2 = 0 0 0.05 0 0.95 IA169 System Verification and Assurance – 12 16/31 How the transient probabilities are computed? 1 2 5 4 3 1 0.95 0.05 1 1 1 P =        0 1 0 0 0 0 0 0.05 0 0.95 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1        Probability in the k-th state when starting in 1 1 0 0 0 0 × P = 0 1 0 0 0 1 0 0 0 0 × P2 = 0 0 0.05 0 0.95 1 0 0 0 0 × P3 = 0 0 0 0.05 0.95 IA169 System Verification and Assurance – 12 16/31 How the transient probabilities are computed? 1 2 5 4 3 1 0.95 0.05 1 1 1 P =        0 1 0 0 0 0 0 0.05 0 0.95 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1        Probability in the k-th state when starting in 1 1 0 0 0 0 × P = 0 1 0 0 0 1 0 0 0 0 × P2 = 0 0 0.05 0 0.95 1 0 0 0 0 × P3 = 0 0 0 0.05 0.95 1 0 0 0 0 × P4 = 0 0.05 0 0 0.95 IA169 System Verification and Assurance – 12 16/31 How the transient probabilities are computed? 1 2 5 4 3 1 0.95 0.05 1 1 1 P =        0 1 0 0 0 0 0 0.05 0 0.95 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1        Probability in the k-th state when starting in 1 1 0 0 0 0 × P = 0 1 0 0 0 1 0 0 0 0 × P2 = 0 0 0.05 0 0.95 1 0 0 0 0 × P3 = 0 0 0 0.05 0.95 1 0 0 0 0 × P4 = 0 0.05 0 0 0.95 1 0 0 0 0 × P5 = 0 0 0.0025 0 0.9975 IA169 System Verification and Assurance – 12 16/31 How the transient probabilities are computed? 1 2 5 4 3 1 0.95 0.05 1 1 1 P =        0 1 0 0 0 0 0 0.05 0 0.95 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1        Probability of being in 5 or 2 in the k-th state IA169 System Verification and Assurance – 12 17/31 How the transient probabilities are computed? 1 2 5 4 3 1 0.95 0.05 1 1 1 P =        0 1 0 0 0 0 0 0.05 0 0.95 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1        Probability of being in 5 or 2 in the k-th state P × 0 1 0 0 1 T = 1 0.95 0 1 1 T P2 × 0 1 0 0 1 T = 0.95 0.95 1 0.95 1 T P3 × 0 1 0 0 1 T = 0.95 1 0.95 0.95 1 T P4 × 0 1 0 0 1 T = 1 0.9975 0.95 1 1 T P5 × 0 1 0 0 1 T = 0.9975 0.9975 1 0.9975 1 T IA169 System Verification and Assurance – 12 17/31 Unbounded reachability - optional slide Unbounded reachability Let p(s, A) be the probability of reaching a state in A from s. It holds that: p(s, A) = 1 for s ∈ A p(s, A) = s′∈succ(s) P(s, s′) ∗ p(s′, A) for s ∈ A where succ(s) is a set of successors of s and P(s, s′) is the probability on the edge from s to s′. Theorem The minimal non-negative solution of the above equations equals to the probability of unbounded reachability. IA169 System Verification and Assurance – 12 18/31 Section Long Run Analysis IA169 System Verification and Assurance – 12 19/31 Long run analysis 1 2 5 4 3 1 0.95 0.05 1 1 1 Recall that we reach the state 5(done) with probability 1. IA169 System Verification and Assurance – 12 20/31 Long run analysis 1 2 5 4 3 1 0.95 0.05 1 1 1 Recall that we reach the state 5(done) with probability 1. 1 2 5 4 3 1 0.95 0.05 1 1 0.5 0.5 What are the states visited infinitely often with probability 1? IA169 System Verification and Assurance – 12 20/31 Transient and recurrent states Definitions A state of DMTC is called transient iff there is a positive probability that the system will not return back to this state. A state s of DMTC is called recurrent iff, starting from s, the system eventually returns back to the s with probability 1. Theorem Every transient state is visited finitely many times with probability 1. Each recurrent state is with probability 1 either not visited or visited infinitely many times.1 1 This holds only in DTMC models with finitely many states. IA169 System Verification and Assurance – 12 21/31 Transient vs. recurrent states Which states are transient? Which states are recurrent? 1 This holds only in DTMC models with finitely many states. IA169 System Verification and Assurance – 12 22/31 Transient vs. recurrent states Which states are transient? Which states are recurrent? Decompose the graph representation onto strongly connected components. 1 This holds only in DTMC models with finitely many states. IA169 System Verification and Assurance – 12 22/31 Transient vs. recurrent states Which states are transient? Which states are recurrent? Decompose the graph representation onto strongly connected components. Theorem 1 A state is recurrent if and only if it is in a bottom strongly connected component. All other states are transient. 1 This holds only in DTMC models with finitely many states. IA169 System Verification and Assurance – 12 22/31 Irreducible Markov Chain For the sake of infinite behaviour, we will concentrate on bottom strongly connected components only. Definition A Markov chain is said to be irreducible if every state can be reached from every other state in a finite number of steps. Theorem A Markov chain is irreducible if and only if its graph representation is a single strongly connected component. Corollary All states of a finite irreducible Markov chain are recurrent. IA169 System Verification and Assurance – 12 23/31 Stationary (Invariant) Distribution Definition Let P be the transition matrix of a DTMC and λ be a probability distribution on its states. If λP = λ, then λ is a stationary (or steady-state or invariant or equilibrium) distribution of the DTMC. Question: How many stationary distributions can a Markov chain have? Can it be more than one? Can it be none? IA169 System Verification and Assurance – 12 24/31 Stationary Distributions Answer: It can be more that one. For example, in the Drunkard’s walk 1 2 3 4 1/2 1/2 1 1 1/2 1/2 both (1, 0, 0, 0) and (0, 0, 0, 1) are stationary distributions. IA169 System Verification and Assurance – 12 25/31 Stationary Distributions Answer: It can be more that one. For example, in the Drunkard’s walk 1 2 3 4 1/2 1/2 1 1 1/2 1/2 both (1, 0, 0, 0) and (0, 0, 0, 1) are stationary distributions. But, this is not an irreducible Markov chain. IA169 System Verification and Assurance – 12 25/31 Stationary Distributions Theorem In every finite irreducible DTMC there is a unique invariant distribution. IA169 System Verification and Assurance – 12 26/31 Stationary Distributions Theorem In every finite irreducible DTMC there is a unique invariant distribution. Q: Can it be none? IA169 System Verification and Assurance – 12 26/31 Stationary Distributions Theorem In every finite irreducible DTMC there is a unique invariant distribution. Q: Can it be none? Theorem For each finite DTMC, there is an invariant distribution. IA169 System Verification and Assurance – 12 26/31 Stationary Distributions Theorem In every finite irreducible DTMC there is a unique invariant distribution. Q: Can it be none? Theorem For each finite DTMC, there is an invariant distribution. Q: How can we compute the invariant distribution of a finite irreducible Markov chain? IA169 System Verification and Assurance – 12 26/31 Stationary Distribution & Cut-sets Again, we can construct a set of equations that express the result. Theorem Let P be a transition matrix of a finite irreducible DTMC and π = (π1, π2, . . . , πn) be a stationary distribution corresponding to P. For any state i of the DTMC, we have j=i πjPj,i = j=i πi Pi,j. IA169 System Verification and Assurance – 12 27/31 Mean Portion of Visited States and Inter Visit Time Theorem Let us have a finite irreducible DTMC and the unique stationary distribution π. It holds that πi = limn→∞E( # of visits of state i during the first n steps)/n. Let us have a finite irreducible DTMC and the unique stationary distribution π. It holds that πi = 1/mi where mi is the mean inter visit time of state i. IA169 System Verification and Assurance – 12 28/31 Aperiodic Markov Chains For example: aperiodic periodic Definition A state s is periodic if there exists an integer ∆ > 1 such that length of every path from s to s is divisible by ∆. A Markov chain is periodic if any state in the chain is periodic. A state or chain that is not periodic is aperiodic. IA169 System Verification and Assurance – 12 29/31 Aperiodic Markov Chains Theorem Let us have a finite aperiodic irreducible DTMC and the unique stationary distribution π. It holds that π = limn→∞λPn where λ is an arbitrary distribution on states. Q: What this is good for? IA169 System Verification and Assurance – 12 30/31 DTMC Extensions - Communication and Nondeterminism Last remark on some DTMC extensions. Modules and synchronisation modules actions rewards Decision extension Markov Decision Processes (MDP) Pmin and Pmax properties IA169 System Verification and Assurance – 12 31/31 Information technology security evaluation – standards, assurance IA169 – System verification and assurance Ji í Barnat, Vojtěch ehák, Vashek Matyáš Course coverage • assurance, threat models, relevant security standards, • testing, simulations, advance testing, symbolic execution, • abstract interpretation, static analysis, theorem proving, • automated formal verification & introduction to model-based verification • concrete software verification tools for analysis of sequential and concurrent systems, real-time systems, and systems with probabilities. 2 IA169 Position within other courses • PA193 – Secure coding principles and practices – Very useful • PA018 – Advanced Topics in IT Security – No strict dependence • IA159 – Formal Verification Methods – Useful follow-up 3 IA169 Course topics I • Need for verification in the security area – Common Criteria, FIPS 140-2, threat models, assurance • Introduction to formal verification and testing • Deductive verification • LTL (Linear Temporal Logic) Model Checking • CTL (Computation Tree Logic ) Model Checking • Symbolic execution 4 IA169 Course topics II • Bounded Model Checking • CEGAR and Abstract Interpretation • Verification of Real-Time and Hybrid systems • Verification of systems with probabilities 5 IA169 Course structure, credits • 2/2/2 credits, +2 for the final exam – Lecture: 2 hours weekly – Seminar: 2 hours weekly – Homework: 5+ hours weekly (on average) 6 IA169 Course marking • Final exam: 70% • Assignments: 30% • Marking scheme: A for 90% or higher, then B for 80% or higher, then C for 70% or higher, then D for 60% or higher, then E for 50% or higher, then F(ail) for less than 50%. Colloquy or credit – at least 44%. 7 IA169 Resources used – first lecture • Common Criteria for Information Technology Security Evaluation, v 3.4, rev. 4, Sep 2012 – http://www.commoncriteriaportal.org/ • Separation Kernel Protection Profile Revisited: Choices and Rationale, T.E. Levin et al., 4th Annual Layered Assurance Workshop, 2010 • Common Criteria Certification in the UK – UK IT security evaluation & certification scheme, CESG • Understanding the Windows EAL4 evaluation, J.S. Shapiro, IEEE Computer 03/2003 • Security Requirements for Cryptographic Modules, FIPS PUB 140-2 – http://csrc.nist.gov/publications/fips/fips140-2/fips1402.pdf 8 IA169 Security threat model • Two views: 1) Description of security threats considered when designing a (security) solution/system. 2) Definition of (all) possible threats to consider. • Usual security notion: – Assets to be protected – Vulnerabilities of assets and relevant systems – Threats exploiting the vulnerabilities – Countermeasures (aim to) mitigate the threats 9 IA169 Threat modelling – approaches • Attacker centric – Popular in the research community (following two slides) • System centric (a.k.a. design/SW centric) – Taking over in the past decade or so, e.g. used in the Microsoft Security Development Lifecycle • Asset centric – Business logic • Defender/owner view getting more prominent 10 IA169 Attacker models – Needham & Schroeder • attacker can eavesdrop and interfere all communication – record/modify/replay/inject messages • node internal processes are safe – secret keys, encryption process, … • Comms security classics, paper from 1978 – paper Using encryption for authentication in large networks of computers, ACM Communications 11 IA169 Attacker models – Dolev & Yao • Network = set of abstract machines exchanging messages. • Message = formal terms. Terms reveal some of the message internal structure to the adversary, but not all. • Adversary can overhear, intercept, and synthesize any message, is limited by the constraints of the cryptographic methods used. – Sometimes put as “the attacker carries the message.” • Paper “On the security of public key protocols”, IEEE Trans. on Information Theory, 1983 12 IA169 Trusted system/product • Such one that behaves in a way we expect it to behave • Can be trusted to only such a functionality that adheres to the relevant security policy • Trust – Belief that (a system…) satisfies given (security) requirements and specifications – Chance that (a system…) can breach the (security) policy without leaving any trace of evidence  13 IA169 Common Criteria 14 IA169 • Interests of users, manufacturers, evaluators • Target of evaluation (TOE) – what is (to be) evaluated • Protection profile (PP) (smartcards, biometrics, etc.) – Catalogued as a self-standing evaluation document • Security target (ST) – theoretical concept/aim • Security Functional Requirements (SFRs) – individual security functions provided by the TOE • Evaluation of TOE – is the reality corresponding to theory (ST)? Common Criteria model • TOE: Target of Evaluation – the evaluated system • TSF: TOE Security Functions – HW, SW, FW used by the TOE • TSC: TSF Scope of Control – interactions under the TOE security policy 15 IA169 Common Criteria – two catalogues • Two catalogues of components for specification of assurance and functionality requirements, with a standard terminology. • Functionality – rules governing access to & use of TOE resources, and thus information and services controlled by the TOE • Assurance – grounds for confidence that an entity meets its security objectives (CC v2.3) – grounds for confidence that a TOE meets the SFRs (CC v3.1) 16 IA169 Assurance is not robustness • Assurance – grounds for confidence that an entity meets its security objectives (CC v2.3) – grounds for confidence that a TOE meets the SFRs (CC v3.1) • Robustness – characterization of the strength of a security function, mechanism, service or solution, and the assurance (or confidence) that it is implemented and functioning correctly (US DoD definition) 17 IA169 CC evaluation in a nutshell 1. Define the product/system for evaluation 2. Specify its functionality 3. Specify the assurance level claimed 4. See details of evaluation with a certification body 5. Prepare evidence 18 IA169 CC: Functional & Assurance Requirements Security Functional Requirements (SFRs) • The core – CC is in a major part a catalogue of security functions • Same product with different ST => different SFRs • Correctness of one function can depend on another function Security Assurance Requirements (SARs) • Measures taken to assure compliance with the claimed functionality • Design, development, evaluation/verification • CC provides a catalogue of SARs 19 IA169 CC functional classes • FAU: SECURITY AUDIT • FCO: COMMUNICATION • FCS: CRYPTOGRAPHIC SUPPORT • FDP: USER DATA PROTECTION • FIA: IDENTIFICATION AND AUTHENTICATION • FMT: SECURITY MANAGEMENT • FPR: PRIVACY • FPT: PROTECTION OF THE TSF • FRU: RESOURCE UTILISATION • FTA: TOE ACCESS • FTP: TRUSTED PATH/CHANNELS 20 IA169 CC assurance classes • APE: PROTECTION PROFILE EVALUATION • ASE: SECURITY TARGET EVALUATION • ADV: DEVELOPMENT • AGD: GUIDANCE DOCUMENTS • ALC: LIFE-CYCLE SUPPORT • ATE: TESTS • AVA: VULNERABILITY ASSESSMENT • ACO: COMPOSITION 21 IA169 CC assurance paradigms • assurance based upon an evaluation (active investigation) • measuring the validity of the documentation and of the resulting IT product by expert evaluators with increasing emphasis on scope, depth, and rigour • CC does not exclude, nor does it comment upon, the relative merits of other means of gaining assurance 22 IA169 Assurance through evaluation I a) analysis and checking of process(es) and procedure(s); b) checking that process(es) and procedure(s) are being applied; c) analysis of the correspondence between TOE design representations; d) analysis of the TOE design representation against the requirements; e) verification of proofs; 23 IA169 Assurance through evaluation II f) analysis of guidance documents; g) analysis of functional tests developed and the results provided; h) independent functional testing; i) analysis for vulnerabilities (including flaw hypothesis); j) penetration testing. 24 IA169 CC evaluation assurance scale The increasing level of effort is based upon: a) scope – the effort is greater because a larger portion of the IT product is included; b) depth – the effort is greater because it is deployed to a finer level of design and implementation detail; c) rigour – the effort is greater because it is applied in a more structured, formal manner. 25 IA169 CC – assurance hierarchy & component structure 26 IA169 Assurance elements – 3 exclusive classes 1. Developer action elements: activities that shall be performed by the developer. Further qualified by evidential material referenced in the following set of elements. Req’s marked by “D” at the element No. 2. Content and presentation of evidence elements: the evidence required, what the evidence demonstrates, what the evidence shall convey. Marked by “C”. 3. Evaluator action elements: activities that shall be performed by the evaluator. Marked by “E”. 27 IA169 28 IA169 29 IA169 7 evaluation assurance levels (EALs) • Hierarchical system – higher or new components – bold faced text in the description for the added components • The following slides present first the EALs in the language of the CC and then from a practical perspective. 30 IA169 EAL1 – functionally tested • some confidence in correct operation is required, but the threats to security are not viewed as serious – sufficient to simply state the SFRs that the TOE must meet, rather than deriving them from threats, etc. through security objectives; – analysis is supported by a search for potential vulnerabilities in the public domain and independent testing (functional and penetration) of the TSF; – This EAL provides a meaningful increase in assurance over unevaluated IT. 31 IA169 EAL2 – structurally tested • assurance by a full security target (with given SFRs); • analysis of the SFRs, using functional and interface specs, guidance documentation and basic TOE architecture description to understand the security behaviour; • configuration management system and evidence of secure delivery procedures; • independent confirmation of the developer test results, vulnerability analysis (based upon the above in italics) demonstrating resistance to penetration attackers with a basic attack potential. 32 IA169 EAL3 – methodically tested and checked • architectural description of the TOE design; • development environment controls • improved testing coverage of the security functionality and mechanisms and/or procedures that provide some confidence that the TOE was not tampered with during development. 33 IA169 EAL4 – methodically designed, tested, and reviewed • complete interface specification, description of the basic modular design of the TOE, implementation representation for the entire TSF; • demonstrating resistance to penetration attackers with an Enhanced-Basic attack potential; • additional TOE configuration mgmt incl. automation; 34 IA169 EAL5 – semiformally designed and tested • modular TSF design; • comprehensive TOE configuration management; • semiformal design descriptions, a more structured (and hence analysable) architecture. 35 IA169 EAL6 – semiformally verified design and tested • formal model of select TOE security policies; • semiformal presentation of the functional specification and TOE design; • modular layered and simple TSF design; • structured development process, development environment controls, and comprehensive TOE configuration mgmt incl. complete automation; • more comprehensive analysis, more architectural structure (e.g. layering), more comprehensive independent vulnerability analysis. 36 IA169 EAL7 – formally verified design and tested • structured presentation of the implementation; • implementation representation, complete independent confirmation of the developer test results; • comprehensive analysis using formal representations and formal correspondence, and comprehensive testing. 37 IA169 CC certified products by country & EAL 38 IA169 EAL1 – functionally tested • analysis supported by independent testing of a sample of the security functions; • applicable where confidence in correct operation is required but the security threat assessment is low. • This EAL is particularly suitable for legacy systems as it should be achievable without the assistance of the developer. 39 IA169 EAL2 – structurally tested • analysis exercises a functional and interface specification and the high-level design of the subsystems of the TOE; • independent testing of the security functions; • evidence required of developer 'black box' testing and development search for obvious vulnerabilities. • EAL2 is applicable where a low to moderate level of independently assured security is required. 40 IA169 EAL3 – methodically tested and checked • analysis supported by 'grey box' testing, selective independent confirmation of the developer test results and evidence of a developer search for obvious vulnerabilities; • development environment controls and TOE configuration management are also required. • EAL3 for a moderate level of independently assured security, with a thorough investigation of the TOE and its development, without incurring substantial reengineering costs. 41 IA169 EAL4 – methodically designed, tested, and reviewed • analysis supported by the low-level design of TOE modules and a subset of the implementation; • testing supported by an independent search for obvious vulnerabilities; • development controls supported by a life-cycle model, identification of tools and automated configuration management. • EAL4 for a moderate to high level security, where some additional security-specific engineering costs may be incurred. 42 IA169 EAL5 – semiformally designed and tested • analysis includes all of the implementation; • supplemented by a formal model, a semiformal presentation of the functional specification and high level design and a semiformal demonstration of correspondence; • search for vulnerabilities must ensure resistance to penetration attackers with a moderate attack potential; • covert channel analysis and modular design required. • EAL5 for a high level of security in a planned development coupled with a rigorous development approach. 43 IA169 EAL6 – semiformally verified design and tested • analysis supported by a modular approach to design and a structured presentation of the implementation; • independent search for vulnerabilities must ensure resistance to penetration attackers with a high attack potential; • a systematic search for covert channels; • EAL6 where a specialised security TOE is required for high risk situations. 44 IA169 EAL7 – formally verified design and tested • the formal model is supplemented by a formal presentation of the functional specification and high level design, showing correspondence; • evidence of developer 'white box‘ testing and complete independent confirmation of developer test results. • EAL7 where a specialised security TOE is required for extremely high risk situations. 45 IA169 CC certified products by country & EAL 46 IA169 Famous issue – Windows 2000 • Windows 2000 operating system was certified (Common Criteria) at EAL-4 in 2002. – with SP3 and one patch; – EAL-4, augmented with ALC_FLR.3 (Systematic Flaw Remediation); – Microsoft invested millions of dollars and three years of effort to gain the certification. (S. Bekker, Redmond Magazine). • Controlled Access Protection Profile (CAPP) 47 IA169 CAPP assumption A.PEER “Any other systems with which the TOE communicates are assumed to be under the same management control and operate under the same security policy constraints. The TOE is applicable to networked or distributed environments only if the entire network operates under the same constraints and resides within a single management domain. There are no security requirements that address the need to trust external systems or the communications links to such systems.” 48 IA169 Controlled Access Protection Profile • Level of protection appropriate for an assumed nonhostile and well-managed user community – requiring protection against threats of inadvertent or casual attempts to breach the system security. • The profile is not intended to be applicable to circumstances in which protection is required against determined attempts by hostile and well funded attackers to breach system security. • CAPP does not fully address the threats posed by malicious system development or administrative personnel. 49 IA169 Windows 2000 EAL-4 certification • EAL4 rating means that you did a lot of paperwork related to the software process, but says absolutely nothing about the quality of the software itself. (J.S. Shapiro) • System disconnected from networks (at different security level), disabled media drives, etc. • Don't hook this to the internet, don't run email, don't install software unless you can 100 percent trust the developer, and if anybody who works for you turns out to be out to get you, you are toast. (J.S. Shapiro) 50 IA169 And Now for Something Completely Different… about Assurance viewed by… • Customer – what level of guarantee I get that security has been implemented in the product? • Developer – what (inputs and cooperation) will my team have to provide for the evaluation? • Evaluator – did I get all required inputs and did all tests run OK to confirm the claim? • Operator – what assumptions can I build on when preparing for my actions? 51 IA169 Security Requirements for Cryptographic Modules • Federal Information Processing Standard (FIPS) Publication 140-2 (FIPS PUB 140-2) • published May 2001 and last updated Dec 2002 – FIPS 140-3 (Draft) – proposed revision, hanging in the air since 2009 (!) • 4 levels, hierarchical levelling • 11 functions (requirements): – Cryptographic module specification; Cryptographic module ports and interfaces; Role, services, and authentication; Physical security; Operational environment; Cryptographic key management; Mitigation of other attacks; … 52 IA169 FIPS 140-2 Annexes (drafts) • Annex A: Approved Security Functions (Draft 2011) • Annex B: Approved Protection Profiles (Draft 2007) • Annex C: Approved Random Number Generators (Draft 2010) • Annex D: Approved Key Establishment Techniques (Draft 2011) 53 IA169 FIPS 140-2 levels I Level 1 – basic security requirements (e.g., certified algorithm); – no specific physical security mechanisms. Level 2 – features that show evidence of tampering – physical access to the plaintext cryptographic keys and critical security parameters (CSPs) within the module • including tamper-evident coatings or seals that must be broken to attain, – or pick-resistant locks on covers or doors to protect against unauthorized physical access. 54 IA169 FIPS 140-2 levels II Level 3 – high probability of detecting and responding to attempts at physical access, use or modification of the cryptographic module; – may include the use of strong enclosures and tamper detection/response circuitry that zeroes all plain text CSPs when the removable covers/doors of the cryptographic module are opened. 55 IA169 FIPS 140-2 levels III Level 4 – physical security mechanisms provide a complete envelope of protection around the cryptographic module with the intent of detecting and responding to all unauthorized attempts at physical access; – protects a cryptographic module against a security compromise due to environmental conditions or fluctuations outside of the module's normal operating ranges for voltage and temperature; – for operation in physically unprotected environments. 56 IA169 FIPS 140-2 • Level 2 – operating system at EAL2+ • Level 3 – operating system at EAL3+ – and additional req.: Security Policy Model (ADV_SPM.1) • Level 4 – operating system at EAL4+ 57 IA169 Nice standards and theory, but… • OpenSSL derivative FIPS-certified, found flawed – that particular one de-certified, others including the flaw not • Dual EC DRBG defective by design mandated for FIPS 140-2 • IBM 4758 (with CCA API) – level 4 – easy/fast logical attacks on CCA API • Safenet Luna CA3 – disassembling showed no potting material – undocumented API functions – functionality in breach of security policy 58 IA169 Study of a particular PP • PP BSI-PP-0025 – German (BSI) Common Criteria Protection Profile for USB Storage Media – https://www.bsi.bund.de/SharedDocs/Downloads/DE/BSI/Z ertifizierung/ReportePP/pp0025b_engl_pdf.pdf?__blob=pu blicationFile • PP organisation: – the TOE description, – the TOE security environment, – the security objectives, – the IT security requirements and – the rationale. 59 IA169 PP BSI-PP-0025 – roles in the TOE • Authorised user (S1) – Holds the authentication attribute required to access the TOE’s protected memory area, in which the confidential data is stored. – Can modify the authentication attribute. 60 IA169 PP BSI-PP-0025 – roles in the TOE, cont’d • Non-authorised user (S2) – Wishes to access S1’s confidential data in the USB storage medium’s memory (examples of confidential data are given in Section 2.5). – Does not have the authentication attribute to access the protected data. – Can obtain a USB storage medium of the same type. Can try out both logical and physical attacks on this USB storage medium. – Can gain possession of the TOE relatively easily since the TOE has a compact form. 61 IA169 PP BSI-PP-0025 – threats (countered) • T.logZugriff – Assuming that S2 gains possession of the TOE, he/she accesses the confidential data on the TOE. S2 gains logical access by, for example, connecting the TOE to the USB interface of a computer system. • T.phyZugriff – Assuming that S2 gains possession of the TOE, he/she accesses the TOE’s memory by means of a physical attack. Such an attack could take the following form, for example: S2 removes the TOE’s memory and places it into another USB storage medium which he/she uses for the purpose of logical access to the memory. 62 IA169 PP BSI-PP-0025 – threats, cont’d • T.AuthÄndern – Assuming that S2 gains possession of the TOE, he/she sets a new authentication attribute, with the result that the data becomes unusable for S1. • T.Störung – A failure (e.g. power failure or operating system error) stops the TOE operating correctly. As a result, confidential data remains unencrypted or the TOE’s file system is damaged. 63 IA169 Study of another PP development • Security kernel – used to simulate a distributed environment, introduced by J Rushby (1981) as a solution to the difficulties and problems that had arisen in the development and verification of large, complex security kernels that were intended to “provide multilevel secure operation on general-purpose multi-user systems.” • U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, v 1.03 • Study paper “Separation Kernel Protection Profile Revisited: Choices and Rationale”, T.E. Levin et al., URL: http://fm.csl.sri.com/LAW/2010/law2010-03-Levin-Nguyen-Irvine.pdf 64 IA169