Formal Verification Basics: The Science of Ensuring System Integrity
In an age where digital systems underpin everything from banking to transportation and even our household gadgets, ensuring their correct
functioning is paramount. One of the techniques that has gained prominence in ensuring the trustworthiness of these systems is "Formal
Verification". But what exactly is it? Dive in as we demystify the world of formal verification.What is Formal Verification?
At its core, formal verification is a method used to prove or disprove the correctness of digital systems (like software or hardware components) against a certain formal specification or property, using formal methods of mathematics.
Imagine writing a contract for building a house. You specify the number of rooms, the size of the kitchen, the position of windows, and so forth. Once the house is built, you then verify if all these specifications have been met. Similarly, formal verification checks if a digital system meets its specifications.
Key Concepts in Formal Verification
- Specification: Before verifying a system, you need to clearly define what it's supposed to do. This is done using a formal language, often mathematical in nature, to avoid ambiguity.
- Model: This represents the system you're trying to verify. It can be a piece of software, a digital circuit, or any other system that can be modeled mathematically.
- Verification: This is the process of ensuring the system (model) adheres to its specification.
There are three primary methods:
Figure 1: Formal verification methods
- Model Checking: An exhaustive search through all possible states of the model to ensure that the system adheres to its specification. If the system is found to violate the specification, the model checker typically provides a counterexample to demonstrate the failure.
- Theorem Proving: This involves proving mathematically that the system adheres to its specification. Unlike model checking, which is automated, theorem proving often requires human intervention and insights to guide the proof.
- Equivalence Checking: Equivalence checking is the process of determining whether two systems (often two representations or levels of the same system) are functionally identical. It asserts that under all possible inputs or conditions, both systems produce the same outputs or behave identically.
-
Properties to Check:
- Safety Properties: These ensure that something bad will never happen. For example, in a train system, two trains should never be on the same track at the same time.
- Liveness Properties: These ensure that something good will eventually happen. For example, if a train is waiting at a signal, it should eventually get a green light.
- Temporal Logic: This is often used to specify properties of systems. Temporal logics allow us to reason about sequences of events and their ordering. Common temporal logics include Linear Temporal Logic (LTL) and Computation Tree Logic (CTL).
What is a Specification?
A specification is a detailed description of the design and operational characteristics of a system or component. It precisely describes what a system is supposed to do, how it should behave, or what properties it should have. Specifications are often written using formal languages or notations to avoid ambiguities.
Example: Elevator System Specification
Consider a simple elevator system. Here's a basic specification:
Figure 2: A simple elevator system
Initial State:
|
Functionality:
|
Safety Properties:
|
Performance:
|
Capacity:
|
In this example, the specification provides clear guidelines about how the elevator system should behave in various scenarios, and these guidelines can be used to design, test, or verify the elevator system.
What is a Model?
In the context of formal verification, a "model" represents a mathematical or formal representation of the system you're trying to verify. The model captures the essential behaviors and characteristics of the system, abstracting away unnecessary details to make the verification process tractable.
Using the Elevator System example:
States:
- Each floor can be a state (e.g., Ground, First, Second, ...).
- Additional states for scenarios like "moving up", "moving down", "doors open", "doors closed", "over capacity", etc.
- From the "Ground" state, if the call button for the First floor is pressed, there might be a transition to the "moving up" state.
- From the "moving up" state, when the elevator reaches the First floor, transition to the "First" floor state and possibly to the "doors open" state.
- A variable to keep track of the current weight inside the elevator.
- Variables to keep track of which floor buttons have been pressed, or where calls are coming from.
- "door open" event when the elevator reaches the requested floor.
- "door close" event, either after a certain time or when a specific button is pressed.
- "move up" or "move down" actions based on the calls or buttons pressed.
In formal verification, a constraint is a condition or a limitation defined on the behavior or properties of a system. It represents bounds or requirements that system behaviors must respect. Constraints provide a way to limit the scope of verification, filter out unwanted behaviors, or define specific conditions that must hold for the correctness properties to be valid. Possible constraints from the elevator example can be:
- Transitions to "moving" states only when "doors closed".
- No transition if weight exceeds capacity.
This model abstracts away intricate details like the mechanics of the elevator, electrical circuits, or the exact speed of the elevator. Instead, it focuses on the core behaviors and sequences of operations that we want to verify against our specifications. In formal verification, this model would then be used with tools or techniques like model checking or theorem proving to ensure it adheres to the given specifications.
What is Model Checking?
Model checking is an automated method for verifying if a given system model meets its specifications. It systematically explores all possible states and transitions in the model to check if they adhere to the desired properties specified.
Given the Elevator System:
Let's conceptualize this with a simple state diagram:
Figure 3: Simplified state diagram of an elevator system
(Note: This is a very simplified version; the real state space, especially for an elevator, is much more complex.)
Using Model Checking on the Elevator System:
- State Exploration: The model checker will start at an initial state (e.g., Ground with Doors Open) and then explore all possible transitions and states from there (e.g., Doors Closed -> Move Up -> First Floor).
- Safety Property Check: The model checker will ensure that, from any state, there isn't a transition that violates safety properties. For example, the model should never transition from a "doors open" state directly to a "move up" state.
- Liveness Property Check: The model checker will ensure properties like "if a call button is pressed on any floor, the elevator will eventually arrive at that floor."
- Feedback: If the model fails to meet the specification, the model checker will provide a counterexample showing the sequence of transitions that lead to the violation. For instance, if there's a scenario where the elevator moves with its doors open, the model checker would provide that sequence of actions as an error.
- Loop Detection: Modern model checkers can detect loops in the state space (e.g., elevator keeps moving up and down without stopping) to ensure it doesn't get stuck in infinite loops during verification.
- State Explosion Problem: One challenge in model checking is that the number of states can grow exponentially with the size of the system (many possible floor requests, door actions, etc.). Efficient algorithms and techniques, such as Binary Decision Diagrams (BDDs), are used to manage and represent large state spaces.
What is Theorem Proving?
Theorem proving is a method used to prove or disprove the correctness of certain properties of a system using deductive reasoning and formal logic. Unlike model checking, which is an exhaustive, automated exploration of all states, theorem proving involves constructing a logical argument to demonstrate the truth or falsehood of a statement about a system.
Using Theorem Proving with the Elevator System:
Imagine you want to prove the safety property: "The elevator will never move unless its doors are closed."
- Define Propositions:
- Let P be the proposition: "The elevator is moving."
- Let Q be the proposition: "The elevator doors are closed."
- Logical Argument:
- Your goal is to prove that whenever P is true, Q must also be true. This can be represented as P→Q (If P then Q ).
- Construct Proof:
- Using axioms (basic truths) and rules of inference, you'd construct a logical proof that demonstrates the truth of P→Q.
Differences between Theorem Proving and Model Checking:
| Model Checking | Theorem Proving | |
| Methodology | Exhaustive, automated state-space exploration. Checks all possible states and transitions against specifications. | Deductive reasoning. Constructs logical arguments to demonstrate properties. |
| Automation | Highly automated, but may be infeasible for large state spaces due to the state explosion problem. | Can be semi-automated with proof assistants, but often requires human intuition and expertise. |
| Output | If a property is violated, provides a counterexample (a sequence of states leading to the violation). | Produces a proof of correctness (or a proof of violation). Does not necessarily give counterexamples in the same way as model checking. |
| Scope | Best suited for systems with finite and reasonably sized state spaces. | Can handle both finite and infinite systems and can reason about more abstract properties. |
What are Safety Properties?
Safety properties are a class of properties that ensure "nothing bad happens" during the operation of a system. They are often used in formal verification to guarantee that a system doesn't enter into undesirable or dangerous states.
Using the Elevator System as an Example:
- Doors Safety: The elevator should not move unless its doors are fully closed.
- This ensures that passengers aren't at risk of falling out or getting caught between moving parts.
- Weight Limit Safety: The elevator should not operate if the weight inside exceeds its maximum weight capacity.
- This ensures that the elevator doesn't get overloaded and risk a mechanical failure or become stuck between floors.
- Emergency Stop Safety: If the emergency stop button is pressed, the elevator should halt its operation immediately.
- This ensures that in the case of perceived danger or malfunction, occupants can stop the elevator's movement.
- Interruption Safety: If an obstruction is detected while the doors are closing, they should re-open.
- This ensures that objects or individuals aren't trapped or squeezed by the closing doors.
What are Liveness Properties?
Liveness properties guarantee that "something good eventually happens" in a system. They are used in formal verification to ensure that a system doesn't become unresponsive, stuck, or deadlocked, and that it will eventually make progress.
Using the Elevator System as an Example:
- Response Liveness: If a floor button inside the elevator or a call button outside the elevator is pressed, the elevator should eventually move to that floor.
- This ensures that users aren't left waiting indefinitely.
- Door Operation Liveness: After the elevator arrives at a requested floor, the doors should eventually open.
- This ensures that passengers can enter or exit the elevator.
- Return to Default Liveness: If the elevator stays idle for a long time at a non-default floor without any input, it should eventually
return to a default floor (e.g., the ground floor).
- This is often implemented in buildings to ensure that elevators are available on primary floors when not in use.
- Emergency Resolution Liveness: If the emergency stop button is pressed, the elevator should eventually resume operation once the emergency
situation is cleared.
- This ensures that the elevator doesn't remain stuck indefinitely after an emergency stop.
What is Temporal Logic?
Temporal logic is a type of formal logic that allows for reasoning about the ordering of events and the progression of time. It extends classical propositional logic by introducing operators that capture temporal aspects, such as sequences of events, their concurrency, and their causality. Temporal logic is particularly useful in specifying and verifying properties of reactive systems, like computer programs, digital circuits, and communication protocols.
There are different types of temporal logics, with the most common ones being:
|
Linear Temporal Logic (LTL): This logic operates on linear time, where time progresses in a sequence of discrete steps or states. Common operators in LTL include:
|
Computational Tree Logic (CTL): Unlike LTL which assumes a linear progression of time, CTL works with branching time, where multiple possible future paths (branches) can emerge from a single state. Key operators in CTL include:
|
Temporal logic provides a way to specify properties of systems in a way that captures time-based behavior. This makes it invaluable in formal methods, especially in model checking, where it's used to express properties that the system should (or shouldn't) satisfy as it evolves over time.
The Power and Pitfalls of Formal Verification
Strengths:
|
Limitations:
|
Further Articles
Formal verification application on smart contracts can further be explored in the following articles:
- Formal Verification of Smart Contracts: Equivalence Checking of Uniswap Library
- Formal Verification Made Easy with SMTChecker
- SMTChecker and SMT Solvers: Exploring Formal Verification One Step at a Time
- SMTChecker: The Game Changer in Smart Contracts Verification and Security
Conclusion
As our reliance on digital systems amplifies, ensuring their foolproof behavior is non-negotiable. Formal verification, with its methodical and mathematical underpinnings, emerges as a beacon of reliability. From the chips that power our devices to financial smart contracts, formal verification techniques are silently but surely safeguarding our digital futures. In future, we will explore more application scenarios of formal verification on smart contracts.
About Truscova:
Truscova comes with 30+ years of academic research and hundreds of academic publications which pioneered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise. Truscova currently analyzes Solidity code combining Formal Verification techniques: abstract interpretation, constraint solving, theorem proving, and equivalence checking.