Formal Verification of Smart Contracts with the K Framework

Currently, blockchain technology is mostly used for handling investments and significant amounts of money. But vulnerabilities in smart contracts can allow hackers to steal tokens. Recently, this happened to the biggest EOS casinos.

Performing a security audit with reliable tools is the best way to prove the indestructibility of your system. Formal verification is used when you need an ironclad guarantee that your smart contracts are protected.

In this article, we analyze the pros and cons of formal verification. To do that, we create a simple ICO smart contract on the Ethereum platform, write high-level and EVM-level specifications, and verify this smart contract with the K Framework.

What is formal verification?

Formal verification is a security audit approach that’s used to prove the correctness of underlying algorithms with respect to a certain formal specification. In order to perform formal verification, you’ll need tools from a framework and a formal specification. Using mathematical methods, formal verification proves that the final program behaves exactly as described in its specification.

Formal verification is used in fields where errors can be quite significant: when producing aircraft components, programming medical or military equipment, and so on. In order to prove the correctness of their hardware, developers turn to formal verification, as it eliminates human error. You can also improve smart contract security with formal verification.

While most blockchain systems aren’t as critical as medical equipment, errors in blockchain systems may cost millions of dollars. This makes formal smart contract verification services a great idea for auditing blockchain systems.

In the case of smart contract verification, there are several projects aimed at creating formally specified execution environments (virtual machines) for various networks. Here are some of them:

• Formal EVM semantics in Lem
• Implementations in F*
• Formal EVM semantics in the K Framework

Two levels of formal specification

Defining the requirements for a smart contract’s formal specification is the longest and most important step in conducting formal verification. Some of the requirements can be borrowed from any existing informal specification (e.g. a white paper). But unfortunately, informal specifications may omit some edge cases. For example, the white paper may simply say, “each investor receives 5% monthly dividends” without specifying how these dividends are distributed. But if you plan to apply formal verification to your smart contract, it’s considered a good practice to start by creating a formal specification. 

This may require several meetings with the smart contract developers in order to discuss the intended behavior of the contract. Every aspect of the smart contract must be thoroughly described. After that, you can move on to creating a specification.

There are two types of formal specifications:

• general, language-level specifications
• refined, bytecode-level specifications

First, the high-level business logic of the smart contract has to be formalized, based on the informal specification and requirements. The informal specification has to describe the intended functionality precisely and comprehensively. Then the smart contract developers should confirm this specification.

Afterward, the high-level specification has to be refined into a low-level specification, or bytecode-level specification, that captures the smart contract behavior at the execution level (in the context of the virtual machine). This bytecode-level specification is necessary since the code written by developers is usually not the code that’s actually going to run when deployed on the blockchain. Compilers and other external factors may influence the final smart contract. We have to ensure that only what was specified in the high-level specification will happen even at the lowest level. During the actual verification, only a bytecode-level formal specification will be used.

In the end, the only thing left to do is to verify that the smart contract meets the specification. For that, we can use one of various execution environments. In our case, we’ll use the K Framework’s correct by construction deductive program verifier.

 

A formal specification has two levels: language-level and bytecode-level.

Pros and cons of formal verification

Formal verification of smart contracts isn’t easy. There’s a steep learning curve and a high entry threshold. A developer needs to undergo special training to be able to formalize requirements using formal verification tools.

However, formal verification comes with many benefits:

• It’s comprehensive. Most formal verification tools use human-readable (or close to human-readable) languages for specifications. So the results of the audit look more like documentation than a security report.
• It’s unambiguous. A manual audit may have human error or some degree of uncertainty. A formal verification will give a definite answer to a simple question: does this program behave as described in the specification?
• It’s complete. Since verification is automatic, it will be performed diligently and thoroughly. A formal verification audit will cover the program in full, with no missed edge cases.
• It doesn’t rely on compilers. Unlike most manual auditors, a formal verification framework can easily use the compiled binary as input. This allows formal verification to catch bugs that were introduced during compilation or other transformations of the source code.
• It’s language-independent. You can easily verify smart contracts written in Solidity, Viper, or other languages that may appear in the future.
• A formal specification can work as documentation for the contract itself.

On the other hand, formal verification has a few drawbacks:

• It requires a specially prepared Ethereum execution environment, which may be unavailable for your specific network.
• A formal specification of the contract itself is required. Creating a formal specification is a long and difficult process. You can’t speed this up or skip defining and discussing the requirements for the specification.
• Verification will only detect inconsistencies between the formal specification and the implementation. If there are any errors in the specification, they will be left undetected. So both specifications should be prepared extremely carefully.
• Formal verification demands a lot of preparation from your development team.
• The price of a mistake in a formal specification is high. During verification, every false requirement will be perceived as correct. Therefore, the verification won’t detect a problem with the smart contract.

Let’s compare the formal verification approach with other, more conventional types of security verification and testing.

Formal verification vs unit testing

Unit testing is usually cheaper than any other type of audit, as it’s performed when developing a smart contract. Proper unit tests should reflect the specification and cover the smart contract with the help of use cases and functionality the specification describes. However, unit tests are just as imperfect as informal specifications. Even if the smart contract code is fully covered with unit tests, the developer may miss some edge cases that could lead to bugs or even security vulnerabilities like overflows or unprotected functions.

Creating a formal specification during development will be more labor-intensive than creating unit tests that fully cover a smart contract. However, a formal specification has a lot more benefits than ordinary unit tests.

Formal verification vs audits and bug bounties

Performing smart contract audits is common practice for developers. Independent testing teams conduct manual audits and penetration testing after creating smart contacts. An experienced developer studies the informal specification and checks the code of the smart contract to see if there are any known vulnerabilities or deviations from the intended behavior. Furthermore, the auditor can analyze GAS usage, code quality, and unit test coverage.

A manual audit is a more suitable option if the smart contract already exists and needs a security checkup. Creating a formal specification for verification at this point would take too much time and delay deployment.

A bug bounty is similar to a manual audit. However, in this case, the developers don’t explicitly employ anyone to perform an audit. Instead, they offer a reward to anyone from the community who finds and reports a bug or a security vulnerability.

Formal verification doesn’t require any third-party auditors or a bug-seeking community. Even smart contract developers can create a specification and verify their contract. Such “self-verification” is trustworthy, since mathematical proofs generated during verification are completely unbiased. Also, a formal specification is readable by humans just like an audit report, so smart contract users can easily check if they’re being fooled.

Formal verification vs static analysis tools

Static analysis tools are used to achieve the same goal as formal verification. During static analysis, a dedicated program (the static analyzer) scans the smart contract or its bytecode in order to understand its behavior and check for unexpected cases such as overflows and reentrancy vulnerabilities.

Moreover, static analyzers and formal verification frameworks may use the same mathematical “backend” in order to prove the absence of errors. For example, both the Mythril static analyzer and the K Framework use the z3 solver library for proofs.

However, static analyzers are limited in the range of vulnerabilities they can detect. In a sense, a static analyzer attempts to perform the same formal verification with a one-fits-all specification that simply states, a smart contract shouldn’t have any known vulnerabilities. Obviously, a custom specification is much better, as it will detect each and every possible vulnerability within a given smart contract.

 

Formal specifications for the K framework supports 5 languages.

Let’s see what tools are useful for verifying a smart contract. 

K Framework for creating and verifying a smart contract

The K Framework is one of the most robust and powerful language definition frameworks. It allows you to define your own programming language and provides you with a set of tools for that language, including both an executable model and a program verifier.

Many developers disregard formal semantics, as it can be difficult to implement, understand, and even use. Interpreters and compilers are usually written without guarantees of correctness, which leaves a lot of room for unexpected behavior. An ideal language framework will not only define exactly what it means for a program to behave correctly but will allow you to create tools that are correct by construction, such as parsers, compilers, interpreters, and debuggers.

The K Framework provides a user-friendly, modular, and mathematically rigorous meta-language for defining programming languages, type systems, and analysis tools. K includes formal specifications for C, Java, JavaScript, PHP, Python, and Rust. Additionally, the K Framework enables verification of smart contracts.

KEVM as a specific application of the K Framework

The K semantics of the Ethereum Virtual Machine (KEVM) is one application of the K Framework on Ethereum. It specifies the full semantics of the Ethereum Virtual Machine (EVM), adding all of the benefits of the formal specification to Ethereum smart contracts. The KEVM provides the first machine-executable, mathematically formal, human readable and complete semantics for the EVM.

The specification includes three main components:

1. The syntax of the language.
2. A description of the state/configuration.
3. The transition rules that drive the execution of programs.

The KEVM implements both the stack-based execution environment, with all of the EVM’s opcodes, as well as the network’s state, gas simulation, and even high-level aspects such as ABI call data.

This allows for simplified creation of formal specifications for smart contracts. It provides auditors with all the tools necessary to verify a smart contract. And the KEVM isn’t limited to any specific programming language.

Applying formal verification to a smart contract

In order to test formal verification on the blockchain, we’ll develop a DeFi application with a simple smart contract, define its specifications, and verify it. It’s best to use an existing framework in order to study formal verification. The K Framework and the KEVM implementation of the Ethereum virtual machine are the most popular tools for this task. We’ll use KEVM in all of our examples.

Creating a smart contract

Let’s start with a look at our smart contract:

pragma solidity 0.4.25;
contract ICO {
    mapping (address => uint256) private _balances;
    uint256 private _totalSupply;
    uint256 private _decimals = 18;
    uint256 private _hardCap = 200 * (10 ** _decimals);
    uint256 private _rate = 2;
      
    function balanceOf(address owner) public view returns (uint256) {
        return _balances[owner];
    }
      
    function buy() public payable {
        require(msg.value != 0);
        require(_hardCap <= _totalSupply + msg.value * _rate);
        _balances[msg.sender] += msg.value * _rate;
        _totalSupply += msg.value * _rate;
    }
}

This is a basic ICO, and a part of an ERC-20 token. It only has two callable functions:

1. Buy – receives Ether and distributes tokens
2. BalanceOf – returns the balance of any given account

Before creating a formal specification, we need to figure out the full requirements for the smart contract. In a real-world scenario, there would be a series of discussions with the creators of the smart contract regarding its functionality. Since we’re the creators in this case, we can design our own requirements:

• The ICO will collect 100 Ether at most, and distribute 200 tokens.
• There’s no time limit for the ICO.
• The emission rate is 2 tokens per Ether (e.g. for 0.1 Ether you will receive 0.2 tokens).

This is really as simple as an ICO can get. Now we can start defining the specification for this contract.

Defining a high-level specification

Here’s the high-level specification for our smart contract:

module ICO
    syntax Value   ::= Int  // this can be changed
    syntax Address ::= Int  // this can be changed
    // defining the "syntax" of the contract
    syntax AExp ::= Value | Address
                | "buy" "(" ")"
                | "balanceOf" "(" AExp ")"                       [strict]
                | "throw"
    // configuring cells for the contract's storage
    configuration <ico>
                  <caller> 0 </caller>
                  <value> 0 </value>
                  <k> $PGM:K </k>
                  <accounts>
                    <account multiplicity="*">
                      <id> 0 </id>
                      <balance> 0 </balance>
                    </account>
                  </accounts>
                  <supply> 0 </supply>
                  <hardcap> Int 200 * (Int 10 ^Int 18) </hardcap>
                </ico>
    // balanceOf returns the balance of a given account
    rule <k> balanceOf(Id) => Value ...</k>
       <id> Id </id>
       <balance> Value </balance>
    // The buy function receives ether and distributes tokens appropriately.
    // Requirements:
    // - the buy function has to receive ether, so the value cannot be zero
    // - once the hard cap has been reached, no more tokens can be sold
    rule <k> buy() => .</k>
       <caller> From </caller>
       <value> MsgValue </value>
       <hardcap> HardCap </hardcap>
       <supply> Total => Total +Int MsgValue *Int 2</supply>
       <account>
         <id> From </id>
         <balance> BalanceFrom => BalanceFrom +Int MsgValue *Int 2 </balance>
       </account>
     requires MsgValue >=Int 0
       andBool Total +Int MsgValue *Int 2 <=Int HardCap
endmodule

As you can see, this specification is very similar to the original smart contract. You can see definitions for both functions as well as rules of what these function should do in each case.

This specification is relatively easy to understand, so this version is a good representation of an informal specification. In fact, there are tools for converting formal specifications with comments into a more user-friendly format – and vice versa. So instead of writing an informal white paper, you can provide a human-readable formal specification.

Defining the EVM specification

The EVM-level specification is quite complex, but it has some definitions that are similar to other specifications. So in order to make it easier to define these specifications, KEVM developers prepared a convenient script. All you have to do is prepare an initialization file for it with all the necessary requirements for each function as well as the necessary parameters for proofs.

Here’s an initialization file for our sample smart contract:

// Defining EVM-level specification for the balanceOf function
[balanceOf]
k: #execute => #halt                                               //execution must stop eventually
statusCode: _ => EVMC_SUCCESS                                      //execution status must be success
output: _ => #asByteStackInWidth(BAL, 32)                          //the function returns the "balance" value
callData: #abiCallData("balanceOf", #address(OWNER))               //define ABI call data for the function (i.e. the signature balanceOf(address))
gas: {GASCAP} => _                                                 //specify GAS usage (in this case we don't really care about GAS, since the function is so simple)
refund: _                                                          //refunded GAS
storage:                                                           //specify changes to storage
    #hashedLocation({COMPILER}, {_BALANCES}, OWNER) |-> BAL        //loads balance of owner balances[owner] into BAL
requires:                                                          //specify requirements in this case - simple sanity checks for parameters
    andBool 0 <=Int OWNER     andBool OWNER     <Int (2 ^Int 160)  //owner address is a 160 bit unsigned integer
    andBool 0 <=Int BAL       andBool BAL       <Int (2 ^Int 256)  //balance is a 256 bit unsigned integer
  
// Defining EVM-level specification for the buy function
[buy]
k: #execute => #halt                                               //execution must stop eventually
statusCode: _ => EVMC_SUCCESS                                      //execution status must be success
output: _ => _                                                     //no return value
callData: #abiCallData("buy", .TypedArgs)                          //define ABI call data for the function (i.e. the signature buy())
gas: {GASCAP} => _                                                 //specify GAS usage (in this case we don't really care about GAS, since the function is so simple)
log: _                                                             //no logs
refund: _                                                          //refunded GAS unspecified
storage:                                                           //changes to storage
    #hashedLocation({COMPILER}, {_BALANCES}, CALLER_ID) |-> (BAL_FROM => BAL_FROM +Int MSGVALUE *Int 2)  //balance of caller is increased by MSGVALUE
    #hashedLocation({COMPILER}, {_SUPPLY}, _SUPPLY)     |-> (_SUPPLY => _SUPPLY +Int MSGVALUE *Int 2)    //total supply is also increased
requires:                                                          //specify requirements
    andBool MSGVALUE >=Int 0                                       //value is not zero (user actually has to pay Ether to buy tokens)
    andBool _SUPPLY +Int MSGVALUE *Int 2 <=Int _HARDCAP            //hardcap is not reached
   
// Program definition. Specifies the bytecode that will be tested. "code" is the compiled smart contract.
[pgm]
compiler: "Solidity"
code: "60806040526012600255600254600a0a60c802600355600260045534801561002657600080fd5b506101b5806100366000396000f30060806040526004361061004c576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806370a0823114610051578063a6f2ae3a146100a8575b600080fd5b34801561005d57600080fd5b50610092600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506100b2565b6040518082815260200191505060405180910390f35b6100b06100fa565b005b60008060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050919050565b6000341415151561010a57600080fd5b6004543402600154016003541115151561012357600080fd5b60045434026000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254019250508190555060045434026001600082825401925050819055505600a165627a7a7230582014c3fff87873fb01861ca509f2330c4adaa1347c8e6f4690a385850aabce07300029"
gasCap: 100000

As you can see, the EVM-level specification has similar requirements to the high-level specification but in a more machine-friendly format. You can find more examples of verified smart contracts and details about specification syntax here.

In order to produce a specification from it, we can simply call the gen-spec script from the KEVM repository like this:

python3 gen-spec.py spec-tmpl.k ico-spec.ini ico-spec ico-spec > ico-spec.k

Verifying the smart contract

Verifying the smart contact is the easiest part. Verification comes down to executing a single command:

kevm prove ./ico-spec.k

After the proof executes, the framework should simply display:

> True

If you see this formal proof for your smart contract, this means your document has been verified correctly.

In order to check that the verification process has executed correctly, let’s add a bug in our code. We can introduce the bug by editing the buy function:

function buy() public payable {
    require(msg.value != 0);
    require(_hardCap >= _totalSupply + msg.value * _rate);
    if (msg.value == 42)
    {
        return;
    }
    _balances[msg.sender] += msg.value * _rate;
    _totalSupply += msg.value * _rate;
}

If we run the verification now, we’ll get a generic indication of an error. Although the bug is obvious to the naked eye, it would be extremely difficult to catch using conventional unit tests or penetration testing techniques if you didn’t have access to the source code.

Conclusion

Formal smart contract verification is a reliable way to ensure the security of your virtual agreements. It has a few advantages over traditional types of security audits and testing. But it must be carried out by a high-calibre developer who can formalize a security contract as a mathematical high-level specification and refine it for a targeted low-level virtual machine. This procedure is time- and resource-consuming.

Apriorit has a team of professional blockchain experts and security testers who can perform a full set of testing procedures to verify the security of your smart contract. We provide various types of audits, including formal verification. We also conduct penetration testing along with behavioral analysis, providing you with a description of smart contract vulnerabilities and potential solutions for all issues we report.