Finding Bugs in Formal Specifications

Formal verification can drastically improve code security when done right. However, it can also miss bugs if the formal specification doesn’t describe important properties of the system. A partial specification may give the false impression that your code behaves as expected and lead to the deployment of buggy code. As a recent example, a critical bug was found in Notional, a formally verified code base, even though the specification seemed to show that the bug was impossible. This blog will explain some common errors in specifications and how to avoid them.

Background — why do we need formal specifications?

Hundreds of millions of dollars are lost each year due to smart contract bugs. The irreversible nature of blockchains makes them a prime target for attacks by hackers. In their quest to prevent catastrophic bugs, more and more DeFi protocols use formal verification to complement testing, manual audits, and bug bounties.

In formal verification, we try to prove that a computer program behaves as expected. We first convert the program to a logical formula, then use mathematical methods to prove it. Formal verification is attractive to developers because, unlike testing tools, it exhausts all possible code paths and can find rare edge cases. Formal verification can also prove the absence of specific classes of bugs.

However, we must keep in mind that formal verification is only as good as the specification of the system. A specification consists of rules — properties we expect the code to adhere to. Unfortunately, some rules do not check anything, and will always pass, regardless of the program’s code. We call them vacuous rules.

Vacuous rules are dangerous because they give the developers false confidence in their system and might lead to premature deployment of buggy contracts. Vacuous rules are surprisingly common. Let’s look at a few types of vacuous rules and how we can detect them.

Vacuous preconditions

By default, when a rule is verified, we try to prove it holds from any arbitrary state of the contract — the Certora prover will consider any values of contracts’ storage and function inputs to be possible. This leads to many false violations of rules, where the chosen values are uninteresting, cause undefined behavior, or cannot be reached by calling the contract’s methods.

For example, consider a function f(y) that returns the ceiling of 1/y. This function should clearly return a value greater than 0. The following rule describes this expectation:

When y=0, the function is not well-defined since division by zero is not allowed, so we must limit the possible inputs. To do so, we define a precondition — all initial states that do not pass this condition are ignored. In the Certora Verification Language, also called CVL, we add preconditions with the keyword require.

While preconditions are a necessity, sometimes a combination of them can entirely rule out all possible counter-examples. When this happens, the verification will prove the rule because no counter-examples could be found, even if what we try to prove is false. For example, the following rule is vacuous:

The assertion is obviously false, as no number is smaller than itself. However, the first require statement ruled out all values of x smaller than two, and the second ruled out all the values greater than one. There are no values of x left to use to disprove the assertion.

The Certora Prover detects vacuous preconditions by removing all user assertions and adding an assert false at the end. If the rule is vacuous, the assertion will never be reached, and the rule will be proven. Otherwise, at least one input and state get to the final assertion, and the Prover will find a counterexample. If the Prover fails to find a counterexample, it knows the rule is vacuous and reports a warning to the user.

For example, the previous rule will become the following during the reachability check:

Unbounded asserts

While we have seen how preconditions can rule out all possible counter examples, another common problem is when they rule out no counter examples. An assertion that can be verified regardless of the preconditions is unbounded. Consider the following rule:

The first assertion is bounded — if we allow x to be 2 or greater, the assertion will fail. Similarly, if we ignore the if condition and let y be 2 or greater, the first assertion will also be violated. However, the second assertion is unbounded by either the require or the if conditions; even if x or y could get any possible values, the assertion would still hold.

Certora has an automatic check that flags unbounded assertions. Their presence means that the specification is not as strong as it could be. For example, in the above case, we can prove the following two rules instead:

The rule max_sanity proves that the assertion z >= x in more scenarios than one_assert_is_unbound did. The assertion of z < 2 is proven for the same variable inputs as it did in the rule one_assert_is_unbound. Hence, overall, the specification covers more possibilities without the unbounded assertion.

Be careful that your unbounded assertions are not tautologies. A tautology is a statement that is always true, regardless of the code we try to verify. An example of a tautological sentence is “the ball is green or not green”; it is true no matter what color the ball is. A tautology is a form of a vacuous assertion. Let’s look at an example.

X is always either smaller than two, greater than, or equal to two. Thus, the assertion expression is a tautology and proves nothing about the code. As with any tautology, this assertion would be flagged by an unbounded assertion check.

Redundant preconditions

Another pitfall when writing rules are redundant preconditions. A redundant precondition does not rule out any counterexamples that violate the rule, and is fruitless. For example:

In this rule, the second require statement is redundant — every counter-example it rules out has already been excluded by the first require. Redundant preconditions hint at logical bugs in the specification. The Certora prover finds redundant require statements by removing them from the rule; if the rule is still proven, then these requires are redundant.

Don’t trust the specification

When using automatic tools, some level of paranoia is always recommended. Do not blindly trust formal verification! Be suspicious of your specifications. Ask yourself if your rules are vacuous. Insert bugs in your code, and see that your specification is violated.

Use automatic checks, like those implemented by the Certora prover. For performance, Certora’s checks are not enabled by default; don’t forget to run them before deployment! There are more types of vacuous rules not covered by this article. The Certora team is working on implementing more types of vacuity checks to catch them all.

Certora is also currently testing a new automated mutation tester. If a mutated source program also meets the specification, that could be a sign that the specification misses essential properties of the system. Together with vacuity checking, mutation testing provides more confidence in the specs and helps strengthen them. Stay tuned for updates!