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 the field of 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. 50 years formal verification 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 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 analysis Static program analysis can be contrasted with techniques like unit testing and fuzzing which are forms of . 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. dynamic program analysis 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 and (developed by some of the founders of ) have shown that formal verification of complex programs like entire operating system kernels is feasible. seL4 CertiKOS CertiK 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 to formal verification due to the requirements of: very well suited 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 functions which do not have side effects on the visible state of the program (like C# property getters), which makes formal verification easier. pure 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 using their proprietary formal verification technology, and there are multiple open-source tools with different approaches to formal verification of smart contracts. auditing smart contracts Approaches to Smart Contract Formal Verification in Ethereum There are for static analysis of Ethereum smart contracts including the Solidity language compiler's module, which can formally verify contract function , , and contract as well as other conditions like the presence of arithmetic overflow and out-of-bounds array access. several open-source tools SMTChecker preconditions asserts invariants There are also external like , a language for writing formal specifications for Ethereum smart contracts. Companies like CertiK pursue research into formal verification with new languages like which can be compiled to EVM bytecode. These three tools represent 3 different approaches to verifying Ethereum smart contracts. formal verification tools Act DeepSEA 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 and . When using SMTChecker, 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. assert require requires With this approach, contract specifications are derived and verified directly from Solidity code without the need to use another language or tool. on the other hand is an entirely separate language that is used to declare the formal specification of an Ethereum smart contract e.g. Act 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 also use open source formal languages and frameworks like for developing for the EVM and Ethereum smart contracts external to Solidity code. Runtime Verification K formal specifications 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 that can be read and using the Coq theorem prover. formal specification proved interactively 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 is an open-source tool for static analysis and formal verification of C# smart contracts. Silver Stratis Silver uses the framework developed by Microsoft Research for developing formally verified object-oriented programs in C#. Spec# 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 ) that statically verifies the CIL bytecode generated by the Spec# compiler conforms to the specification of the program. independent project 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 and and simple math functions like and . forall exists max 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 flag or use the 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. --verify verify 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 called SimpleVerifiableContracts to store our contract code. You can download a Silver or build it yourself using the instructions on the GitHub . example project release repo Method Contracts First, let's consider the 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. Max But in some cases, such functions may be necessary so we can naively implement a function as an example of a verifiable C# contract method. Our C# version of looks like this: Max Max 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 keyword to specify method preconditions, the keyword to specify method postconditions, the keyword to specify loop invariants and the 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: requires ensures invariant forall 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 option filters the verifier output by only matching class names with this name. We get the following output: -c Any code which doesn't satisfy our contract specification will be flagged by the Silver verifier e.g if in our method we pass an array of 4 numbers to our method this will not verify: CallMax Max Assertions To handle arbitrary array lengths in public methods we need to use the function from the Stratis smart contract API: runtime Assert 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 will be a public contract method instead of just a library method, the 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. Max runtime Assert A 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. runtime Assert A runtime in a method is thus translated to the Spec# keyword ...logically we can assume at any point in the method after the runtime until the value may change again. Assert assume a.Length >= 5 Assert s and invariants in Spec# on the other hand act as checkpoints for the verifier. A 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. Static assert static 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 with-the-capital-A and with-the-common-a .) runtime Assert static 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 folder of the repository has several examples we can look at, like a multiply function implemented as a loop: unittests for 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 instead of and the verifier caught it: i <= b i < b 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 functions. In programming 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. pure pure 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 gets sent to it and ’s it to the 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? CRS Transfer Owner We need to write a specification that the behavior of the method must always conform to. Let's imagine there's a method called which returns the balance of CRS for an arbitrary Stratis blockchain address. Donate GetBalance(Address 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 method completes, should be equal to the old value of + whatever was sent in the message to the smart contract i.e. Transfer GetBalance(Owner) GetBalance(Owner) 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 The reason this is needed is because 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. Microsoft.Contracts.Owner. Owner 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 method where we declare a variable called and then say that the balance of the address is the plus the value of whatever was sent in the Message. Transfer oldBalance Owner oldBalance The method we see above is part of the Silver 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. GetBalance base smart contract library //@ 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 the method we see it actually returns a which indicates the success or failure of the transfer operation. Logically it is only when the is a success that the balance of the address will increase. So we can say this in our specification for our Donate method: look at Transfer ITransferResult ITransferResult Owner 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 method is verified successfully: ==> Donate [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 as a post-condition to the method by turning this static to a runtime and replacing the variable with the use of the Spec# operator. The final version of our simple verifiable method is: assert Donate assert Assert oldBalance old Donate 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 not returning a 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 the bugs in code that did not conform to the specification. ITransferResult Success. all 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 or 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. Multiply Donate 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 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 . why 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.
