About Certora Prover
Certora has been the only team that offers Prover Technology for verifying security rules, which includes the following properties:
- Minimal false alarms: Certora Prover ensures that the reported errors are real
- Formal correctness guarantees: Certora Prover makes sure that there are no missed alarms for proven rules
- Fully automatic: Users do not have to intervene while Certora Prover is processing
- Agile: Certora Prover supports arbitrary programs and integrates into CI/CD pipeline
The Certora Prover is built on well-researched formal verification techniques. Here is the workflow:
Specifications are a set of rules that invoke the contract under investigation and make various assertions about its behavior. These rules are combined with the contract under analysis to generate a logical formula known as a verification condition, subsequently proved or disproved by an SMT solver. The solver also gives a concrete test case indicating the violation in case the rule is disproved.
In the analysis, the specification rules are quite important. Only the most fundamental properties can be examined without suitable rules (e.g., no assertions in the contract itself are violated). Users must develop rules that explain the high-level properties they want to test on their contracts to use Certora Prover efficiently. The different aspects of the specification language are described in this user handbook. Another purpose is to assist the reader in understanding and writing high-level properties.
The purposes (the needs) of this instruction
[Purpose 1] Ensuring Smart Contract Security
As the title of this blog and Certora Prover’s slogan, its most significant and straightforward purpose is to ensure that users' smart contracts are safe. In comparison to traditional software development, smart contract development has a significantly higher demand for code security since smart contracts often handle sensitive digital assets (e.g., cryptocurrencies, tokens, digital art files, etc.). Transactions on blockchains are irreversible, and the code of smart contracts cannot be modified after deployment. Moreover, it is more difficult to guarantee security in smart contracts than in other types of software because the smart contract's code is always publicly accessible (therefore, anyone can try to exploit the code, design an attack, and execute it). Another element that makes code security difficult to ensure is the compiler itself. Compilers for smart contracts are not as advanced as compilers for standard programming languages. And also, there is a lack of best practices for writing safe code and tools/techniques to verify code correctness.
[Purpose 2] Taking advantage of the Prover Technology
As being said above, Certora is the only team that provides Prover Technology for smart contracts. But what is Prover Technology exactly? Prover Technology is a formal verification technique (formal verification is the process of proving or disproving the correctness of specified algorithms underpinning a system concerning a formal specification or property using formal mathematics methods). Formal verification has been a useful way to ensure the security of traditional software programs, so it is a promising technique to protect smart contracts.
[Purpose 3] Making it easier to use Certora Prover
Last but not least, like every other instruction, we want to help readers use Certora Prover. Although Certora Prover’s guide is already pretty specific, we still want to ensure that no one will be confused using Certora Prover.
Instructions
[Step 1] Install Certora Prover
Follow installation steps in Installation of Certora Prover - Certora Prover Documentation - Confluence (atlassian.net).
[Step 2] Writing the specification
Write specific rules that you want your smart contract to follow. You can learn how to write a specification in Specification By Example - Certora Prover Documentation - Confluence (atlassian.net).
Let’s say that you have a smart contract which is called Bank.sol as follow:
pragma solidity ^0.7.0;
contract BankBroken {
// mapping from a user to its balance
mapping (address => uint256) private funds;
// total funds in the bank
uint256 totalFunds;
// deposit amount into bank and update the user's balance in the bank accordingly
function deposit(uint256 amount) public payable {
funds[msg.sender] += amount;
totalFunds += amount;
}
//
function transfer(address to, uint256 amount) public {
require(funds[msg.sender] > amount);
uint256 fundsTo = funds[to];
funds[msg.sender] -= amount;
funds[to] = fundsTo + amount;
}
// withdraw the total balance of user into its personal wallet address
function withdraw() public returns (bool success) {
uint256 amount = getFunds(msg.sender);
funds[msg.sender] = 0;
success = msg.sender.send(amount);
totalFunds -=amount;
}
// retrieves the user's recorded balance in the bank
function getFunds(address account) public view returns (uint256) {
return funds[account];
}
// retrieves the total funds that the bank stores
function getTotalFunds() public view returns (uint256) {
return totalFunds;
}
// retrieves the account's ETH balance in its personal wallet address
function getEthBalance(address account) public view returns (uint256){
return account.balance;
}
}
*Source code is taken from Certora Online Editor
And here is a rule for verifying that withdrawal either revert or returns true.
rule withdraw_succeeds {
/* The env type represents the EVM parameters passed in every
call (msg.*, tx.*, block.* variables in solidity */
env e;
// Invoke function withdraw and assume it does not revert
/* For non-envfree methods, the environment is passed as the first argument*/
bool success = withdraw(e);
assert success, "withdraw must succeed";
}
The rule calls to withdraw with an arbitrary EVM environment (e) in an arbitrary initial state. It assumes that the function does not revert. The assert command checks that success is true on all potential executions. Notice that each Solidity function has an extra argument, which is the EVM environment.
To simulate the execution of all functions in the contract, you can define a method argument in the rule and use it in invocation statements. For example:
rule others_can_only_increase_my_balance() {
method f; // an arbitrary function in the contract
env e; // the execution environment
address other;
// Assume the actor and the other address are distinct
require e.msg.sender != other;
// Get the balance of `other` before the invocation
uint256 _balance = getFunds(other);
calldataarg arg; // any argument
f(e, arg); // successful (potentially state-changing!)
// Get the balance of `other` after the invocation
uint256 balance_ = getFunds(other);
assert _balance <= balance_, "Reduced the balance of another address";
}The Prover verifies that the conditions hold against any function call with any arguments.
[Step 3] Start a verification
When starting the verification, you will be prompted to set the configurations, such as the main contract name, solidity compiler version, etc. These configurations will be stored in a local configuration file in the conf subfolder. You can edit the configuration file manually or create a new one (clicking on the Create Certora IDE conf file button).
The conf file will be used to start the verification process. Next, use the VS Code Command Palette (Ctrl/Cmd + Shift + P) to trigger the Certora Run Script command or simply click the Run Certora IDE button.
Alternatively, you can follow the instructions in Running The Certora Prover - Certora Prover Documentation - Confluence (atlassian.net).
[Step 4] Results
After approving the request using the specified access key, the program submits the work to Certora's server. The command line will get messages alerting it of its progress. It's worth noting that the job will continue to run even if you interrupt it. An email message is issued with links to the findings when the verification is complete.
The output will additionally include links to the results in case the CLI tool is not interrupted:
Status page: https://prover.certora.com/jobStatus/...?anonymousKey={anonymousKey}
Verification report: https://prover.certora.com/output/...?anonymousKey={anonymousKey}
Full report: https://prover.certora.com/zipOutput/...?anonymousKey={anonymousKey}
Follow these links to view the results.
The results might look like this:
A verification report is an HTML file that displays all the spec file rules in a table. A green hue is assigned to each officially proven rule. Rules that have been broken are shown in red. The call trace and arguments that led to the violation will also be included in the report. The Certora Prover discovers a violation of the monotone rule in this case. To examine the call trace and try to figure out the reason, click the rule.
References
[1] Certora website, accessed March 19th, 2022.
[2] Certora Prover Documentation, certora.atlassian.net, accessed March 19th, 2022.
[3] Installation of Certora Prover, Certora Prover Documentation, accessed March 19th, 2022.
[4] Specification By Example, Certora Prover Documentation, accessed March 19th, 2022.
[5] W. Zou et al., Smart Contract Development: Challenges and Opportunities, accessed March 19th, 2022.
[6] Introduction to Formal Verification, Berkeley University of California, accessed March 19th, 2022.