Formal verification is a method of mathematically proving that a computer program functions as intended. It involves expressing the program's properties and expected behavior as mathematical formulas, and then using automated tools to check that these formulas hold true. This process helps ensure that the program meets its desired specifications.

Formal verification is a tool that can be applied to many systems, including:

Formal Verification of Smart Contracts

Formal verification of smart contracts works by representing the logic and desired behavior of smart contracts as mathematical statements, and then using automated tools to check if these statements are correct.

The process involves:

Sometimes the automated theorem provers or model checkers cannot prove or disprove that a property holds true. In this case, the specifications and desired properties may need to be refined and the verification process repeated.

The specifications and desired properties can be refined by applying more specifications to smaller pieces of code or making the specifications more detailed. This can make it easier for the theorem provers and model checkers to validate that specifications and properties hold true.

Formal verification can be applied to one contract or to multiple contracts at a time. Web3 projects often use multiple contracts, and it is important to make sure that the contracts work together and implement the desired project functionality correctly.

This use of mathematical reasoning helps to ensure that smart contracts are free from bugs, vulnerabilities, and other unintended behavior. It also helps to increase trust and confidence in the contract, as its properties have been rigorously proven to be correct.

Translating code into a formal representation

Code Snippet 1 shows a simplified program that implements a token transfer function. There are two users that each have a balance of tokens (balance and balance2). The function transferFromUser1 transfers tokens from User 1 to User 2. The program has an invariant that the total supply of tokens always equals the sum of the balances.

uint balance1;
uint balance2;
uint totalSupply;

// Transfer money from User 1 to User 2.
function transferFromUser1(uint amount) {
    balance1 = balance1 - amount;
    balance2 = balance2 + amount;
}

Code Snippet 1: A simple program illustrating a transfer

We represent the invariant as a mathematical formula. We number formulas to keep track of them. Because formulas are mathematical, = means “equals”, not assignment, in them:

Formula 1: totalSupply =  balance1 + balance2     // sum of balances

Code Snippet 2 shows how we can add logical formulas representing what is true at each point in the function (for simplicity, we ignore the possibility of integer overflow. Handling that would make the formulas much longer).

function transferFromUser1(uint amount) {

  // Formula 1: totalSupply = balance1 + balance2

  balance1 = balance1 - amount;

  // old(balance1) represents the value of balance1 when entering the function.
  // Formula 2: totalSupply = old(balance1) + balance2
  // Formula 3: balance1 = old(balance1) - amount // implied by the assignment
  // Formula 4: Formula 2 ^ Formula 3

  balance2 = balance2 + amount;

  // old(balance2) represents the value of balance2 when entering the function.
  // Substitute old(balance2) into Formula 4, replacing balance2.
  // Formula 5: (totalSupply = old(balance1) + old(balance2)) ^
  //            (balance1 = old(balance1) - amount)
  // Formula 6: balance2 = old(balance2) + amount   // implied by the assignment
  // Formula 7: Formula 5 ^ Formal 6.
  // Formula 7 expands to:
  //            (totalSupply = old(balance1) + old(balance2)) ^
  //            (balance1 = old(balance1) - amount) ^
  //            (balance2 = old(balance2) + amount)
}

Code Snippet 2: Function with logical formulas representing the meaning of the code.

If we want to check that transferFromUser1 maintains the program invariant, we can check that Formula 7 (at the end of the function) implies the invariant (Formula 1). Here is the proof, using high-school algebra simplification rules.

Assume Formula 7 is true 
Solve for old(balance1) and old(balance2) using the last 2 clauses of Formula 7:
  old(balance1) = balance1 + amount
  old(balance2) = balance2 - amount
Substitute that into the first clause of Formula 7:
  totalSupply = (balance1 + amount) + (balance2 - amount)
Cancel addition and subtraction of amount:
   totalSupply = balance1 + balance2

How formal verification and manual auditing work together

Formal verification and manual auditing complement each other in ensuring the security of smart contracts.

Formal verification provides a systematic and automated way to check the contract's logic and behavior against its desired properties, making it easier to identify and fix any potential errors or bugs. It is especially useful for finding complex and subtle issues that may be difficult to detect through manual inspection. When dealing with complex or multiple contracts, it can become difficult for a human to reason about all the possible combinations and cases that need to be checked. Machines, however, are well-suited to this task.

Manual auditing provides a human expert review of the contract's code, design, and deployment. The auditor can use their experience and expertise to identify potential security risks and evaluate the contract's overall security posture. They can also verify that the formal verification process was performed correctly, and check for issues that may not be detectable with automated tools. Their expert insight helps ensure that the specifications and desired properties used in formal verification are indeed the right ones.

Combining formal verification and manual auditing provides a comprehensive and thorough evaluation of a smart contract's security, increasing the chances of finding and fixing any vulnerabilities. The result is a defense-in-depth approach to security that leverages the unique capabilities of both humans and machines.

Conclusion

This is an overview of what formal verification is and how it can be applied to increase the security of smart contracts and decentralized applications. Stay tuned for a forthcoming technical deep dive into the formal verification of ERC-20 tokens.

Read more: https://www.certik.com/resources/blog/3UDUMVAMia8ZibM7EmPf9f-what-is-formal-verification