Post-Mortem Analysis of the Notional Finance Vulnerability — A Tautological Invariant

Published in

Certora

8 min readJan 17, 2022

Introduction

On January 7, 2022, Notional Finance reported a critical vulnerability prevented in their smart contracts. The vulnerability arose due to a potential double-counting of assets — the same token could appear both as a “bitmap currency” and an “active currency”. This bug slipped through the best auditors in the DeFi space. During development, the Notional team has employed Formal Verification by using the Certora Prover to check an invariant of the system: no asset should ever be marked as both “bitmap” and “active”.

Invariants are properties of program states describing the program’s integrity and thus preventing nasty surprises. The utility of invariants for program safety has been widely recognized since the beginning of Computer Science. Invariants play an important role in DeFi security since “code is law”, and everybody can execute code with no ability to revert transactions. Thus, when an invariant is violated, all bets are off, as undesired behaviors become possible from a violating state. Invariants can either be enforced dynamically via runtime checks or proved statically before the code is deployed via Formal Verification tools like the Certora Prover.

The invariant that the Notional Finance team wrote and checked in their code was unfortunately not describing the property the developers had in mind. Due to a logical error, the invariant was vacuous, i.e., there was no way to violate it. It thus showed up as “verified” in the output of the Certora Prover.

A white-hat hacker has since reported that the code is vulnerable by reaching a program state that was expected to be infeasible. As soon as we received the report from the Notional Finance team, we studied the original invariant and corrected it to describe the original intention of the developers. We confirmed that the correct invariant could have flagged the issue beforehand.

In this post, we describe both the wrong and correct invariants and the lessons learned. In particular, we discuss our soon-to-be-coming improvements to the tool to prevent such situations in the future.

The state of the Notional Finance system

An asset (or currency) deposited to an account in Notional can belong to either one of two types: “bitmap”, which has to be explicitly enabled using the enableBitmapCurrency method, and “active”, which is the automatic group to which an asset is assigned. It is expected that if a user calls enableBitmapCurrency, the system will ensure the asset is no longer marked as an “active” currency.

Assets are represented using 14 bits. Each asset can have up to two flags set for it, and so it takes up to 16 bits (or 2 bytes) in storage. Each account is associated with a bitmapCurrencyId field of type uint16 and an activeCurrencies field of type bytes18 (i.e., 144 bits) holding up to 9 assets.

For the state to be correct, the non-zero, 14-bit value representing the asset in bitmapCurrencyId must not appear in any of the slots of activeCurrencies.

The Vacuous Invariant

The original invariant that was written to describe the idea of non-intersecting assets was as follows:

// WRONG INVARIANT
invariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(
    address account, 
    uint144 i
)
    0 <= i && i < 9 && getBitmapCurrency(account) != 0 &&
        (
            // When a bitmap is enabled it can only have currency masks
            // in the active currencies bytes
            (hasCurrencyMask(account, i) && getActiveUnmasked(account, i) == 0) ||
                getActiveMasked(account, i) == 0
        ) => getActiveUnmasked(account, i) != getBitmapCurrency(account)

The invariant is taking an account and an index in activeCurrencies, and is expected to check that the currency in the ith index is not equal to the bitmap currency (the right-hand side of the implication, or the conclusion): getActiveUnmasked(account, i) != getBitmapCurrency(account). The left-hand side of the implication (the premise) was expected to set some natural requirements, e.g., that the index should be between 0 and 9. The invariant uses two auxiliary definitions for looking at the currency stored in slot i, one that includes just the 14 bits of the currency (getActiveUnmasked), and one that includes the flags (getActiveMasked).

However, closer inspection of the invariant shows that the conclusion follows trivially from the premise. In the premise, we first note that the bitmap currency must be non-zero. We then analyze each disjunct (element of the “or” expression) separately:

hasCurrencyMask(account, i) && getActiveUnmasked(account, i) == 0: this tells us that the currency ID of interest (active unmasked currency ID in slot i) is zero. Combined with the information that the bitmap currency is non-zero, it follows that the currency ID we examine is not the bitmap currency. So the conclusion, therefore, follows immediately.
getActiveMasked(account, i) == 0: we note that in the spec, the getActiveMasked definition returns more bits than getActiveUnmasked (16 bits instead of just 14). Therefore, if getActiveMasked(account, i) == 0 it must be the case that getActiveUnmasked(account, i) is also zero. The conclusion follows trivially by a similar argument to the previous case.

Therefore, it follows that the conclusion cannot ever be false if the premise is true. When the Certora Prover checks this invariant, it tries to find a concrete input and state such that:

Before executing some public method in the code, the conclusion follows from the premise.
After executing some public method in the code, the premise is true, but the conclusion is false.

However, such an input state cannot exist, as the conclusion follows from the premise on all inputs and regardless of what method is executed.

We realized that the invariant was vacuous and could not be used to find the vulnerability that existed in the code.

Less is More

We came up with a correct formalization of the desired property in a simple form:

invariant bitmapCurrencyIsNotDuplicatedInActiveCurrencies(
    address account, 
    uint144 i
)
  0 <= i && i < 9 
         && getActiveUnmasked(account, i) != 0 
         && hasCurrencyMask(account, i) 
              => getActiveUnmasked(account, i) != getBitmapCurrency(account)

It requires that given an account and index into activeCurrencies between 0 and 9, if the unmasked currency is non-zero, and the “active” flag is set for it, it must be different from the bitmap currency.

We ran the revised invariant on the method exposing the vulnerability, enableBitmapForAccount, and received the expected violation of the rule.
In the pre-state before executing the method, we note that the bitmap currency is 0, and 0x3ffe is the active currency in slot 8 (the last one in activeCurrencies). We also see that since the last 2 bytes in activeCurrencies are 0xfffe, the “active” flag is set. In the post-state, 0x3ffe is now set as the bitmap currency, but the active currencies stay the same, meaning that 0x3ffe is also an active currency. From this state, double spending would be possible, allowing an exploit.

Upon releasing the suggested hotfix to the Notional code, we ran the revised invariant on it, and it successfully proved the code correct. The relevant verification reports with the output of the tool can be found here and here. The full revised spec is available as well.

Checking Vacuity

Sometimes it is indeed hard to formalize rules correctly. Nevertheless, it is possible to check ourselves when writing rules and ensure that we are not missing our intended meaning.

In our case, we could take the incorrect invariant and assert it as a rule. If this rule is verified, it means there is no state in the system that ever violates the invariant, meaning there is nothing to check:

rule verifiedIfInvariantIsVacuous(address account, uint144 i) {
    assert 0 <= i && i < 9 && getBitmapCurrency(account) != 0 &&
        (
            // When a bitmap is enabled it can only have currency masks
            // in the active currencies bytes
            (hasCurrencyMask(account, i) && getActiveUnmasked(account, i) == 0) ||
                getActiveMasked(account, i) == 0![]        ) => getActiveUnmasked(account, i) != getBitmapCurrency(account);
}

A good invariant helps separate the states between good and bad states. A bad invariant contains all states.

The problem of vacuity is long-standing in the field of formal verification, not just in software verification, but in fact going back to hardware verification. Several techniques have been developed for automatic vacuity checks[1]. If a vacuity check fails, a warning is displayed to the programmer. We plan to integrate such methods in the near future.

Another useful technique that anybody can employ today is to manually add bugs to the code, with the goal of breaking rules we have written. If we do not receive reports of violations of our rules by adding such bugs to the code, perhaps the rules have been formalized incorrectly.

Better Specs for Better Security

The vulnerability found in the Notional Finance code has slipped through some of the best auditors and the talented team of Notional Finance. Notional has taken extensive precautions to shield its code using different layers: auditing, Formal Verification, and bug bounties. There is no silver-bullet when it comes to security, and we are forever learning how to improve.

Multiple layers of security are good, but do not guarantee 100% protection. Certora rules were not checked in this incident, but they could easily be tested and audited to avoid the security hole.

The utility of formal specification for code safety is well understood. However, getting specifications right can get as tricky as getting the code right. We are suggesting the following measures to improve the security of the specifications and the code:

Audit the specifications. Good specifications are easy to read and review. We note that the corrected specification is more readable. Certora plans to engage with external auditors to review the rules. This is depicted in the figures.
Open bug bounties to uncover specification issues and not only code issues.
Develop technologies for checking specifications. We have already implemented sanity checks to ensure that every assertion in a rule is reachable (that it contains no require(false) or logically-equivalent statements). We are now implementing a check for invariants, as explained above.
Integrate testing tools for specifications and, in particular, mutation testing.

Rules should be scrutinized just like code. The Certora Prover can then provide very high coverage against bugs.

Takeaways

Our conclusions from this incident are:

A code without specification is like a house without a plan.
Writing formal specifications is hard and requires careful thought and tooling.

A famous quote by D. Knuth is

Some tasks are best done by machine,
while others are best done by human insight;
and a properly designed system will find the right balance.

We are trying to find the right balance to simplify the verification task with the Certora Prover. We are now adding checks to human written invariants. In the future, the computer would suggest useful invariants for common financial transactions.

Acknowledgements

We thank the Notional Finance team for their prompt notification about the issue and their honesty and transparency.

Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh:
Efficient Detection of Vacuity in Temporal Model Checking. Formal Methods Syst. Des. 18(2): 141–163 (2001) ↩︎