Formal verification techniques can be applied to many systems, including:
Computer hardware design: Ensuring that integrated circuits and digital systems meet their desired property specifications and behave correctly.
Software engineering: Verifying the correctness and reliability of software systems, especially in mission-critical applications such as aviation, medical devices, and financial systems.
Cybersecurity: Evaluating the security of cryptographic algorithms and protocols, and identifying vulnerabilities in security-sensitive systems.
Artificial intelligence and machine learning: Verifying the properties and behavior of AI and ML models, ensuring that they operate as intended and make accurate predictions.
Automated theorem proving: Verifying mathematical theorems and proving mathematical conjectures, which have applications in fields such as mathematics, physics, and computer science.
Blockchain and smart contracts: Ensuring the correctness, security, and reliability of blockchain systems and smart contracts.
Formal Verification of Smart Contracts
Formal verification of smart contracts works by representing the logic and desired behavior of smart contracts as mathematical statements. Then, auditors use automated tools to check if these statements are correct.
The process involves:
- Defining the specifications and desired properties of a contract in formal language.
- Translating the code of the contract into a formal representation, such as mathematical models or logic.
- Using automated theorem provers or model checkers to validate that the specifications and properties of the contract hold true.
- Repeating the verification process to find and fix any errors or deviations from the desired properties.
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 formal methods may need to be repeated.
The specifications and desired properties can be refined by applying more specifications to smaller code segments or by making the specifications more detailed. This can make it easier for theorem provers and model checkers to verify that requirements and properties hold.
Formal verification can be applied to a single contract or multiple contracts simultaneously. Web3 projects often use multiple contracts, and it is essential to make sure that the contracts work together and implement the desired project functionality correctly.
This use of mathematical reasoning helps to ensure that formally verified smart contracts are free from bugs, vulnerabilities, and other unintended behavior. It also helps increase trust and confidence in the contract, as its properties have been rigorously proven correct.
Translating code into a formal representation
Code Snippet 1 shows a simplified program that implements a token transfer function. There are two users who 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, automated way to verify the contract's logic and behavior against its desired properties. This makes it easier to identify and fix any potential errors or bugs. It is beneficial 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 identify issues that automated tools may not detect. 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 evaluation of a smart contract's security. This increases the chances of finding and fixing any vulnerabilities. The result is a defense-in-depth security approach that leverages the unique capabilities of both humans and machines.
Conclusion
This article serves as an introduction to formal verification and its application to enhance the security of smart contracts and decentralized applications. Stay tuned for a forthcoming technical deep dive into the formal verification of ERC-20 tokens.
