Formal Verification - SOFT40171 Lecture Notes PDF

SOFT40171 – Design and Development of Secure Systems Week 4 – Introduction to Formal Verification Dr Alexandros Konios 18/02/2025 Agenda  What formal verification is  Definition of formal verification  Different verification techniques  T...

SOFT40171 – Design and Development of Secure Systems Week 4 – Introduction to Formal Verification Dr Alexandros Konios 18/02/2025 Agenda  What formal verification is  Definition of formal verification  Different verification techniques  Theorem Proving and Model Checking  Introduction to Temporal logic and specifically to Computation Tree Logic (CTL)  Explanation of CTL syntax, quantifiers and operators Week 4 – Introduction to Formal Verification Learning Objectives Upon completion of this session, you should be able to:  Explain the main verification techniques and their aim  Used to examine the correctness of a system w.r.t its formal specification  Express system properties in Computation Tree Logic  Use CTL quantifiers and operators Week 4 – Introduction to Formal Verification Formal Verification 18/02/2025 Formal Verification Formal Verification is the process of checking the correctness of a system with respect to the system specification  Prove or disprove system properties using formal methods Properties used in Formal Verification are explicitly defined using a formal language  This language has formal semantics that are used to express the properties Week 4 – Introduction to Formal Verification Types of Formal Verification Formal Verification can be distinguished into two main categories of verification techniques:  Theorem proving techniques  Used to prove that a mathematical and logical statement related to the system is is a logical consequence of a set of statements (the axioms and hypotheses).  Based on predicate logic.  Model checking techniques  Check properties against the generated state space of the behavioural model of the system In this talk, we will focus only on the model checking of system properties Week 4 – Introduction to Formal Verification Model Checking Model checking is a method of formally verifying finite-state concurrent systems.  Properties about the system are expressed as temporal logic formulas.  Use of efficient symbolic algorithms to check these properties against the state space of the model defined by the system and conclude whether the specification holds or not. In other words, the idea of Model Checking is to inspect all the reachable states of a system to check if some state fails to satisfy a given correctness criterion (e.g., existence of a deadlock state). Week 4 – Introduction to Formal Verification Properties to be Verified There exist two categories of system properties that are usually verified via model checking:  Safety properties  Assert that bad system behaviour must not happen  Liveness properties  Assert that good system behaviour must happen Example: Assuming that you have a software that performs mathematical operations. Thus, these properties could be as follows:  Safety property: The software will never fail  Liveness property: The input operations are successfully executed. Week 4 – Introduction to Formal Verification Temporal Logic 18/02/2025 Temporal Logic Temporal logic can be defined as a set of rules and symbols that represent and reason about propositions in terms of time. There exist different temporal logics with different view of underlying computation.  Computation Tree Logic (CTL) views computation of a system as a tree.  System can move into different paths for future states.  Linear Temporal Logic (LTL) views computation of a system as a set of paths.  System can move only along one direction (path) into the future. The choice between CTL and LTL depends on what the problem is about (e.g. examine sequential or concurrent behaviour):  CTL allows us to quantify over paths whereas LTL does not;  LTL allows us a greater ability to describe individual paths. Week 4 – Introduction to Formal Verification Computation Tree Logic (CTL) – Operators and Quantifiers CTL is used to describe paths navigation from a given state.  Using sets of path quantifiers and logical and temporal operators Logical Operators:  Logical operators used in CTL are: ¬, ∧,∨, ⇒ and ⇔. Temporal Operators:  The temporal operators of CTL are distinguished into path quantifiers and linear temporal operators:  Path quantifiers:  A (also ∀): for all computation paths from a state.  E (also ∃): for some computation path(s) from a state.  Linear temporal operators: describe properties along a path.  Gp (symbol ◻◻) ─ p holds at every state (or always) along the path.  Fp (symbol ♢) ─ p holds at some state along the path.  Xp (symbol ⚬) ─ p holds at the next state of current one along the path  pUq ─ p holds until q holds at some state along the path.  pWq − similar to U, but q does not need to hold. Week 4 – Introduction to Formal Verification Examples of Operators and Quantifiers (1/2) Explaining the “global” temporal operator (i.e. Gp): “Gp is true for a computation path if p holds at all states (points of time) along the path.” p= … s0 s1 s2 s3 s4 Explaining the “eventual” temporal operator (i.e. Fp): “Fp is true for a computation path if p holds at some state (point of time) along the path.” p= … s0 s1 s2 s3 s4 Week 4 – Introduction to Formal Verification Examples of Operators and Quantifiers (2/2) Explaining the “next” temporal operator (i.e. Xp): “Xp is true for along a computation path if p holds at the next state of the current one.” p= … (Assuming s0 is the current state) s0 s1 s2 s3 s4 Explaining the “until” temporal operator (i.e. pUq): “pUq is true for a computation path if p holds at all state along the path until a state where q hold is reached.” p= q= … s0 s1 s2 s3 s4 Week 4 – Introduction to Formal Verification Computation Tree Logic (CTL) – Syntax and Combination of Operators/Quantifiers The syntax of the Computation Tree Logic is based on the combinations of the temporal operations and path quantifiers along with the use of the logical operators. Possible combinations are:  AG, AF, AX  EG, EF, EX Using logical operators with the above combinations to define properties:  AG(¬ p)  EF (p1 ∧ p2)  AX (p1 ∨ p2)  AG(p1 ⇒ EF(p2)) Week 4 – Introduction to Formal Verification Computation Tree Logic (CTL) – Syntax and Combination of Operators/Quantifiers  AG p AF p AX p  EG p EF p EX p Week 4 – Introduction to Formal Verification Activity in CTL Taking as example the Petri net model of the producer and consumer problem, try to express the following properties in CTL propositions:  The consumer eventually consumes the product by removing it from the buffer.  If the producer is ready to produce, next he always put his product to the buffer.  The buffer is always empty or full.  If the buffer is not full, then it is empty (and vice versa). Week 4 – Introduction to Formal Verification Example of Producer and Consumer Considering the PN: The Reachability Graph of this PN model is: Week 4 – Introduction to Formal Verification Summary The most important points of this session are summarised below:  Formal Verification enables the detection system errors with respect to the system specification  Model checking investigates the system properties using CTL or LTL to consider Week 4 – Introduction to Formal Verification References Clarke E. M. (2008). The birth of model checking. In 25 Years of Model Checking, volume 5000 of Lecture Notes in Computer Science, pp 1-26. Springer Berlin Heidelberg. Clarke, E. M., Klieber, W., Novacek, M. and Zuliani, P. (2012). Model checking and the state explosion problem. In Tools for Practical Software Verication, volume 7682 of Lecture Notes in Computer Science, pp 1-30. Springer Berlin Heidelberg. Week 4 – Introduction to Formal Verification Any Questions?