<style>
.reveal {
font-size: 24px;
}
</style>
## Smart contracts as inductive systems
Martin Lundfall, Ethereum Foundation @ EthCC[3].
slides at: https://cutt.ly/proof
---
## The dual nature of specifications
Martin Lundfall, Ethereum Foundation @ EthCC[3].
slides at: https://cutt.ly/proof
---
## An update from the formal verification team
Martin Lundfall, Ethereum Foundation @ EthCC[3].
slides at: https://cutt.ly/proof
---
## What are smart contracts?
<span>
_"A smart contract is a set of promises, specified in digital form, including protocols within which the parties perform on these promises."_
Nick Szabo, 1996
<!-- .element: class="fragment" data-fragment-index="1" --></span>
<span>
| Good | Bad |
| -------- | -------- |
| Emphasises _protocol_ of interaction | Vague |
| Specifies attack vectors: naïve vandalism or incentive compatible breaches | Stake seems to live "beyond" the contract |
<!-- .element: class="fragment" data-fragment-index="2" --></span>
<!-- "A mediator must be trusted with some of the contents and/or performance of the contract. An arbitrator must be trusted with some of the contents, and some of the history of performance, and to resolve disputes and invoke penalties fairly." -->
<!-- PoW / PoS seem to fit this description -->
---
### A humble vending machine
![](https://i.imgur.com/pxPRz2x.jpg)
---
## What are smart contracts?
<span>
_"A smart contract is an address with nonempty EVM bytecode"_
Yellow paper, 2014
<!-- .element: class="fragment" data-fragment-index="1" --></span>
<span>
| Good | Bad |
| -------- | -------- |
| Specific | Implementation specific |
| Clear model of statefulness | What are attacks? |
<!-- .element: class="fragment" data-fragment-index="2" --></span>
<!-- People who reject the term DAO "attacker" -->
---
## What are smart contracts?
<span>
An initial state, together with a finite list of stateful functions, operating in a context of other stateful systems.
Inductive systems, with each external function method an inductive step.
<!-- .element: class="fragment" data-fragment-index="1" --></span>
<!-- Appropriate level of abstraction. -->
<!-- Splits concerns into implementation and design. -->
---
<span>
<!-- .slide: data-background="https://i.imgur.com/7yCoZwl.png"-->
</span>
---
## Tree of possible states
![](https://i.imgur.com/67oWY4y.png)
---
## Defining smart contracts
We **define a smart contract** by specifying the initial state and the (stateful) functions. To specify the functions, we declare how they update state and their return value.
We **define the design goals** of a smart contract by specifying what properties should be true of these functions.
We **implement a smart contract** by writing algorithms satisfying the specifications.
---
## Specifications allows for modular formal verification
Given a specification we can verify the implementation or design goals of a smart contract.
---
## Verifiying implementation
Strategy: symbolic execution or model checking.
<span>
### Verifying source code
<!-- .element: class="fragment" data-fragment-index="1" -->
</span>
<span>
- Demonstrating that the Solidity code performs the state updates as specified.
- Requires a formal semantics of Solidity.
- Assumes correctness in compiler.
- Tools: `smt-checker`, `solc-verify`, ....
<!-- .element: class="fragment" data-fragment-index="1" -->
</span>
<span>
### Verifying EVM bytecode
<!-- .element: class="fragment" data-fragment-index="2" -->
</span>
<span>
- Demonstrating that the EVM bytecode performs the state updates as specified.
- Requires a formal semantics of EVM.
- Tools: `KEVM`, `Mythril`, ...
<!-- .element: class="fragment" data-fragment-index="2" -->
</span>
<span>
Longer list of fv tools at [github.com/leonardoalt/etherem_formal_verification_overview](https://github.com/leonardoalt/ethereum_formal_verification_overview)
<!-- .element: class="fragment" data-fragment-index="3" -->
</span>
---
## Verifiying design goals
Strategy: induction <span> with extra steps <!-- .element: class="fragment" data-fragment-index="1" --></span>
<span>
### Invariants
<!-- .element: class="fragment" data-fragment-index="2" -->
</span>
<span>
- A predicate over state variables that remains true for the lifetime of the contract.
- Can be split into _inductive_ and _non-inductive_ invariants.
- Examples:
- `sum(balanceOf) == totalSupply`
- $\Sigma_{i}({\tt rate_i} \cdot \Sigma_{u}({\tt art_{iu}})) + \Sigma_{u}({\tt sin_{u}})= \Sigma_u({\tt dai_u})$
- `x * y = k`
<!-- .element: class="fragment" data-fragment-index="2" --></span>
<span>
### Other
<!-- .element: class="fragment" data-fragment-index="3" --></span>
<span>
- General properties that cannot be expressed as invariants.
- "Correctness" is expressed in terms of past input data or off-chain behaviour.
- Example: `deposit_contract`.
<!-- .element: class="fragment" data-fragment-index="3" --></span>
---
## Case study: deposit contract.
- An "end-to-end" formal verification of the deposit contract was recently performed by RV.
- Both the design goals and the implementation of the deposit contract was formally verified.
- The two parts of the verification were joined in a refinement proof.
---
## Case study: deposit contract.
![](https://i.imgur.com/cM7jf76.jpg)
---
## Case study: deposit contract.
![](https://i.imgur.com/2olo2GW.jpg)
---
## Case study: deposit contract.
![](https://i.imgur.com/Ex1ccxR.jpg)
---
## Case study: deposit contract.
![](https://i.imgur.com/90vFpIh.jpg)
---
## Case study: deposit contract.
![](https://i.imgur.com/cKXoOA2.jpg)
---
## Case study: deposit contract.
![](https://i.imgur.com/So2idk1.jpg)
---
## Case study: deposit contract.
![](https://i.imgur.com/yuFzUdU.jpg)
---
## Case study: deposit contract.
![](https://i.imgur.com/TC5iXH9.jpg)
---
## Case study: deposit contract.
![](https://i.imgur.com/5Zcx32s.jpg)
---
## Design goal:
Verifying that the "incremental merkle tree algorithm" yields the same state root as the naïve algorithm.
Notably not an "invariant" property!
- Found: missing max value edge case.
## Implementation bugs found:
- [Faulty ABI encoding](https://github.com/vyperlang/vyper/issues/1563)
- [Missing calldata well-formedness check](https://github.com/vyperlang/vyper/issues/1730)
## Liveness subtlety:
- [Hardcoded gas values for precompile calls](https://github.com/vyperlang/vyper/issues/1761)
---
## What do the specs look like?
![](https://i.imgur.com/dpzpelk.png)
---
## What should a specification look like?
- Human readable
- Functional description with clear intended semantics
- Implementation agnostic
- Should be complete enough to admit "adversarial implementations"
---
## Introducing Act
- [Act](https://github.com/ethereum/act) is a specification language that grew out of [`klab`](https://github.com/dapphub/klab), a tool developed for writing KEVM proofs.
- It will support exporting implementation or design goal proofs to different backends. The first targets are:
- KEVM
- SMT
- Coq
- Refinement "for free".
---
<span>
## Specifications
<!-- .element: style="float: top;"-->
<style>
.reveal {
font-size: 24px;
}
</style>
<!--
.element {
float: right;
}
-->
</span>
Token definition in [Act](https://github.com/ethereum/act):
![](https://i.imgur.com/HWpzqaU.png)
---
## Benefits outside of formal verification
- Clear specifications help in auditing and integrations
- Specs can be tested or fuzzed against!
- Correctness criteria can be used for decentralized insurance
- An implementation neutral way of specifying ERCs.
---
## From one specification:
![](https://i.imgur.com/DOBkA6s.png)
---
## Export K specs:
![](https://i.imgur.com/TRZBOM1.png)
---
## Export K specs:
![](https://i.imgur.com/pjjYkHQ.png)
---
## Export SMT specs:
![](https://i.imgur.com/YKWMWgl.png)
---
## Export CoQ definition:
![](https://i.imgur.com/y50Aabn.png)
---
## Proving contract invariants with SMT solvers
The invariant `x * y == z` is not provable with Solidity's builtin smt-checker because the invariant is **non-linear**.
Linear arithmetic expressions can contain any valid combination of the symbols `<, <=, and, or, ==, +, -`, can crucially **not** contain multiplication between variables.
The SMT encoding used by the smt-checker is not able to prove non-linear invariants.
But proving only the inductive step is still feasible!
---
## Control flow encoding (Solidity's SMT checker) fails!
![](https://i.imgur.com/YKWMWgl.png)
---
## But proving the inductive step succeeds!
![](https://i.imgur.com/xpe6bvW.png)
---
## More details at
https://github.com/ethereum/act/tree/nonlinearexample/examples/homogeneous
---
## Difficulties:
- Calls to unknown code.
- Abstractions over arrays and mappings.
- Loops.
---
## Reentrancy complicates induction
![](https://i.imgur.com/zdv6JMa.png)
---
## Conclusion
- Write specifications, formulate correctness criteria!
- Formal verification tools are maturing. They are good at proving implementation correctness, but more work is needed to prove design goals.
- `Act` is a DSL for functional specification of smart contracts and their design goals, enabling a modular approach to formal verification.
- Add specifications and correctness criteria for your contracts at [github.com/ethereum/act/tree/master/examples](https://github.com/ethereum/act/tree/master/examples)
---
## References
🙌 Thank you! For more reading, check out:
- https://cutt.ly/proof
- https://github.com/leonardoalt/ethereum_formal_verification_overview
- https://github.com/ethereum/act
- https://github.com/dapphub/klab
- [@MartinLundfall](https://twitter.com/MartinLundfall)
{"metaMigratedAt":"2023-06-15T04:43:51.717Z","metaMigratedFrom":"YAML","title":"Smart contracts as inductive systems","breaks":"true","description":"EthCC[3] talk","contributors":"[{\"id\":\"c15c3dcc-f7fe-48c3-9f3c-72efbf8f997a\",\"add\":14226,\"del\":16491}]"}