Formal verification: the road to complete security of smart contracts
Martin Lundfall,
MakerDAO�
With the help of Everett Hildenbrandt & Runtime verification, Denis Erfurt, Lev Livnev
Formal verification is the process of specifying and verifying the behavior of programs
Specification: mathematical description of intended program behavior
Verfication :: operational semantics of language -> specification -> proof
What kinds of assurances does formal verification provide?
For smart contract based dapps, we can roughly speak of problems coming in 4 different “flavors”
The tools and methods for analysis of these problems differ.
Four flavors of dapp behavior
What can happen over the course of one tx?
What can happen over the course of a list of tx?
What will happen in the case of eclipse attacks, frontrunning, chain reorderings, replay attacks, etc?
How will a self-interested, rational economic actor use this dapp?
Four flavors of dapp behavior
What can happen over the course of one tx?
What can happen over the course of a list of tx?
What will happen in the case of eclipse attacks, frontrunning, chain reorderings, replay attacks, etc?
How will a self-interested, rational economic actor use this dapp?
Efficacy of
formal methods
kinda
One paradigm for defining operational semantics is rewriting logic.
KEVM a.k.a. “The Jello paper” – The operational semantics of the EVM has been defined in the K framework.
Human readable, executable specification that passes the EVM VMTests and GeneralStateTests
Automatically derives a suite of analysis tools. Most crucially a debugger, and a program verifier
Specifications and reachability claims
The K prover understands specifications in terms of reachability claims:
S requires P(S) => S’ ensures P’(S’)
“Any pre-state s ∈ S satisfying P(s) will evaluate to a post-state s’ ∈ S’ s.t. P’(s’)”
Proof search by symbolic execution and branching until error or oom.
State is defined as a KEVM configuration
and is large and unwieldy
Klab act: Literal specification format
Klab act: Literal specification format
Token_transfer_pass_rough.k
Token_transfer_fail.k
Assumed true
Assumed false
Klab act: Literal specification format
Token_transfer_pass_rough.k
Token_transfer_fail.k
Assumed true
Assumed true
Klab act: Literal specification format
Token_transfer_pass_rough.k
Token_transfer_fail.k
Token_transfer_pass.k
Token_transfer_pass_oog.k
If no if header is present, _fail.k + _pass.k + _oog.k
are exhaustive and specify the entire behavior of this method.
VGas >= G
VGas < G
Klab proof debugger
K’s prover only outputs #True or #False, or fails.
Klab provides a graphical command line tool allowing you to step through and explore the symbolic execution that happens as part of a K proof.
Can also be used to explore the behavior of “unknown” contracts, where only bytecode is known.
Pic of klab here
Interlude: Writing provable smart contracts
Keep code modular and as simple as possible
Think in EVM, not in Solidity
Methods should do one thing under the right conditions, and REVERT otherwise
Avoid calls to unknown code as much as possible
Contract inheritance and the use of libraries sweeps complexity under the rug
Exhaustiveness
Non-standard models of a dapps
A dapp with complete specifications essentially define a dapp
Any bytecode that verifies against these specifications should be “just as good” as the canonical implementation
A key consideration for any formal verification process is its resilience against “adversarial code” – code that passes the specs but is otherwise “faulty”
Reverse bug bounty
Gas optimization
System invariants
Once a complete specification has been proven, the specs define the atomic steps of a relatively small state machine.
Contract methods are now “first class” primitives
The lifetime of a system can be described as a finite list of calls [C0, C1, ... , Cn], where each call is one of the specified methods
Proving system invariants can now be done with a simple induction / case splitting over the methods defined in the system.
MakerDAO System invariants
Future of formal verification
Server-client based klab – verify your contracts in the browser
Documentation generation from specs (sneak peak at stablecoin.technology)
Symbolic exploration tools for “wild” bytecode
Viper, WASM support
More kinds of claims – proof systems for linear temporal logic
Mathematical foundation of acts
Formal methods to tackle “blockchain specific” problems and incentive analysis