A Case Study of Code-Level Verification with Motoko-san

Arshavir Ter-Gabrielyan
14 min readJan 25, 2023

--

Please first read DFINITY’s latest post on Code-Level verification in Motoko. This post is a technical extension aimed at Motoko programmers.

Consider ClaimReward, a canister designed to reward the very first claim (e.g., by sending some crypto tokens). All subsequent claims shall not be rewarded. Similar logic is used in practice in lottery and auction applications.

Below is the Motoko implementation of ClaimReward:

actor ClaimReward {
var claimed = false;
var count = 0 : Int;

private func reward() : () {
// (send reward) // step 1
count += 1; // step 2
};

public shared func claim() : async () {
if (not claimed) { // step 0
reward();
claimed := true; // step 3
};
};
}

The canister consists of a single actor, whose two fields are claimed (a flag indicating if the reward has already been claimed) and count (the number of times that the reward has been sent out). In Motoko, fields of an actor can be directly modified only by the functions of the actor; external callers (be those human users or other smart contracts) may invoke only the public functions, potentially resulting in certain field modifications.

The only public function that ClaimReward has is claim. This function does not take any arguments, nor does it return anything (note that all public functions in Motoko must have an async return type). Naturally, an invocation of claim may cause some field modifications. Let us see what this function is doing:

  • step 0. The claim function first checks if the claimed flag is not yet set (otherwise returning without any effect).
  • If the condition not claimed is met, the following happens:
    – We call reward()
    step 1. The reward tokens are sent back to the caller.
    step 2. The count is incremented by one.
  • step 3: The claimed flag is set.

For now, we abbreviate step 1 with the send reward comment.

Specifying a canister invariant

Recall that the purpose of the ClaimReward canister is to reward the very first claim, and no other claim. Clearly, the total number of rewards sent to users over the lifetime of this canister should not exceed one. This condition can be formalized as follows:

(not claimed implies count == 0)  // initially synchronized
and (count == 0 or count == 1) // reward is unique

We call this condition the canister invariant of ClaimReward. Despite its simplicity, this canister invariant is a useful specification for our code. From a user's perspective, this condition expresses the rules of the ClaimReward canister. Remember that the user may not be a programmer and might not be able to fully understand the source code! In contrast, we can easily communicate the above canister invariant in plain English.

Canister invariants are also essential for defining what it means for an implementation of ClaimReward to be correct. In particular, it must be impossible for an adversary to use a canister in such a way that would violate the canister invariant. Conversely, if there is a scenario in which, by invoking some public function(s), an adversary could break the invariant, that would imply that the canister is not implemented in a correct manner.

Code-level specifications

Above, we pointed out two key advantages of our code-level specification approach, i.e., the practice of specifying a canister’s intention (the rules of the game) through the same language that is used to implement this canister:

  1. Code-level specs are formal (the notion of correctness has meaning only if the code is formally specified)
  2. Code-level specs can be easily communicated to other developers and end users.

Aren’t specifications code, too?

Two other practical advantages of code-level specifications are that the specifications can be (1) written and version controlled alongside the executable code and (2) checked automatically at compile time. In contrast, the first advantage is lacking in dedicated software modeling languages like TLA+, that makes it hard for a smart contract developer to detect possible source code modifications that require manual model adjustments. And the second advantage is lacking in back-of-an-envelope specification approaches, e.g., plain text (think, Javadoc), that requires regular human inspection and can easily get outdated.

Below, we demonstrate how to write code-level specifications for the ClaimReward canister. The assert:invariant <exp>; syntax allows specifying a canister invariant <exp> that is type checked just like a normal Motoko expression — while not affecting the ClaimReward's runtime behavior in any way.

actor ClaimReward {
var claimed = false;
var count = 0 : Int;

assert:invariant
(not claimed implies count == 0) // initially synchronized
and (count == 0 or count == 1); // reward is unique

private func reward() : () {
// (send reward)
count += 1;
};

public shared func claim() : async () {
if (not claimed) {
reward();
claimed := true;
};
};
}

Verifying canister invariants automatically

We are now ready to verify the canister code against its invariant.
Motoko-san is a tool that makes this an easy process (a very early prototype is available on the VS Code extension marketplace). The tool provides a familiar user experience similar to that of the Motoko type checker.

Disclaimer: DFINITY released Motoko-san as a community preview; no further updates are currently planned. Please use this tool at your own risk. Refer to the documentation for the list of currently supported features.

To ask Motoko-san to verify a file, we add // @verify as the first line. The tool will either report an error, underlining the offending code with a red wave (Fig.1, above), or show a green checkmark ✅, indicating that the code is proven to comply with the formal specifications (Fig.2, above).

Pro tip: Motoko-san works well together with Error Lens, a VS Code extension that shows error messages right next to the line that caused it.

Opening our formally specified ClaimReward canister in VS Code with Motoko-san, we observe that it verifies. Great!

This is a good time to play a bit with the tool: For example, try changing the second initializer to var count = 1 : Int;, in which case the tool will report a verification error:

Canister invariant cannot be established after initialization

This error is of course expected, as a canister invariant must be established right after initialization.

Handling async code

Our current ClaimReward implementation does not show how the reward is actually sent. In practice, the code abbreviated (send reward) could, e.g., transfer some tokens from the ClaimReward canister's account back to the user's account. Transferring tokens would practically involve calling a public function of another canister (e.g., Ledger.transfer). Since the result of this call is an async object, our reward function needs to await it. Therefore, (1) the return type of reward itself should be async, and (2) claim should await on reward(). We represent this logic as follows:

actor ClaimReward {
var claimed = false;
var count = 0 : Int;

assert:invariant
(not claimed implies count == 0) // initially synchronized
and (count == 0 or count == 1); // reward is unique

private func reward() : async () {
// (send reward)
count += 1;
};

public shared func claim() : async () {
if (not claimed) {
await reward();
claimed := true;
};
};
}

We assume here that the async call abbreviated with (send reward) cannot fail; handling failures would require additional code. Under this assumption, the count variable tracks the number of reward transfers.

Let’s now inline the reward function to make the control flow more apparent:

actor ClaimReward {
var claimed = false;
var count = 0 : Int;

assert:invariant
(not claimed implies count == 0) // initially synchronized
and (count == 0 or count == 1); // reward is unique

public shared func claim() : async () {
if (not claimed) {

// yield control ...
await async {
// ... receive control

// (send reward)
count += 1;

// yield control ...
};
// ... receive control

claimed := true;
};
};
}

To explain how async code works in Motoko, we first need to define which code fragments are guaranteed to be executed immediately, i.e., without being interleaved with other code fragments.

What is an atomic code block?

An atomic block of code is the smallest portion of code that is guaranteed to be executed immediately.

Control-yielding semantics of await

When our new variant of ClaimReward.claim is executed, the await statement splits the function into several atomic blocks. In particular, the atomic block under await async is not necessarily executed immediately after the branch condition has been checked, but possibly with some other atomic blocks being executed in between. Similarly, the execution of claimed := true will not necessarily happen right after the async code execution finishes. Again, other atomic blocks may be executed in between.

Consider the following question. Let’s abbreviate the branch statement as b, the code block under await async as a, and claimed := true as c. Which of the following executions are possible?

  • b, a, c
  • b, a, c, b
  • b, a, c, b, a, c
  • b, a, b, a, c, c
  • b, a, b, c, a, c

The first case in this list represents a single invocation of ClaimReward.claim. The second case is similar, but after the first invocation returns, another one occurs; however, the condition of the branch b is not satisfied, so the second invocation returns without a and c being executed again. The third case is identical to the first one, with one repetition.

What scenarios do the last two cases represent?

Reentrancy

Reentrancy is an interleaved execution of atomic code blocks. Since there is no other function in the ClaimReward canister except for claim, it might be unclear what atomic blocks can realistically be involved in reentrancy in this case. We will now show that even a canister with just one function may end up handling multiple concurrent invocations, resulting in reentrancy. We will then explain why reentrancy can be dangerous.

Consider a scenario in which the execution of one invocation of claim enters the branch. Eventually, the async block will be executed, increasing the value of count (now count equals 1). If the very next executed atomic block happens to be claimed := true, then all is fine since:

  1. The reached state complies with our canister invariant.
  2. The next invocation of claim will not cause any changes to the fields as the branch condition not claimed will no longer be satisfiable.

However, if another invocation of claim starts executing before the claimed := true atomic block, then we might observe that count equals 2! This violates our canister invariant that specifies only 0 and 1 as acceptable values of count. Practically, this means that the reward can be claimed more than once, and a simple reentrancy attack could drain the canister owner's account balance.

What are Reentrancy attacks?

Reentrancy attacks are attacks on canisters in which their invariant is violated by an interleaved execution of async code. A canister is reentrancy-safe if there is no possible reentrancy attack. We want to verify that our canisters are reentrancy-safe.

A simple fix for our ClaimReward canister involves swapping the two statements under the branch. Concretely, a reentrancy-safe implementation would first set the claimed flag (before yielding the control for the first time), and only then await the execution of the async block. Indeed, this would prevent an attacker from gaining rewards multiple times as the very first reward will be sent only after the claimed flag, which guards the reward, is already set.

Automatic compile-time detection of reentrancy attacks

Wouldn’t it be nice to have a tool that automatically detects and reports reentrancy attacks — while the code is being compiled? We demonstrate how this is done with Motoko-san. To this end, let us try to verify the (buggy) code from the previous listing.

Motoko-san reports the following verification error:

Canister invariant violated by async block

Naturally, this is expected, as we already know that there exists a reentrancy attack in our code.

Here is how we can fix the code:

actor ClaimReward {
var claimed = false;
var count = 0 : Int;

assert:invariant
(not claimed implies count == 0) // initially synchronized
and (count == 0 or count == 1); // reward is unique

public shared func claim() : async () {
if (not claimed) {
claimed := true;

// yield control ...
await async {
// ... receive control

// (send reward)
count += 1;

// yield control ...
};
// ... receive control
};
};
}

Perhaps surprisingly, Motoko-san reports the same error again:

Canister invariant violated by async block

The reason Motoko-san reports an error in this case is that, unlike in our ad-hoc reentrancy argument, Motoko-san verifies canisters in a function-modular manner. In other words, each canister function needs to be verified against the canister invariant independently of the knowledge about all other functions. Even the fact that there are no other functions (as is the case in our latest variant of ClaimReward) is (purposefully) not taken into account by Motoko-san.

Function-modular verification

Yes, function-modular verification is potentially incomplete — i.e., there can be false-positives. However, this approach enables scaling verification efforts to applications with arbitrary-many functions, as we explain next.

While correct, the canister implementation that we have converged to so far (Fig.3, below) is unsafe under code evolution. To illustrate this point, assume that the code so far has been written entirely by one person, Alice, who is unfortunately unaware of the benefits that Motoko-san has to offer. After publishing the code as it is, Alice’s work is continued by Bob. Let’s assume that the only knowledge that Bob has from Alice about this canister’s original intention comes from two sources:

  1. The ClaimReward canister invariant.
  2. ClaimReward's public API, consisting of the function claim.

Now, Bob wants to extend the canister with another function, reset(), that will return the canister to its original state (Fig.4, above). Bob thinks that this extension will preserve backward compatibility, as he concluded that the reset function does not contradict the intention of the original canister. Indeed, the initial state of the canister must satisfy the canister invariant — no issue with that — and all pre-existing functions remain unchanged. Therefore, Bob commits the following code:

actor ClaimReward {
var claimed = false;
var count = 0 : Int;

assert:invariant
(not claimed implies count == 0) // initially synchronized
and (count == 0 or count == 1); // reward is unique

public shared func claim() : async () {
if (not claimed) {
claimed := true;

// yield control ...
await async {
// ... receive control

// (send reward)
count += 1;

// yield control ...
};
// ... receive control
};
};

public shared func reset() : async () {
claimed := false;
count := 0;
};
}

It is now possible to violate ClaimReward's canister invariant using the following sequence of invocations: claim() , reset(), claim(). Indeed, this sequence can result in an effective reentrancy attack, since the execution of reset() may occur during the execution of claim() (between the first yield control / receive control pair). In this attack, both invocations of claim will increase count, so we will eventually observe count == 2 .

Luckily, Bob is a Motoko-san user. He immediately gets a verification error, indicating that the async block in ClaimReward.claim is problematic. Although a reentrancy attack on ClaimReward exploits Bob's reset function, it is actually Alice's claim function that is vulnerable. Indeed, removing the claim function whatsoever would result in a reentrancy-safe (yet, practically useless) canister.

Explicitly specifying assumptions in async code

Arguably, we should blame neither Alice nor Bob for the vulnerability in the listing above. The problem is due to Alice’s implicit assumption (that Bob didn’t know about) of the fact that no code can mess up the intermediate state of claim's execution, namely, between the first yield control / receive control pair.

To avoid confusion, Alice decides to encode her assumption explicitly, following the code-level specification approach. Concretely, she wants to express the following async constraints:

  1. The claimed flag must still be set when the first receive control is reached.
  2. The value of count must still be 0 when the first receive control is reached.
  3. At most one instance of this async block may be executed per invocation of claim.

Async constraints serve a dual purpose. On the one hand, they are assumptions while reasoning about the atomic block inside await async. Concluding that this block actually preserves the canister invariant requires that these assumptions are met. In particular, if assumption 2 were violated, then the value of count after the async block could be less than 0 or greater than 1, violating the canister invariant. (Recall that we don’t know what other functions there are in the canister while reasoning about claim.)

On the other hand, async constraints are also formal proof obligations that must be respected by all functions of the ClaimReward canister. For example, reset in the listing above violates proof obligation 1, as it sets claimed back to false (which can be exploited in a reentrancy attack).

The third async constraint above is a bit more subtle. Generally, atomic blocks to be executed are picked up from a runtime message queue, allowing for the same code block to be scheduled multiple times. For example, this is useful to process async calls to public functions efficiently. However, the async block in our ClaimRewards canister is of course not supposed to be scheduled more than once per message queue (otherwise, the reward could be sent more than once).

Canister specifications = Canister invariant + Async constraints

Since async constraints restrict all functions of a canister, they are similar to the canister invariant. However, while the canister invariant typically contains information that is useful to the canister’s users, async constraints are mostly useful for communicating design decisions (involving async code) among canister developers. In particular, async constraints typically describe intermediate states of execution of public functions.

Syntactically, it seems the easiest to write async constraints next to the atomic blocks that they refer to (note that canisters often have multiple async blocks that would potentially need different sets of async constraints).

Motoko-san provides the following experimental syntax for writing async constraints:

actor ClaimReward {
var claimed = false;
var count = 0 : Int;

assert:invariant
(not claimed implies count == 0) // initially synchronized
and (count == 0 or count == 1); // reward is unique

public shared func claim() : async () {
if (not claimed) {
claimed := true;

await async {
assert:1:async claimed and count == 0;

// (send reward)

count += 1;
};
};
};
}

Here, assert:1:async <exp>; allows specifying async constraints as a regular Motoko expression (e.g., it is type checked). The conjunction of claimed and count == 0 specify, correspondingly, the async constraints 1 and 2 of Alice's informal async constraints:

1. The claimed flag must still be set when the first receive control is reached.

2. The value of count must still be 0 when the first receive control is reached.

Finally, the digit 1 in assert:1:async specifies async constraint 3, namely:

3. At most one instance of this async block may be executed per claim invocation.

While the reset function added by Bob respects the canister invariant, this function does not respect the async constraint 1. Motoko-san automatically detects this problem (Fig.5, below).

After removing the reset function that caused the problem, Motoko-san is able to automatically verify the canister against its formal specifications (Fig.6, above). ✅

A safe and secure ClaimReward canister implementation

As a happy new Motoko-san user, Alice has now fully specified and (automatically) formally verified the ClaimReward canister against its invariant and the async constraints. Assuming that all future collaborators, like Bob, continue using Motoko-san to verify their code, no reentrancy-related vulnerabilities can arise, as the tool will be able to check that all the assumptions (which are now explicit) actually hold.

A natural next step is to integrate the code-level verifier into a continuous integration and deployment (CI/CD) pipeline. Such integration is feasible, as our canister’s formal specification is now part of the codebase. But this is a story for another time.

Acknowledgements

We cordially thank Marco Eilers, Gabor Greif, Martin Raszyk, Claudio Russo, and Ryan Vandersmith for contributing to the design and implementation of the Motoko-san prototype tool. Thanks, Marco and Claudio, also for proofreading this text.

--

--

Arshavir Ter-Gabrielyan

Software Engineer at the DFINITY Foundation, Dr. sc. from ETH Zürich