Formal Verification: Why and How

Smart contract’s security is still a crucial challenge in the Ethereum Ecosystem. In fact, since code is law once a smart contract gets exploited, there is no way back. This is important especially if a contract is constructed to manage with large quantities of capital. All of us remember the Parity multi-sig wallet case where 300 million dollars got lost because someone killed one of the main components (Library contract) by mistake. Therefore, debugging smart contracts must be a duty of extreme importance and should be done extremely carefully, thus we need a way to be sure at almost 100% that what’s is written in a solidity smart contract works as expected.

Here is How Formal verification comes to play: What if instead of testing our smart contracts using our own convictions as humans beings, we instead use mathematically generated proofs?

Here is How:

The core of formal verification is the K Framework.

The K Framework is nothing more than:

a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules.

In simpler words, K Framework is a language specifically made for defining semantics. Semantics describes the behaviour of computer programs. For example, when we say that a construction x++ for x that is uint256 means that a program in Solidity executing it will always increase the value of x by 1, except for one value x = 2²⁵⁶–1:

Thanks to the K Framework we can write our specifications for our smart contract. Specifications are the set of rules that our smart contract has to follow in order to function correctly.

After our specifications are done we are verifying them using the Z3 Theorem Prover. Z3 is a high-performance theorem prover whose job, in this case, is to verify whether for any input a determined condition is respected. If we have written our specifications and smart contracts correctly then the verification will be successful and the proof will be Accepted.

Here is the workflow:

But How can we accomplish that?

In order to formally verify a contract, you have to verify its semantic

Let’s consider the following contract:

What this contract does is allowing to execute set to change valueand then lock that information by setting isSet to true, thus making any attempts to execute set result in a revert

The Solidity compiler stores the variable value in slot 0 and the variable isSet in slot 1. If we want to verify whether set does its job as it is supposed to (set valueonly once) we will have to verify:

• If for any possible input with slot 1 set to false, the contract modifies value as it is supposed
• If for any possible input with slot 1 set to true, the contract always reverts

This may sound like something very hard to do, but in reality, is quite simple and there are multiple options to start formally verifying your smart contracts and there are tools that allow us to perform Formal Verification at a relatively high level. In this article, I am going to use klab , a tool provided by DappHub that comes with a high-level specification language.

Let’s start writing code

Let’s set up our environment like this:

├── dapp
│   ├── out
│   │   └── OneWaySetter.sol.json
│   └── src
│       └── OneWaySetter.sol
└── src
    ├── prelude.smt2.md
    ├── specification.act.md
    └── storage.k.md

where:

• config.json is the file that tells to Klab where and what to look at.
• OneWaySetter.sol is our Solidity Smart Contract
• OneWaySetter.sol.json is our compiled Solidity smart contract (in order to compile your smart contract open your terminal, go to the dapp folder cd dapp and type

solc --combined-json=abi,bin,bin-runtime,srcmap,srcmap-runtime,ast src/OneWaySetter.sol > out/OneWaySetter.sol.json

• specification.act.md is where our specifications are contained (Klab high-level language)
• storage.k.md is used to complete our specifications (high-level semantics) with some K language (low-level semantics). this file will be empty in this case.
• prelude.smt2.md is written using the low-level input format of Z3 theorem prover and contains the prelude of our formal verification. the prelude is the collections of all the facts that could be relevant to our smart contract.

Our Specification.

First, let’s make our configuration:

For this example, we aren’t using anything that needs storage.k.md so we will keep it empty.

This is our prelude (prelude.smt2.md):

Finally, let’s define our specifications (specification.act.md):

```act
behaviour set of OneWaySetter
interface set(uint256 Value)
types
   IsSet : bool
storage
   0 |-> _ => Value
   1 |-> IsSet => 1
iff
   VCallValue == 0
   IsSet == 0
```

What we are doing here is:

Types Preamble:

• in the types preamble we declare the variables needed for our specification

Storage Preamble:

• in the storage preamble, we specify anything that changes the contract’s state and assigns the values declared into the types premble
• setting IsSet to represent the value of slot 1 before the execution of set and specify that after the execution slot 1 changes its value to one.
• Specify that slot 0 changes to the value given as input.

Iff Preamble:

• in the iff preamblewe determine the conditions needed for not cause a revert
• We say that there should be no ethers sent along with the transaction VCallValue == 0 and that the slot 1must be 0 before the execution of set.

now we can run klab prove-all and:

Doing initial spec build, this may take a while...
[ 'src/OneWaySetter.sol' ]
[ 'src/OneWaySetter.sol' ]
3410388bb51887b48311a94d8f63166ba1ad88dd98b988ece7a0e734622b2801 OneWaySetter__exhaustiveness
51c13b8610bad9cbfd805e52e169b639870b3a24860c265cd82fb2aa6e7a3775 OneWaySetter_set_pass_rough
d9f27f2f84fec78589a6c8bd390748a396250bfe5b0195f0bde7daa0f8eda667 OneWaySetter_set_fail_rough
STARTING proof batch 1.
Academic tradition requires you to cite works you base your article on.
When using programs that use GNU Parallel to process data for publication
please cite:
O. Tange (2011): GNU Parallel - The Command-Line Power Tool,
  ;login: The USENIX Magazine, February 2011:42-47.
This helps funding further development; AND IT WON'T COST YOU A CENT.
If you pay 10000 EUR you should feel free to use GNU Parallel without citing.
To silence this citation notice: run 'parallel --citation'.
2020-01-11T11:09:38.620Z
2020-01-11T11:09:38.624Z
Using evm-semantics from /home/giulio/klab/evm-semantics/
Proof STARTING: d9f27f2f84fec78589a6c8bd390748a396250bfe5b0195f0bde7daa0f8eda667.k [OneWaySetter_set_fail_rough] (with state logging)
Using evm-semantics from /home/giulio/klab/evm-semantics/
Proof STARTING: 51c13b8610bad9cbfd805e52e169b639870b3a24860c265cd82fb2aa6e7a3775.k [OneWaySetter_set_pass_rough] (with state logging)
Proof ACCEPT: 51c13b8610bad9cbfd805e52e169b639870b3a24860c265cd82fb2aa6e7a3775.k [OneWaySetter_set_pass_rough] (with state logging)
2020-01-11T11:10:51.968Z
/home/giulio/klab/bin/klab: riga 2: /home/giulio/klab/bin/../libexec/klab-gas-analyser: File o directory non esistente
2020-01-11T11:10:52.293Z
Using evm-semantics from /home/giulio/klab/evm-semantics/
Proof STARTING: 3410388bb51887b48311a94d8f63166ba1ad88dd98b988ece7a0e734622b2801.k [OneWaySetter__exhaustiveness] (with state logging)
Proof ACCEPT: d9f27f2f84fec78589a6c8bd390748a396250bfe5b0195f0bde7daa0f8eda667.k [OneWaySetter_set_fail_rough] (with state logging)
2020-01-11T11:10:54.822Z
Proof ACCEPT: 3410388bb51887b48311a94d8f63166ba1ad88dd98b988ece7a0e734622b2801.k [OneWaySetter__exhaustiveness] (with state logging)
2020-01-11T11:11:48.006Z

as we can see our formal verification is successful and that was quite simple to do. so what does this tell us:

Making Errors is easy for humans, but for mathematics, it is not, so we should put our trust in math as much as possible rather than in a developer. if you don’t, you will end like the Parity multi-sig wallet.

~ Cheers

Giulio2002 - Overview

Get Best Software Deals Directly In Your Inbox