Background
It seems almost every week we hear of bugs and security incidents involving smart contracts that result in significant financial and reputation losses to organizations and individuals.
Smart contracts contain the implementations of DAOs, voting systems, tokens, NFTs, DeFi services, and many other kinds of blockchain applications and assets.
By their nature smart contracts can be accessed by anyone, their code can be inspected by anyone, and their transactions and state changes are recorded on a public blockchain and can be observed by anyone.
Couple these facts with the immutability of smart contract transactions and you end up with both a tempting target for deliberate exploits by attackers and a source of potentially disastrous consequences from inadvertent programming errors in smart contract code.
For at least 50 years the field of formal verification has offered to programmers the tantalizing vision of eliminating programming errors and automagically finding bugs and vulnerabilities in operating systems and applications using formal logic and mathematics.
Formal verification refers to the process of automating checking a hardware or software system for errors by checking a formal model of the system against formal requirements or specifications of behavior.
Both models and specifications are precise enough that a computer can perform the checks with the help of tools like automated theorem provers and SMT solvers.
Different formal models can be used e.g. a digital electronic or mechanical system can be modeled as a finite state machine and a formal specification can be a list of valid state transitions for the system.
A formal verification would show the system never makes a state transition not in the specification, without the designer or programmer having to exhaustively test and observe every possible state.
Formal verification is thus a kind of static analysis where an attempt is made to deduce the properties of a program by examining its source code or binary code without actually executing the program.
Static program analysis can be contrasted with techniques like unit testing and fuzzing which are forms of dynamic program analysis. Dynamic analysis relies on the programmer and the testing or fuzzing application specifying the conditions under which the program code will execute and be examined, like the range of input values to a smart contract method.
However, programs and the environments they run in are often complex enough that is practically impossible for programmers to specify or simulate in advance all the input or conditions a program will encounter, and examine in total the behavior which results from each condition.
Exploits in smart contracts are usually due to attackers discovering program behavior due to certain highly specific smart contract inputs and edge cases and blockchain states that were not considered by the programmers beforehand.
Today many areas of computing like industrial and safety-critical systems, microprocessor design, cryptographic protocol design and implementation, operating system device driver implementation, and others depend on and extensively use formal verification.
Projects like seL4 and CertiKOS (developed by some of the founders of CertiK) have shown that formal verification of complex programs like entire operating system kernels is feasible.
Many programming tools and languages now exist for carrying out formal verification of software either for existing languages like C or Java or Solidity, or through completely new languages that support constructing formal specifications directly.
While formal verification may be hard to implement for general purpose applications, smart contracts are very well suited to formal verification due to the requirements of:
-
Determinism
-
Restricted execution and state changes
-
Simplicity of logic
-
Finite execution times
In a blockchain, the different nodes must be capable of reaching consensus on changes to the blockchain state by the addition of transactions. Smart contracts must therefore not contain operations like I/O and network calls or date-time calls or any operations that can execute differently due to differences in the hardware or software environments of the different blockchain nodes.
This includes operations that dynamically allocate memory on the heap which can fail due to memory exhaustion. Smart contracts use an explicit notion of state in contrast to regular programs where state is only implicitly defined, and things regular programs contain like mutable global variables or mutable public fields or arbitrary objects allocated on the heap are generally not permitted in smart contracts.
The only way to share or store state persistently in smart contract methods is by using the state store on the blockchain. These characteristics make it easier to distinguish pure functions which do not have side effects on the visible state of the program (like C# property getters), which makes formal verification easier.
Smart contract program logic must be simple and not convoluted in order to be understood and audited easily. Finally, smart contracts are allocated a finite amount of gas which guarantees execution stops after a finite amount of instructions, so things like infinite loops are not possible.
All these characteristics make smart contract programs very amenable to formal verification. While unit and integrated testing, black-box testing, fuzzing, and other ways of dynamically analyzing and testing smart contracts will always be important, formal verification of smart contracts offers a way to significantly enhance the security and correctness of smart contracts.
Several companies like CertiK offer commercial services for auditing smart contracts using their proprietary formal verification technology, and there are multiple open-source tools with different approaches to formal verification of smart contracts.
Approaches to Smart Contract Formal Verification in Ethereum
There are several open-source tools for static analysis of Ethereum smart contracts including the Solidity language compiler's SMTChecker module, which can formally verify contract function preconditions, asserts, and contract invariants as well as other conditions like the presence of arithmetic overflow and out-of-bounds array access.
There are also external formal verification tools like Act, a language for writing formal specifications for Ethereum smart contracts. Companies like CertiK pursue research into formal verification with new languages like DeepSEA which can be compiled to EVM bytecode. These three tools represent 3 different approaches to verifying Ethereum smart contracts.
The Solidity compiler's SMTChecker tries to statically verify method preconditions and asserts in Solidity code which means you don't have to learn another language or tool e.g.
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
contract Max {
function max(uint[] memory _a) public pure returns (uint) {
require(_a.length >= 5);
uint m = 0;
for (uint i = 0; i < _a.length; ++i)
if (_a[i] > m)
m = _a[i];
for (uint i = 0; i < _a.length; ++i)
assert(m > _a[i]);
return m;
}
}
is an example of a verifiable method in Solidity using the existing runtime verification functions assert and require. When using SMTChecker, requires declares a precondition which is a condition involving the function parameters that must be statically verified to hold before the function is called by other functions.
With this approach, contract specifications are derived and verified directly from Solidity code without the need to use another language or tool.
Act on the other hand is an entirely separate language that is used to declare the formal specification of an Ethereum smart contract e.g.
constructor of StateMachine
interface constructor()
creates
uint256 x := 0
invariants
x <= 1
behaviour f of StateMachine
interface f()
case x == 0:
storage
x => 1
ensures
(post(x) == 0) or (post(x) == 1)
behaviour g of StateMachine
interface g()
case x == 1:
storage
x => 0
ensures
(post(x) == 1) or (post(x) == 0)
is an example of a formal specification in Act for the simple Solidity contract below:
contract StateMachine {
uint x;
function f() public {
if (x == 0)
x = 1;
}
function g() public {
if (x == 1)
x = 0;
}
}
Companies like Runtime Verification also use open source formal languages and frameworks like K for developing formal specifications for the EVM and Ethereum smart contracts external to Solidity code.
The key to this approach is the usage of a separate language from the implementation language to declare a smart contract formal specification.
DeepSEA is also an entirely separate language to Solidity with a syntax resembling functional languages like OCaml.
However, in DeepSEA you write both smart contract specification and implementation in the same language e.g.
const _totalSupply = 100000
object signature ERC20Interface = {
constructor : unit -> unit;
const totalSupply : unit -> int;
const balanceOf : address -> int;
transfer : address * int -> bool;
approve : address * int -> bool;
transferFrom : address * address * int -> bool
}
object FixedSupplyToken : ERC20Interface {
let balances : mapping[address] int := mapping_init
let allowances : mapping[address] mapping[address] int := mapping_init
let constructor () =
balances[msg_sender] := 100000
let totalSupply () =
let bal0 = balances[address(0)] in
_totalSupply - bal0
let balanceOf tokenOwner =
let bal = balances[tokenOwner] in
bal
let transfer(toA, tokens) =
let fromA = msg_sender in
let from_bal = balances[fromA] in
let to_bal = balances[toA] in
assert (fromA <> toA /\ from_bal >= tokens);
balances[fromA] := from_bal-tokens;
balances[toA] := to_bal+tokens;
true
The DeepSEA compiler generates both executable bytecode that can run on the EVM and a formal specification that can be read and proved interactively using the Coq theorem prover.
The key thing to observe with this approach is that implementation and specification of smart contracts are done in the same language, albeit a language that Solidity programmers aren’t likely to be familiar with.
Smart Contract Formal Verification in Stratis
Silver is an open-source tool for static analysis and formal verification of Stratis C# smart contracts.
Silver uses the Spec# framework developed by Microsoft Research for developing formally verified object-oriented programs in C#.
Spec# centers on the idea of a program specification expressed directly in C# code using certain small extensions to the C# language, a compiler that can understand these extensions, and a program verifier (codenamed Boogie, later spun off as an independent project) that statically verifies the CIL bytecode generated by the Spec# compiler conforms to the specification of the program.
Spec# uses C# as much as possible while providing some new keywords and constructs which allow the programmer to express method and class contracts as preconditions, postconditions, assertions, loop invariants, and class invariants, using logic quantifiers like forall and exists and simple math functions like max and min.
Silver uses an updated version of Spec# and maintains compatibility with existing C# compilers by allowing you to embed Spec# specifications as comments while rewriting C# code using Roslyn syntax rewriters to be compatible with the old C# 2.0 dialect Spec# understands.
When you compile a C# smart contract with Silver using the --verifyflag or use the verify command, Silver rewrites your code and creates another assembly compiled with the Spec# compiler. The code in this .NET assembly contains metadata allowing it to be translated into Boogie and formally verified by the Boogie program verifier. You can embed Spec# annotations into your C# code as comments which are rewritten and read by the Spec# compiler as a formal specification for your smart contract.
The key feature of Spec#'s approach to formal verification and what makes it so appealing is that specifications are written directly into smart contract code using C# syntax. Spec# retains the advantages of having the specification language be the same as the implementation language, while still allowing a broad and powerful set of specification constraints to be written and verified, using a familiar C# syntax. Silver is thus a formal verification tool that combines some of the advantages of the different approaches to Ethereum smart contract verification we saw before.
We're going to duplicate some of the examples of formal verification we looked at before using C# to give you an idea of how to use Silver. We'll create a Visual Studio example project called SimpleVerifiableContracts to store our contract code. You can download a Silver release or build it yourself using the instructions on the GitHub repo.
Method Contracts
First, let's consider the Max function example from Solidity's SMTChecker docs. Keep in mind that smart contract languages tend not to contain built-in or library functions that do things like sorting because these functions consume a lot of gas and in most cases are better suited to run off-chain by an attached dApp.
But in some cases, such functions may be necessary so we can naively implement a Max function as an example of a verifiable C# contract method. Our C# version of Max looks like this:
private uint Max(uint[] a)
//@ requires a.Length >= 5;
//@ ensures forall{int i in (0:a.Length); result >= a[i]};
{
uint m = 0;
for (int n = 0; n < a.Length; n++)
//@ invariant forall {int i in (0:n); m >= a[i]};
{
if (a[n] > m)
{
m = a[n];
}
}
return m;
}
The code is almost the same as the Solidity function but shorter. Spec# code declaring the method specification is embedded as comments which preserve compatibility with other C# compilers and the Stratis SCT validation tool.
You use the requires keyword to specify method preconditions, the ensures keyword to specify method postconditions, the invariant keyword to specify loop invariants and the forall quantifier to assert conditions or predicates that are true for all values in an array. We can verify this smart contract project on the command line using the Silver CLI:
silver compile examples\SimpleVerifiableContractsSimpleVerifiableContracts.csproj --verify
-c Arithmetic
Silver rewrites our code to be consumed by the Spec# compiler and compiles and verifies it. The -c option filters the verifier output by only matching class names with this name. We get the following output:
Any code which doesn't satisfy our contract specification will be flagged by the Silver verifier e.g if in our CallMax method we pass an array of 4 numbers to our Max method this will not verify:
Assertions
To handle arbitrary array lengths in public methods we need to use the runtime Assert function from the Stratis smart contract API:
public uint Max(uint[] a)
public uint Max(uint[] a)
//@ requires a.Length >= 5;
//@ ensures forall{int i in (0:a.Length); result >= a[i]};
{
Assert(a.Length >= 5, "The array length must be more than 5.");
uint m = 0;
for (int n = 0; n < a.Length; n++)
//@ invariant forall {int i in (0:n); m >= a[i]};
{
if (a[n] > m)
{
m = a[n];
}
}
return m;
}
If Max will be a public contract method instead of just a library method, the runtime Assert function must be used to handle arrays of arbitrary length because there's no way for the Spec# compiler to verify parameter values at runtime which get passed to the method by the Stratis CLR VM.
A runtime Assert will immediately exit the method if the condition or predicate is not met so from a logical POV we know any code from this point on will have this condition holding.
A runtime Assert in a method is thus translated to the Spec# keyword assume...logically we can assume a.Length >= 5 at any point in the method after the runtime Assert until the value may change again.
Static asserts and invariants in Spec# on the other hand act as checkpoints for the verifier. A static assert says that the condition specified must be true at this point in the program and the program verifier will try to prove the asserted condition holds.
There are many cases where you must statically assert conditions in order to get the verifier to progress to verify some final property or condition...the more static asserts you use in your code, the more you help out the program verifier. (Make sure you understand the difference between runtime with-the-capital-A Assert and static with-the-common-a assert.)
A very common type of static assert you will be using a lot is loop invariants.
Loop Invariants
Loop invariants assert conditions that will always hold through the execution of a C# loop. Loop invariants are critical to allowing Spec# to verify code containing loops like for and while blocks and while Spec# can infer some automatically, it's almost always necessary to explicitly state some in your code. For instance, if we remove the loop invariant in the above code by turning it into an ordinary comment:
// invariant forall {int i in (0:n); m >= a[i]};
Spec# is unable to verify the postcondition holds:
Verification results
└── File: c:\Projects\Silver\examples\SimpleVerifiableContracts\bin\Debug\netcoreapp3.1\ssc\SimpleVerifiableContracts.dll
└── Methods
├── ArithmeticContract..ctor$Stratis.SmartContracts.ISmartContractState$notnull: Ok
│ └── Duration: 0.322931s
├── ArithmeticContract.Max$System.UInt32.array$notnull: Failed
│ ├── Errors
│ │ └── Method ArithmeticContract.Max(uint[]! a), unsatisfied postcondition: forall{int i in (0:a.Length); result >= a[i]}
│ │ └── File:
│ └── Duration: 0.0190016s
└── ArithmeticContract.CallMax: Failed
├── Errors
│ └── Call of ArithmeticContract.Max(uint[]! a), unsatisfied precondition: a.Length >= 5
│ ├── File: c:\Projects\Silver\examples\SimpleVerifiableContracts\ssc\Arithmetic.cs
│ ├── Line: 26
│ └── Column: 9
└── Duration: 0.024215s
[09:48:29 INF] 2 out of 7 method(s) failed verification.
Let's look at another C# example using loop invariants this time from the DeepSEA language. DeepSEA doesn't seem to have many examples of usage as yet but the unittests folder of the repository has several examples we can look at, like a multiply function implemented as a for loop:
let _val : int := 0
(* a can be negative; b must be positive *)
let multiply (a, b) =
for i = 0 to b do
begin
let val = _val in
_val := val + a
end;
let val = _val in assert(val = a*b);
_val := 0
This is a just multiply implemented as a for loop adding a to itself b times. We can implement it in C# like this:
private uint Multiply(uint a, uint b)
//@ ensures result == a * b;
{
uint val = 0;
for (uint i = 0; i < b; i++)
//@ invariant i <= b;
//@ invariant val == a * i;
{
val += a;
}
return val;
}
Although this is an extremely simple function I still made mistakes implementing it the first time. I used the loop condition i <= b instead of i < b and the verifier caught it:
Verification results
└── File: c:\Projects\Silver\examples\SimpleVerifiableContracts\bin\Debug\netcoreapp3.1\ssc\SimpleVerifiableContracts.dll
└── Methods
├── ArithmeticContract..ctor$Stratis.SmartContracts.ISmartContractState$notnull: Ok
│ └── Duration: 0.3247862s
├── ArithmeticContract.Max$System.UInt32.array$notnull: Ok
│ └── Duration: 0.0189602s
├── ArithmeticContract.CallMax: Ok
│ └── Duration: 0.0329967s
└── ArithmeticContract.Multiply$System.Int32$System.UInt32: Failed
├── Errors
│ └── After loop iteration: Loop invariant might not hold: i <= b
│ ├── File: c:\Projects\Silver\examples\SimpleVerifiableContracts\ssc\Arithmetic.cs
│ ├── Line: 73
│ └── Column: 20
└── Duration: 0.0090002s
[10:24:28 INF] 1 out of 8 method(s) failed verification.
Again both invariants are necessary to verify that the postcondition holds.
Verifying C# Contract Methods With State
Both examples we've looked at so far are examples of pure functions. In programming pure usually denotes functions or methods that do not change the visible state of the program or object when they execute; algorithms for numeric operations are typical examples of pure functions.
There's a stronger version of pure which denotes functions whose return value only depends on parameter values like mathematical functions i.e. functions that are deterministic, but the weaker version is more commonly used in object-oriented programming and is what Spec# uses.
Smart contracts usually involve modifying the state of the blockchain by adding blocks containing the transactions they have created. So let's look at an example of a contract method that results in blockchain state changes.
Imagine we want to create a Stratis DeFi app that helps people donate to their favorite open-source developer. A smart contract implementation in C# might start with something like this:
using Stratis.SmartContracts;
public class DonateContract : SmartContract
{
public DonateContract(ISmartContractState state)
: base(state)
{
state.PersistentState.SetAddress(nameof(Owner), state.Message.Sender);
}
public void Donate()
{
Transfer(Owner, Message.Value);
}
private Address Owner
{
get => return State.GetAddress(nameof(Owner));
set => State.SetAddress(nameof(Owner), value);
}
}
This is a really simple contract that takes whatever CRS gets sent to it and Transfer’s it to the Owner address. The owner of the smart contract is stored in the persistent state in the constructor and this code runs once when the contract is created. So how can we formally verify this contract?
We need to write a specification that the behavior of the Donate method must always conform to. Let's imagine there's a method called GetBalance(Address address)which returns the balance of CRS for an arbitrary Stratis blockchain address.
This method doesn't exist in Stratis smart contracts for arbitrary addresses and with most blockchains, this function is non-trivial to implement...but at the specification level all we care about is how this function behaves, not its implementation.
A key thing to remember about writing specifications is to focus on logic, not implementation.
If we had such a method we could say that after the Transfer method completes, GetBalance(Owner)should be equal to the old value of GetBalance(Owner) + whatever was sent in the message to the smart contract i.e.
ulong oldBalance = GetBalance(Owner); // Get the old balance for the Owner address
Transfer(Owner, Message.Value); // Transfer whatever was sent
assert GetBalance(Owner) == oldBalance + Message.Value; //The new balance should now include whatever was sent.
This is our first attempt at a specification. To write this in Spec# we just need to add 3 annotations to our smart contract:
using Stratis.SmartContracts;
public class DonateContract : SmartContract
{
public DonateContract(ISmartContractState state)
: base(state)
{
state.PersistentState.SetAddress(nameof(Owner), state.Message.Sender);
}
public void Donate()
{
//@ assume Microsoft.Contracts.Owner.None(Owner);
//@ ulong oldBalance = GetBalance(Owner);
Transfer(Owner, Message.Value);
//@ assert GetBalance(Owner) == oldBalance + Message.Value;
}
private Address Owner
{
get => return State.GetAddress(nameof(Owner));
set => State.SetAddress(nameof(Owner), value);
}
}
The first thing that sticks out is the annotation referencing Microsoft.Contracts.Owner.The reason this is needed is because Owner is a property of the SmartContract class i.e. a method call, not a field. Spec# has this idea of object mutability where calling a method switches the method's receiver(target) to a mutable or "unowned" state where it doesn't have an "owner" and every other object in the call that could possibly be modified must be in the same mutable state.
This happens automatically for fields but not for properties. It's just a minor bookkeeping detail when writing specifications that involve properties instead of fields and isn't important to dig into right now.
The important parts of our specification are the lines above and below our call to the Transfer method where we declare a variable called oldBalance and then say that the balance of the Owner address is the oldBalance plus the value of whatever was sent in the Message.
The GetBalance method we see above is part of the Silver base smart contract library and is not part of the Stratis API for smart contracts. It can only be accessed in a specification i.e. inside the //@ statement blocks.
But...when we try to verify this, it doesn't pass:
Uh-oh, it looks like we made a mistake in our reasoning.
When we look at the Transfer method we see it actually returns a ITransferResult which indicates the success or failure of the transfer operation. Logically it is only when the ITransferResult is a success that the balance of the Owner address will increase. So we can say this in our specification for our Donate method:
public void Donate()
{
//@ assume Microsoft.Contracts.Owner.None(Owner);
//@ ulong oldBalance = GetBalance(Owner);
ITransferResult r = Transfer(Owner, Message.Value);
//@ assert r.Success ==> GetBalance(Owner) == oldBalance + Message.Value;
}
where ==> is the logical implication operator in Spec#. With this specification, the Donate method is verified successfully:
[11:03:08 INF] Compilation succeded with 0 warning(s). Assembly is at c:\Projects\Silver\examples\SimpleVerifiableContracts\bin
\Debug\netcoreapp3.1\ssc\SimpleVerifiableContracts.dll.
Verification results
└── File: c:\Projects\Silver\examples\SimpleVerifiableContracts\bin\Debug\netcoreapp3.1\ssc\SimpleVerifiableContracts.dll
└── Methods
├── ArithmeticContract..ctor$Stratis.SmartContracts.ISmartContractState$notnull: Ok
│ └── Duration: 0.2784462s
├── ArithmeticContract.Max$System.UInt32.array$notnull: Ok
│ └── Duration: 0.0190412s
├── ArithmeticContract.CallMax: Ok
│ └── Duration: 0.034999s
├── ArithmeticContract.Multiply$System.Int32$System.UInt32: Ok
│ └── Duration: 0.0079999s
├── DonateContract..ctor$Stratis.SmartContracts.ISmartContractState$notnull: Ok
│ └── Duration: 0.1226313s
├── DonateContract.Donate: Ok
│ └── Duration: 0.086572s
├── DonateContract.get_Owner: Ok
│ └── Duration: 0.0195311s
└── DonateContract.set_Owner$Stratis.SmartContracts.Address$notnull: Ok
└── Duration: 0.0155473s
[11:03:10 INF] Verification succeded for 8 method(s).
Once we have the correct specification we can write the ending assert as a post-condition to the Donate method by turning this static assertto a runtimeAssert and replacing the oldBalance variable with the use of the Spec# old operator. The final version of our simple verifiable Donate method is:
public void Donate()
//@ ensures GetBalance(Owner) == old(GetBalance(Owner)) + Message.Value;
{
//@ assume Microsoft.Contracts.Owner.None(Owner);
ITransferResult r = Transfer(Owner, Message.Value);
Assert(r.Success, "The transfer did not succeed.") ;
}
Analysis
Of course, we could have found the issue in our code by writing a unit test and using a mocking framework that would simulate ITransferResult not returning a Success. But the difference is that using formal verification we found a bug in our code by checking the formal specification of a method against its implementation, and this same procedure would find all the bugs in code that did not conform to the specification.
Our bug-hunting procedure relies on logic and writing a single specification, not on our ability to anticipate and write tests for every condition that could arise when our code interacts with its environment. While the need to write a formal specification requires a few more lines of code, specifications in Spec# are concise and continuous with our existing C# code, in contrast to languages like Act or the K framework.
Conclusion
Hopefully, this article has given you a small taste of what formal verification is and how it can help you develop safer smart contracts. Even when writing very simple code like the Multiply or Donate method, I liked the feeling of the verifier looking over my shoulder and pointing out possible mistakes. Common programming errors like off-by-one loop condition errors can potentially result in disastrous consequences in smart contracts.
One way to compare formal verification to other analysis and testing methods is by observing that dynamic analysis like unit tests and black-box testing usually produces underestimation and false negatives regarding potential security issues in smart contract code, while static analysis methods like formal verification usually produce over-estimation and false positives regarding potential issues.
Silver is currently under development and there are many ways that the formal verification features can be improved e.g right now Silver doesn't give any indication of why a condition or invariant fails to hold. It should be possible to extract this info from the Z3 model which was generated as a counterexample to show the verification conditions are not valid. In addition, using Silver from the CLI is not optimal, it would be far better if this information could be made available inside Visual Studio via the existing Silver Roslyn analyzer.
We've only scratched the surface of this huge topic and this article is just the first of hopefully many more articles on formal verification of Stratis C# smart contracts as a great way to supplement existing dynamic analysis and testing methods and to improve the security of blockchain applications and assets.