The main challenge encountered when formally verifying software properties is convincing the verification tool that an "obviously true" property really is true. In this case the problem was the opposite. The Move Prover accepted a specification we assigned to a contract function, but when we double-checked the specification by deliberately introducing a bug in the code, the Prover said the buggy code was also correct.

The problem was with the specifications in the code, not the Prover. The old adage of “Who will watch the watchers?” applies here. How do we know the specifications are correct and how do we know we are proving what we intended to prove?

The code in question looked something like this (simplified for demonstration purposes):

module 0x1234::mycoin {
  use std::string;
  use std::signer;
  use aptos_framework::coin::{Self, MintCapability};

  struct MyCoin has key, store {}
  struct CapStore has key {
    mint_cap: MintCapability<MyCoin>,
  }

  const E_PERMISSION: u64 = 0;

  public entry fun init(account: &signer) {
    // Validate the account is the module owner
    assert!(signer::address_of(account) == @0x1234, E_PERMISSION);

    // Initialize a new coin with the Aptos framework
    let (burn_cap, freeze_cap, mint_cap) = coin::initialize<MyCoin>(
      account, string::utf8(b"MyCoin"), string::utf8(b"MYCN"), 8, true
    );

    // Store the mint capability and drop the others
    move_to(account, CapStore { mint_cap });
    coin::destroy_burn_cap(burn_cap);
    coin::destroy_freeze_cap(freeze_cap);
  }
}

This is a fairly standard Move contract that initializes a custom instance of the generic Aptos Coin and grants the owner permission to mint more coins. A reasonable specification for init, captured by the following spec block, is that account owns a CapStore resource after its successful execution.

spec init { ensures exists<CapStore>(signer::address_of(account)); }

What does the Move Prover have to say about this?

$ move prove [INFO] preparing module 0x1234::mycoin [INFO] transforming bytecode [INFO] generating verification conditions [INFO] 1 verification conditions [INFO] running solver [INFO] 0.239s build, 0.212s trafo, 0.004s gen, 0.612s verify, total 1.065s

Success! But just to be sure, what happens if we change the following line? From this:

move_to(account, CapStore { mint_cap });

To this:

coin::destroy_mint_cap(mint_cap);

Now our specification definitely shouldn’t be provable, so let’s check with the Prover again.

$ move prove [INFO] preparing module 0x1234::mycoin [INFO] transforming bytecode [INFO] generating verification conditions [INFO] 1 verification conditions [INFO] running solver [INFO] 0.243s build, 0.194s trafo, 0.004s gen, 0.603s verify, total 1.044s

It still managed to “verify” our specification, but we know this is wrong. In fact, it turns out we can write any postcondition we want.

spec init { ensures false; }

So was the Prover broken? No. Its behavior was entirely sound, but a bit unintuitive. We can see exactly what’s going on if we enable two very useful flags: --check-inconsistency and --unconditional-abort-as-inconsistency. The first flag tells the Prover to look for inconsistencies; that is, sets of assumptions that are impossible to satisfy simultaneously. For example, x < 0 and x > 0. The second flag says to treat any function that always aborts as an inconsistency. Any code that comes after a call to such a function is unreachable. We can assume whatever postcondition we want. This is the formal logic version of “garbage in, garbage out”.

Turning these on gives us some insight into the problem.

$ move prove -- –check-inconsistency --unconditional-abort-as-inconsistency [INFO] preparing module 0x1234::mycoin [INFO] transforming bytecode [INFO] generating verification conditions [INFO] 2 verification conditions [INFO] running solver [INFO] 0.264s build, 0.218s trafo, 0.008s gen, 0.665s verify, total 1.154s error: there is an inconsistent assumption in the function, which may allow any post-condition (including false) to be proven ┌─ ./sources/mycoin.move:13:3 │ 13 │ ╭ public entry fun init(account: &signer) { 14 │ │ // Validate the account is the module owner 15 │ │ assert!(signer::address_of(account) == @0x1234, E_PERMISSION); 16 │ │ · │ 25 │ │ coin::destroy_freeze_cap(freeze_cap); 26 │ │ } │ ╰───^ Error: exiting with verification errors

The prover reports an “inconsistent assumption”. If we remove the --unconditional-abort-as-inconsistency flag, the warning goes away. This means that the Prover has detected that init will always abort. Another way to check that the Prover thinks the function unconditionally aborts is by verifying the init function against a specification that explicitly says this:

spec init { aborts_if true; }

This explains why our intentional bug still passed verification, but why does the Prover decide that the init function always aborts? Fortunately, init isn’t a very long function, and with some experimentation and educated guesses we fairly quickly ruled out everything except coin::initialize. Digging into the Aptos source code, we eventually came to the following function (as of this commit):

fun initialize_internal<CoinType>(
  account: &signer,
  name: string::String,
  symbol: string::String,
  decimals: u8,
  monitor_supply: bool,
  parallelizable: bool,
): (BurnCapability<CoinType>, FreezeCapability<CoinType>, MintCapability<CoinType>) 
{
  let account_addr = signer::address_of(account);

  assert!(
    coin_address<CoinType>() == account_addr,
    error::invalid_argument(ECOIN_INFO_ADDRESS_MISMATCH),
  );

  assert!(
    !exists<CoinInfo<CoinType>>(account_addr),
    error::already_exists(ECOIN_INFO_ALREADY_PUBLISHED),
  );

  assert!(
    string::length(&name) <= MAX_COIN_NAME_LENGTH,   
    error::invalid_argument(ECOIN_NAME_TOO_LONG)
  );
  assert!(
    string::length(&symbol) <= MAX_COIN_SYMBOL_LENGTH,     
    error::invalid_argument(ECOIN_SYMBOL_TOO_LONG)
  );

  let coin_info = CoinInfo<CoinType> {
    name,
    symbol,
    decimals,
    supply: 
      if (monitor_supply) { 
        option::some(optional_aggregator::new(MAX_U128, parallelizable)) 
      } else { 
        option::none() 
      },
  };
  move_to(account, coin_info);

  (
    BurnCapability<CoinType> {}, 
    FreezeCapability<CoinType> {}, 
    MintCapability<CoinType> {}
  )
}

There’s a lot here, but the important part is this assertion:

assert!( coin_address<CoinType>() == account_addr, error::invalid_argument(ECOIN_INFO_ADDRESS_MISMATCH), );

This is checking that account_addr (which comes from the same account variable in our init function) is the same address that owns the module in which CoinType (MyCoin in this case) is defined. Looking back at init, we can see that this should be guaranteed by the assertion just before the call to coin::initialize, so how does this assertion fail? For the answer, we have to look at the specification for coin_address.

spec coin_address {
  pragma opaque;
  ensures [abstract] result == spec_coin_address<CoinType>();
}

spec fun spec_coin_address<CoinType>(): address {
  // TODO: abstracted due to the lack of support for `type_info` in Prover.
  @0x0
}

And here we see the problem. Due to a technical limitation in the Move Prover at the time that we did this work, the specification was unable to express the actual value returned by coin_address, so instead it stated that the returned address is always @0x0. However, in init we asserted that signer::address_of(account) == @0x1234. The prover sees that 0x1234 != 0x0 and, quite reasonably, concludes that the assertion will always fail and that init always aborts.

To avoid this issue, we had to weaken the specification. The simplest option is to state that coin_address may return any address by removing the ensures clause entirely.

This over-approximates the true set of allowable return values, but that is preferable to an under-approximation because it doesn’t introduce inconsistencies.

We reported this issue to the Aptos team. The technical limitation has been resolved and the Aptos team has updated the coin_address specification to properly express the actual return value.

How Can This be Avoided?

In this particular case, using the --check-inconsistency and --unconditional-abort-as-inconsistency options of the Move Prover catches the bug. We use those options routinely now. However, there are inconsistencies that those options don’t detect, so they’re not a silver bullet for avoiding this problem.

This episode illustrates a more general issue with formal verification. In other kinds of auditing you search for bugs, and if you find one anyone can see it. You can point to the bad line(s) of code and construct a proof-of-concept example that concretely demonstrates the problem. Formal verification, on the other hand, aims to show that the code’s behavior always satisfies some set of mathematical properties, and you attempt to write those properties in a way that guarantees the absence of incorrect behavior. However, if the properties are inconsistent or incomplete, formally verifying them may not guarantee what you intended.

It is therefore important to pay close attention to all the components that contribute to the verification.

These include:

Experienced verification engineers take measures to guard against these errors, as well as the rare chance that the verification tools themselves might have bugs affecting the verification results.

To make sure that the specifications are correct, we consider what behavior the specifications are intended to rule out and deliberately add such behavior to the code to see that verification fails in the expected way. This is exactly how we found the issue described above.

Making sure there are no errors in the assumed specifications of surrounding code is similar to finding errors in software. Since by definition these are the parts of the code that are not being formally verified, we instead need to carefully review the assumed specifications to see if they accurately describe the behavior we expect of the surrounding code. Just as an ordinary code reviewer needs to be an expert programmer, a specification reviewer should be a formal verification engineer with experience in writing specifications themselves.

To avoid problems with the verification tools, projects should make use of widely used, well-tested software as far as possible, and verification engineers should be aware of how it is implemented so that they can avoid pitfalls. For example, the Move Prover works by translating the programs into the Boogie intermediate language. It then uses the standard Boogie engine, which is actively maintained and has been used for formal verification in industry settings for over a decade.

To avoid having to trust more code than absolutely necessary, it is possible to build tools around a small trusted kernel. At CertiK we have experience with this approach using the Coq proof system. In a ground-breaking research project, the CertiKOS operating system kernel was verified with minimal assumptions: only the Coq kernel and a short description of x86 assembly language has to be trusted.

Conclusion

Formal verification provides the highest level of software assurance, and is the only method that can objectively rule out the possibility of incorrect behavior relative to a mathematical specification. But it still requires care. In this case, even though we used the Move Prover, an overlooked line of specification in a completely different codebase was enough to undermine the validity of the verification. After we corrected it we were able to successfully verify the client code, and the fix has now been applied to the main Aptos repository. We also recommend that all verification efforts include quality assurance steps that check that incorrect behavior fails to verify.

This illustrates that for formal verification to work as intended, verification tools alone are not enough. Good software engineering and proof management practices are also essential, and verification engineers need sufficient experience to know where the pitfalls are.

Read more: https://www.certik.com/resources/blog/1NygvVeqIwhbUk1U1q3vJF-the-move-prover-quality-assurance-of-formal-verification