In this post, we introduce our custom formal verification service. Unlike the Standards-Based Formal Verification service that we described in Formal Verification of ERC-20 Tokens, this service tailors the formal verification for each individual project. It provides a higher degree of security by proving important properties customized for the project’s features and identifying issues that are otherwise difficult to find using other approaches.

Our custom formal verification involves the following steps:

1. Writing Customized Specifications: Security specialists create human and machine-readable specifications using a specification language and annotate them in the contracts under verification.

2. Translation to the Verification Language: CertiK-developed tools translate specifications along with contracts into a verification language that can be verified in a verification framework.

3. Interactive Verification: Formal verification experts verify the specifications in the verification framework.

4. Triaging Results and Creating Reports: Security specialists and formal verification experts iterate on the verification results, create findings accordingly, and post the verification results in the audit reports.

5. Continuous Verification: We repeat steps 1-4 with each revision of the contract code to ensure that identified issues are fixed and new issues are not created.

To deliver the best formal verification service, we have designed our own specification language and utilize a best-in-class formal verification environment. The following subsections describe these two crucial components at a high level.

Specification Language

Our specification language serves as the bridge between security specialists and formal verification experts or tools. It enables security specialists to articulate security properties in a precise and unambiguous manner. Furthermore, it aids formal verification experts and tools in understanding the verification objectives without needing domain knowledge of the contracts under verification. We designed and implemented a specification language for Solidity called BISSOL (Behavioral Interface Specifications for Solidity). This language is both human-readable and machine-readable, drawing inspiration from well-established behavioral interface specification languages such as the Java Modeling Language (JML) and the ANSI C Specification Language (ACSL). BISSOL allows security specialists to collaboratively work on specifications with contract developers, enables formal verification tools to analyze them directly, and supports formal verification experts in interactively verifying them in a verification environment.

Verification Environment

Our verification environment, used to check contracts against the specifications, utilizes Dafny, maintained by Amazon Web Services. We chose Dafny because of its modular verification capability, powerful verification engine, and extensive user community. Dafny enables our formal verification experts to perform deductive verification, a reliable and interactive method for verifying complex systems and software. We have developed parsers, multiple stages of translators, and a suite of Dafny libraries encapsulating the properties of the EVM environment. These tools convert Solidity contracts annotated with BISSOL specifications into Dafny programs, which our experts then verify using the Dafny framework. This verification process is modular and systematic, and we have successfully applied it to a wide variety of Solidity projects, including those with intricate logic and computation.

A Simple Example

In this section, we present a simple example to illustrate how Solidity code specified with BISSOL looks and how it can be verified using Dafny.

A Counter Contract

For this example, we'll examine a smart contract implementing a counter that has two functions: increment and decrement. This smart contract either increases or decreases the state variable count based on certain conditions. Specifically, the increment function increments count by one unless count is 5, and the decrement function decrements count unless its value is either 5 or 1.

BISSOL requires specifications to be written in specification blocks. These start with //@ for single-line specifications and are enclosed within /*@ */ for multi-line specifications. Broadly speaking, verification keywords can be categorized into two main groups: contract-level and function-level specifications.

Contract-level specifications describe the intended behavior of a smart contract, ensuring that certain conditions remain true regardless of individual function executions. These conditions are invariants (statements that should always hold) or constraints (statements that should be true after every function execution). For instance, saying that the equation x * y = k should always hold, or the sum of user token balances should never exceed the total supply, would be an invariant; saying that the number of tokens in the contract can only increase but never decrease would be a constraint.

Function-level specifications, in contrast to contract-level ones, pertain specifically to individual functions within a smart contract. They define the expected behavior, prerequisites, and postconditions of a function's execution.

In our example, we've incorporated two contract-level specifications (as defined in Line 3 and 4). The invariant keyword is used to state predicates that must remain true after the contract's constructor has run, as well as both before and after every function call. In essence, this means that the formal verification will examine whether the specified condition remains intact after the contract's constructor has been invoked and around every function call—both preceding and following its execution. The constraint keyword is used to state conditions that must be true following every function call. The fundamental distinction between constraint and invariant lies in their temporal focus. A constraint is a two-state predicate, allowing for descriptions that encompass the states both before and after a function call. An invariant is a single-state predicate, used to assert conditions that must be true before and after every function's execution. While constraints provide a dynamic perspective, capturing the transitions between states, invariants provide a static perspective, emphasizing unchanging truths.

• The invariant specification dictates that the count variable must always be between 0 and 5, inclusive. This guarantees that, throughout the contract's execution, count can never be negative or exceed 5.
• The constraint specification dictates that once count achieves a value of 1 or higher, it will always maintain a value of at least 1. In other words, after reaching or surpassing this threshold, the value of count cannot drop below 1.

Within the increment and decrement functions, we observe function-level specifications. For the increment function, two distinct specification cases are written, separated by the also keyword. The also keyword allows for the segmentation of multiple behaviors that apply to the same function. The requires clause in each specification case establishes a precondition, effectively stating that the behavior described by the specification case only occurs when this precondition is met. The ensures keyword defines postconditions, indicating that if the function doesn't terminate prematurely (or revert), then the specified condition will be met upon its completion. The assignable keyword specifies which state variables might be altered during the function's operation.

In essence, the first specification case for the increment function clarifies that when count is below 5, the function will guarantee it is incremented by 1. The second specification case for the increment function states that if the count is 5 (checked with precondition), the function always reverts (reverts_when true).

The decrement function has a single specification case with three clauses, which applies universally (since we did not specify a requires, it is assumed to be requires true). First, if count is at 1 or 5, the function reverts, indicating that no decrement operation is feasible. Second, the expression count == \old(count) - 1 ensures that count is decremented by 1 if the function executes successfully. Finally, the expression \result == count confirms that the function's return value matches the new value of count.

When we translate the contract with specifications and verify these specifications in Dafny, Dafny can demonstrate that the contract meets the specifications. This example is small and straightforward, so it does not require manual effort from a verification engineer.

Let's now modify the smart contract and introduce scenarios that violate the specifications. In the revised contract below, the integer type of count shifts from uint256 to int256. Furthermore, the return type of the decrement function is updated to int256. Before examining the implications, we can undertake another verification to assess the outcome:

Upon running the verification tool, we find that one of the postconditions could not be verified. Can you spot why?

The reason lies in the invariant specification: count >= 0 && count <= 5. Since the initial value of count is 0, and the decrement function does not check if count is 0 (it only checks for 1 and 5), decrementing from 0 violates the invariant by reducing count to -1, contrary to the invariant that count should never be less than 0. Let's update the decrement function to include a check for zero as well. Here is the modified decrement function:

Upon rerunning our verification tool with the updated Solidity file, the output confirms that the contract now adheres to the specified conditions.

Recap

requires

• Represents the precondition of a function.
• Specifies the conditions that must be met before the function is called.
• If these conditions are not met, the subsequent specifications won't be valid.

ensures

• Represents the postcondition of a function.
• Specifies what will be true after the function completes its execution.
• If the function doesn't end prematurely or revert, the specified postcondition will be satisfied once the function completes.

assignable

• Identifies the state variables that can be modified or affected during the function's execution.
• States limitations about the potential side effects of the function on the contract state.

reverts_when

• Identifies situations that cause the function to revert.
• States the circumstances under which the function is guaranteed to fail.

\result

• Refers to the return value of the function.
• Allows for writing conditions or specifications about what the function should return.

Application to Real Projects

We have conducted custom formal verification for over 30 client projects, varying in complexity from a single contract with fewer than 100 lines of code to extensive projects comprising hundreds of contracts with more than 12,000 lines of code. Throughout these projects, we have validated over 350 properties and identified more than 20 significant issues. Our security specialists found our specification language BISSOL intuitive and effective for articulating realistic properties crucial for the projects under audit.

We have also applied custom formal verification to projects involved in bug bounties and audit competitions not hosted by us. This process successfully pinpointed issues that were overlooked during manual reviews and by other formal verification tools employed by different audit firms.

Sample Issues Identified by Custom Formal Verification

Incorrect Calculation

Consider the calculateRewardAmount function below with BISSOL specifications stating the expected range of return value of calculateRewardAmount function. Custom formal verification disproved the specification and identified the issue that the function's reward calculation mechanism may result in incorrect reward distributions. This issue arises from the mishandling of the stakeCount and stakeFeatures variables during the staking and unstaking processes.

Risks of Underflow or Overflow

Consider the approve function below with BISSOL specification stating that the function should neither increase minter’s balance nor decrease the spender’s balance. Custom Formal Verification disproved the specification and identified the issue that in the approve function, the operation _accounts[minter].balance -= leftover could cause an underflow if leftover is greater than the minter's balance. This underflow would paradoxically increase the miner's balance to a very high value (type(uint128).max), contradicting the non-mintable nature of the token.

Potential Denial of Service

Consider the swapBack function below with BISSOL specification stating that the function should never revert. Custom formal verification disproved the specification and identified the issue that when _liquidityFeeCount and _reflectionFeeCount are both zero, a divided-by-zero error can occur when calculating amountToLiquify leading to the function reverting. The issue would cause a Denial of Service (DoS) for all functions using swapBack, including transfer and transferFrom functions.

Missing Variable Updates

Custom Formal Verification can also be used to identify the existence of unintended behaviors. Consider the addToStake function below annotated with unintended behavior that the user's reward always remains unchanged. Custom Formal Verification proved that the unintended behavior is true, and identified the issue that when users add stakes to an existing staking plan, the contract only accumulates the accrued rewards and does not adjust the overall reward for the fixed staking plan based on the new total staked amount. This could lead to discrepancies in reward distribution, as the calculated reward is not proportional to the updated staked amount.

Related Work

Certora is a formal verification tool for smart contracts that focuses on automated verification and supports bounded model checking. To use Certora, users must learn their language, CVL, in order to write specifications. This language is expressive but can be hard for non-experts to master. Security specialists found BISSOL easier to learn since it doesn’t require knowledge of verification. Therefore, they can concentrate on writing comprehensive specifications, and leave the verification to the formal verification experts.

K is a formal verification framework that enables deductive verification and interactive theorem proving, similar to CertiK Custom Formal Verification. Its underlying theory and implementation provide a high level of expressiveness, making it suitable for verifying complex programs and algorithms. To use the K framework, formal specifications are written in the K language, which is quite different from Solidity syntax. CertiK designed BISSOL to be similar to Solidity so it is easier to learn and understand, and can be used as a formal behavioral document for the contracts since it is directly annotated on top of target functions or contracts.

Conclusion

This post introduced our custom formal verification service, including its specification language and verification framework. Stay tuned for forthcoming technical deep dives into the results of verifying more live platforms.