Formal verification is a precise, highly trustworthy method of ensuring the security of smart contracts. It is one of the more complicated and potentially intimidating approaches, but it does come with a kind of security and verified truth guarantee that other methods can’t promise.
“Formal verification is essentially concerned with identifying the correctness of hardware and software design operation. Because verification uses formal mathematical proofs, a suitable mathematical model of the design must be created.” -Science Direct
Let’s break that down in layman's terms. Formal verification, as it applies to Web3 development, is the process of taking blockchain code and using mathematical principles to verify that the behavior of the code meets certain requirements defined by a formal system specification.
A property, or invariant, can be analyzed for conformity to certain behaviors (possible value changes during execution). A logical specification is used to express those behaviors, which are used to process the code and determine if the invariants conform to their defined constraints in all possible scenarios.
There are few guarantees in security, but formal verification is an exception. It ensures, 100%, that the code meets the specification, (here’s the hitch) given that you’ve created your specification appropriately. Assuming that this is the case, you can be certain that your code will behave as specified.
This is what makes formal verification the ultimate tool for verification. Vulnerabilities are generally associated with a false assumption that the code conforms to a certain behavior, but formal verification gives you a rare certainty.
Comparing this with the fuzzing technique, we can define similar specifications for the code. However, instead of formally verifying them, fuzzing will hit the contract with tons of executions. Fuzzing uses brute force: it inelegantly blasts inputs and looks at the outputs for verification. It can be tuned to perform more optimally than random input selection, but will ultimately have computational limitations to exploring all possible behaviors that formal verification does not.
If formal verification is so powerful, why doesn’t everyone use it all the time? Well, because it’s not simple - the technique is extremely challenging and cerebral, not to mention time consuming. Choosing and building the correct verification specification is also very difficult, and the power of that 100% guarantee rests on executing this piece correctly.
Given these constraints, it’s an understandably underutilized method. So, where do we go from here?
Symbolic execution is one technique under the formal verification umbrella, and, compellingly, it’s much more approachable while maintaining a high level of rigor. Where methods like fuzzing, testing, and concrete execution explore only one path, symbolic execution instead looks at all possible execution paths and follows the possibilities those paths surface down each successive branch.
Normally, when you’re debugging a smart contract, the process takes you down a specific path. With this more dynamic technique, you can follow all the possibilities during your audit, drastically increasing the ability to discover exploitable vulnerabilities across various use cases.
There are a few tools that can help you employ the principles of symbolic execution without doing this manually (rejoice!).
Symbolic execution tools use some principles of formal verification and symbolic execution, and, crucially, explore paths and their possibilities in a controlled environment.
“A symbolic debugger is a program development tool that interacts with a running program and a programmer at the source language level. The symbolic debugger can stop the program and examine any currently active variable.” - ACM
There are several types of symbolic execution tools that can help you audit your smart contracts - debuggers, provers, and static analyzers:
The ability to tangibly explore the possibilities of symbolic execution is extremely helpful for testing and verification. When you’re auditing, you’re exploring all the possibilities in your mind - being able to look at the invariants can be a great advantage.
Symbolic debuggers remove a lot of manual calculations and the need to write an additional formal specification manually. Leveraging these tools allows you to validate complex code and the outcomes of that code without getting overwhelmed (and without being stuck in your head).
Let’s use the smart contract and its associated test file below as an example:
The example `PausableToken` contract implements approval-related functionality of a standard ERC20 token. In addition, the contract is pausable, which means that the contract’s operation will be paused if the `pause` variable is set to `true`, and calls to its functions, such as `approve`, will revert.
To make sure that `PausableToken`’s `approve` is implemented correctly, we can define the following Foundry test. The `test_approve` function has three parameters, which Foundry will assign random values to: address `from` calling `approve`, address `to` of the token allowance recipient, and `amount` of tokens they will be allowed to spend after the function execution. The assertion at the end of the test ensures that, during the execution, `approve` has set the value of `allowance` correctly.
We can successfully run this test with both Foundry and Kontrol. In both cases, the test passes, which means that the function is implemented correctly. However, analyzing it with Kontrol generates a stronger security and correctness guarantee, ensuring that `allowance` is updated properly for all possible inputs and callers.
At the same time, since the token contract can be paused, there does exist a scenario where `approve` will revert, in which case the test will fail. With regards to plausibility, the state of the contract is controlled by a storage variable `paused` which by default is `false`. The way to make it `true` in Foundry is to include a separate function call to the token contract and explicitly move it to a paused state.
Kontrol, on the other hand, allows making the smart contract’s storage values symbolic, which means that, in a single run, it can explore both execution paths whether the contract is paused or not. To make `PausableToken`’s storage symbolic, we can add a call to the `kevm.symbolicStorage(address)` cheatcode to the `setUp` function body as shown below. `symbolicStorage` is one of the supplementary cheatcodes that Kontrol supports in addition to most of Foundry’s cheatcodes. To use it, we need to install the `kontrol-cheatcode` library (`forge install runtimeverification/kontrol-cheatcodes`) and add `KontrolCheats` to the test contract’s parents. Now, Kontrol will verify that `approve` behaves correctly and does not revert not only for all possible inputs but also for all possible storage variable values in the token contract.
Running Kontrol on the updated test contract identifies a reverting execution path. The “Path condition” section of the output indicates that the failure occurs if the first byte in token’s storage slot 0 — corresponding to `paused` — does not equal zero, or, in other words, evaluates to `true`, meaning that the contract has been paused.
By simultaneously exploring all possible execution paths, Kontrol exposes a potential failure that would have been overlooked by fuzzing alone.
When running tests, Kontrol automatically converts Solidity code to EVM bytecode and, then, formal representation that can be verified. Alternatively, to make the code verifiable, one would have to come up with a specification written in a separate language. In K, specification for standard ERC20 functions would look like:
rule <k> allowance(Owner, Spender) => Allowance ...</k>
<owner> Owner </owner>
<spender> Spender </spender>
<amount> Allowance </amount>
rule <k> approve(Spender, Allowance) => true ...</k>
<caller> Owner </caller>
<owner> Owner </owner>
<spender> Spender </spender>
<amount> _ => Allowance </amount>
<log> Log => Log Approval(Owner, Spender, Allowance) </log>
requires Allowance >=Int 0
rule <k> approve(_, Allowance) => throw ...</k>
requires Allowance <Int 0
rule <k> transfer(To, Value) => true ...</k>
<caller> From </caller>
<account>
<id> From </id>
<balance> BalanceFrom => BalanceFrom -Int Value </balance>
</account>
<account>
<id> To </id>
<balance> BalanceTo => BalanceTo +Int Value </balance>
</account>
<log> Log => Log Transfer(From, To, Value) </log>
requires To =/=Int From // sanity check
andBool Value >=Int 0
andBool Value <=Int BalanceFrom
andBool BalanceTo +Int Value <=Int MAXVALUESee the full example here. For a deeper dive into Kontrol and other examples, check out this blog on Kontrol 101.
Using symbolic execution tools can help you complete audits that benefit from the thoroughness and certainty of formal verification without the burden of developing your own mathematical specifications.
Ready to give formal verification and symbolic execution a shot? Simbolik is a great place to get started. Let us know how it goes on Discord!
This post was written in collaboration with Runtime Verification.