WETH
Giáo trìnhTesting and security

Formal Verification

Xác minh hình thức trong phát triển giao thức Ethereum

A brief introduction to formal verification

Overview

Formal methods are techniques used for mathematical analysis of software and hardware systems. The philosophical roots of formal methods reach back to ancient Greece with Plato's exploration of theory of forms in his book "Sophist"; throughout 17th the century, mathematicians further developed the concept through abstract algebra. German polymath, Gottfried Leibniz's vision laid the groundwork for what we now call formal reasoning. In the 19th century, pioneering work by George Boole on analysis and Gottlob Frege on propositional logic provided the foundation for formal methods.

Under formal methods, formal verification is a verification technique that helps find the answer to a simple question: "Does a system correctly meet its required specifications?". It does that by abstracting a system as a mathematical model and proving or disproving its correctness.

A "system" is defined as a mechanism that is able to execute all of the functions given by its external interface. For a system, an "invariant" is a property that remains unchanged, regardless of its current state. For example, an invariant of a vending machine is: Nobody should be able to dispense a product for free. Formal verification tests the correctness of a system by checking if all its invariants holds true.

This rigorous method for scrutiny of systems scores the highest ranking on the EAL scale, signifying its profound impact on security.

Types of formal verification:

  • Model checking / assertion-based checking: Models a system as a finite state machine and verifies its correctness and liveness using propositional logic.
  • Temporal logic: Models a system whose propositions varies with time.
  • Equivalence checking: Verifies if two models of the same specification but varying implementations produce the same result.

Coq

Coq is a widely adopted, open source proof management system. It was used to specify and formally verify the CompCert compiler for the C programming language. The compiler is used to develop safety-critical programs for aircraft, cars, and nuclear power plants.

TLA+

TLA+ is a formal specification language developed by the Turing award-winner Leslie Lamport. It is mostly used for modeling concurrent and distributed systems. Amazon web services uses TLA+ for verifying robustness of their distributed systems.

Alloy

Alloy is an open source language and analyzer for software modeling. Notably, the flash file system design was analyzed against the POSIX standard using Alloy.

Z3

Z3 is a symbolic logic solver developed by Microsoft research. It is used in a wide range of software engineering applications, ranging from program verification, compiler validation, testing, fuzzing, and optimization.

Example

Formal verification of a system begins by selectively abstracting the system to create a focused model for correctness testing.

Dijkstra elegantly describes this process:

I have grown to regard a program as an ordered set of pearls, a “necklace”. The top pearl describes the program in its most abstract form, in all lower pearls one or more concepts used above are explained (refined) in terms of concepts to be explained (refined) in pearls below it, while the bottom pearl eventually explains what still has to be explained in terms of a standard interface (=machine). The family becomes a given collection of pearls that can be strung into a fitting necklace.

The TLA+ spec to models a traffic controller:

-------------- MODULE TrafficController --------------

CONSTANTS MaxCars
VARIABLES carsWaiting, greenSignal

Init == /\ carsWaiting = 0
        /\ greenSignal = FALSE

Arrive(car) == IF carsWaiting < MaxCars THEN carsWaiting' = carsWaiting + 1 ELSE UNCHANGED carsWaiting

Depart == IF carsWaiting > 0 THEN carsWaiting' = carsWaiting - 1 ELSE UNCHANGED carsWaiting

ChangeSignal == /\ carsWaiting > 0
                /\ greenSignal' = TRUE

Next == \/
         \E car \in {0, 1}: Arrive(car)
         \/ Depart
         \/ ChangeSignal

Invariant == carsWaiting <= MaxCars

Spec == Init /\ [][Next]_<<carsWaiting, greenSignal>> /\ []Invariant

=======================================================

Understanding the TLA+ semantics are not important for this discussion. Here is a brief of what it does:

Init initializes the system with no cars waiting. The Arrive models the arrival of cars, increasing the count of waiting cars if the maximum capacity has not been reached. Conversely, the Depart simulates cars departing from the controller, decrementing the count of waiting cars if there are any. Lastly ,ChangeSignal dictates that if cars are waiting, the traffic signal switches to green.

The invariant Invariant == carsWaiting <= MaxCars ensures the number of cars waiting never exceeds MaxCars, a defined constant.

Note how this abstraction conveniently ignores all the irrelevant interactions at a traffic signal (honking, anyone?).

Efficient abstraction is an art.

Ethereum and formal verification

Safety and liveliness assurance is central to Ethereum's decentralized infrastructure. Formal verification plays a critical role in verifying correctness of:

  • The protocol's execution and consensus specifications.
  • Client implementations.
  • On-chain smart contract applications end users interact with.

Protocol verification

Formal verification is used by the Runtime Verification team to verify bacon chain specification, and the Gasper finality mechanism.

KEVM builds upon K framework for crafting formal semantics and conducting verification of the Ethereum Virtual Machine (EVM) specification for correctness.

Formal verification is an essential tool in the test suite and was used to discover a subtle array-out-of-bound runtime error within the state transition component.

Formal verification as part of testing suite

Formal verification a slice of a Swiss cheese model in a test suite – Source: Codasip.

Verifying optimizations

Equivalence checking is extensively used for software optimization. For example, an optimized smart contract can be tested for correctness against its previous version to confirm that the optimization hasn't introduced any unintended behavior.

Smart contract verification

Bugs or vulnerabilities in smart contracts can have devastating consequences, leading to financial losses and undermining user trust. Formal verification tools like tools Certora Prover and halmos helps identify these issues.

For example, Runtime Verification formally verified a deposit smart contract application and found a subtle bug.

Formal verification has always been an integral part of the Solidity language. Here Christian from the Solidity team from an early workshop:

Solidity compiler also implements a formal verification approach based on SMT (Satisfiability Modulo Theories) and Horn solving.

Leo from EF Formal Verification team explains how to use this feature:

Challenges with formal verification

Formal verification is hard. The process itself can be complex and time-consuming, requiring specialized skills and tools. Additionally, formal verification can only guarantee the correctness of the model, not necessarily the underlying implementation itself. Errors in the translation process between model and code can still introduce vulnerabilities.

Formal verification relies on efficient abstraction of a system. And abstraction is hard. If you leave an important detail out of the abstraction it can introduce safety issues. For this reason, often times engineers use a complementary simulation method like fuzzing to test a system using random input.

Despite these challenges, formal verification is a powerful technique that can help design safe and efficient systems. We'll close on this insightful quote from Dijkstra:

“Program testing can be used to show the presence of bugs, but never to show their absence!”

Resources

🗣️ Talks

📄 Publications

Kurtosis

Kurtosis - công cụ tạo và kiểm thử mạng Ethereum cục bộ

Consensus Spec Tests

Kiểm thử thông số kỹ thuật đồng thuận Ethereum

On this page

A brief introduction to formal verificationOverviewPopular toolsCoqTLA+AlloyZ3ExampleEthereum and formal verificationProtocol verificationVerifying optimizationsSmart contract verificationChallenges with formal verificationResources🗣️ Talks📄 Publications