# Post-Mortem Analysis of the Notional Finance Vulnerability - A Vacuous Invariant

## Introduction
On January 7, 2022, [Notional Finance reported about a critical vulnerability prevented in their smart contracts](https://blog.notional.finance/critical-bug-payout-report/).
The vulnerability arised due to a potential double-counting of assets, as the same asset could appear both as a "bitmap currency" and an "active currency".
The Notional team was aware during development that no asset should never be marked both as "bitmap" and "active", and has employed Formal Verification and the Certora Prover by writing an _invariant_ whose declared purpose was to check that such a state could never be reached.

Invariants are properties of program states describing the integrity of the program and thus preventing bad surprises. The utility of invariants for program safey is widely recognized since the beginning of Computer Science. Invariants play an important role in DeFi security since "code is law" and code can be executed by everybody with no ability to revert transactions. Thus, when an invariant is violated, all bets are off.
Invariants can either be enfored dynamically via runtime checks, or proved statically before the code is deployed via formal verification tools like the [Certora](https://www.certora.com) 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 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, corrected it to describe the original intention of the developers, and 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 would ensure the asset is no longer marked as an "active" currency.

In particular, 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 with an `activeCurrencies` field of type `bytes18` (i.e., 144 bits), which holds up to 9 assets.

For the state to be correct, a 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 dsecribe 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 `i`th 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 would show that the conclusion follows trivilly from the premise.
In the premise, we first note that it must be that the bitmap currency is non-zero. We then analyze each disjunct 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 0. Combined with the information that the bitmap currency is non-zero, it follows directly 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.

It therefore follows that the conclusion cannot be ever 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.

# A Corrected Invariant
Once

# The Certora Prover

The Certora prover checks invariants before the code is executed.
The Solidity code is compiled into EVM code using the Solidity compiler.
Then the EVM code and the invariant is compiled into mathematical constraints. These constraints are solved using existing solvers.

SHOW THE VIOLATED STATE
# Lessons Learned

One of the hardest problems in computer science is coming up with invariants. This requires careful thoghts about the system. The original invariant was almost right but vacoues.

The Certora prover can be used to check that an invariant holds on all executions before the code is deployed.
We are now adding checks to detect vacous invariants like these invariants.
We plan to warn developers againts two types of vacoues rules:
1. Vacoues asserts and invariants. We check that there exist no state that violate the invariant. A simple vacoues invariant is *A-->A* or $A /\ !A$
2. Vacous require statements. There exists no state which satisfies the expression. A simple exmple is $5> 7$ or $A /\ !A$.

Both of cases can be easily prevented using the Certora prover before the code is verified.

# Ackoledgements