On September 30th, camlCase released Dexter.

Dexter is a smart contract empowering decentralized exchange, performing the same function for tez as Uniswap on Ethereum does for ether; it enables trade between tez and any other token implemented by an FA1.2 contract.

To this day, the following efforts have been undertaken to ensure Dexter’s quality, including:

• a security audit by Trail of Bits,
• extensive property-based testing by camlCase, and
• a formal verification of the functional specification of Dexter’s underlying smart contract by Nomadic Labs, using the Coq proof assistant with the Mi-Cho-Coq framework — the topic of this blog post.

Checking smart contracts is never about attaining certainty; it’s about clarifying what we do and do not know. Therefore, our efforts increase our confidence in the Dexter smart contract, but do not make errors impossible. In this blog post we give:

• an outline of what we have proved about Dexter, and also
• what we did not prove.

What is Dexter and FA1.2?

Dexter is a smart contract, with an accompanying decentralized app enabling decentralized token exchange on the Tezos blockchain. Users call Dexter’s smart contract to trade between tez and other tokens, without the intervention of a central authority. For instance:

• tez can be exchanged to tzBTC, a token that wraps bitcoin, and
• tez can be exchanged to USDtez, a USD-pegged stable-coin token⁴.

More precisely, Dexter is compatible with any FA1.2 token¹. FA1.2 is a standard for smart contracts implementing tokens on the Tezos blockchain. It specifies a minimal set of entrypoints for the contract to provide and how these entrypoints must behave. It is similar to the ERC20 standard for Ethereum.

Formally verifying a functional specification of Dexter

Nomadic Labs has experience of applying formal verification to smart contracts, most notably through our formal verification of the multisig and the spending limit contracts. We brought this experience to bear on Dexter as follows:

• We built an informal, functional, specification (in collaboration with camlCase);
• formalized this specification in Coq; and
• certified that the Dexter smart contract satisfies the formal specification, using a machine-checked proof in Coq.

The informal specification clearly and comprehensively describes the Dexter smart contract’s desired functional behaviours in natural language. This does three important things:

1. It’s a clear, human-readable, functional specification of the contract. A functional specification defines the contract’s desired, immediate output, in terms of updated storage and emitted operations, for each input.
2. The act of rigorously working through the specification improved the quality of the final code in a virtuous engineering cycle which ironed out details and covered corner cases.
3. We could then convert this human-readable specification into a formalization suitable for machine checking in Coq.

This work, while considerable and consequential, cannot be a panacea or a silver bullet. The following aspects has only been checked in the audit, and through testing, but have not been subject to a formal study:

• we cannot guarantee the soundness of the specification;
• we have not formally verified Dexter’s inter-contract communication; and finally
• we have not formally verified the temporal properties of Dexter.

This is subject to future work. We discuss each of these limitations in more detail below.

But, within these limitations: we know what the contract does, we checked the design space in detail — and furthermore, we proved it.

Specified, certified code in this style is also an important long-term investment in maintainability and security. For example it is future work to verify high-level, economic properties such as non-depletion, and to do this we will not have to look at Dexter’s source code: we can read the human-readable specification and/or reason from the formal specification, and our certification ensures the conclusions will hold of the implementation.

Methodology

Our development followed a policy where the contract is specified, implemented, and verified by three distinct teams:

• the specifiers,
• the implementors, and
• the verifiers.

This policy forces the teams to verify each other’s work, and thus increases overall confidence in the development.

For example, if the verification team spots a divergence between the code and the specification, they can’t just change one to suit the other: they have to communicate with the implementors and specifiers to agree on an intended behavior, and update the code and/or the specification accordingly.

For Dexter, we have had:

• one specifier who worked with camlCase with the informal specification, and then worked with the formalization of that specification;
• camlCase that implemented the code of Dexter; and
• two verifiers that proved the contract against the formal specification.

We followed this policy for most of the entrypoints, but time constraints meant the specifier also participated in the verification of 3 out of 11 entrypoints.

Time investment

Work with the informal and formal specification of Dexter has been ongoing part-time since November 2019. In total, the collaborating on the informal specification and developing the formal specification took 2 person-weeks from Nomadic Lab’s side. The final proof took three verification engineers four person-weeks to write.

Verification framework

The functional specification of Dexter has been verified in the Coq proof assistant using the Mi-Cho-Coq framework.

Coq is a rich environment, in which we can directly state and prove a wide variety of mathematical properties. In particular we can specify programs, program executions, and properties of program executions — including correctness with respect to a specification — all in a single theorem-proving environment.

Likewise Mi-Cho-Coq embeds Michelson smart contracts in Coq, so we can specify Michelson contracts and verify their properties, all in Coq — for instance, that a contract can’t fail or run out of tokens.

We do not reason directly on the Mi-Cho-Coq interpreter, since implementation details of how scripts are interpreted (think: stack manipulation), are irrelevant. Instead, we use Mi-Cho-Coq’s weakest-precondition calculator, which translates a contract and its execution into a logical proposition. To prove properties of the contract, we just need to prove properties of the corresponding logical proposition.

Findings

Developing a chain of formal spec / informal spec / implemented code, and checking that the three match up, catches errors. Below, we detail the errors Nomadic Labs found in the Dexter contract. These errors have been fixed in the version of Dexter running on mainnet.

Parameter verification

Each entrypoint of Dexter specifies a set of conditions on the parameters that must hold to successfully execute the entrypoint.

• Sometimes the formal specification omitted parameter verifications that the informal specification said should be present.
• Sometimes the code omitted parameter verifications that the informal specification said should be present (this can be a particular security issue).
• Sometimes the informal specification omitted parameter verifications that the code implemented.

Operation order

Michelson contracts emit operations at the end of execution (e.g. token transfers). In Dexter’s case, the operations are transfers either: to the caller of the contract; to a FA1.2-compliant token contract; or to another Dexter contract. When verifying Dexter we found incoherencies in the order of operations emitted by Dexter with respect to the specification.

For example: suppose a user wants to sell \(X\) many tokens, for \(Y\) many tez using the tokenToXtz entrypoint. Dexter’s specification asserts that Dexter should

1. transfer \(Y\) tez to the caller, and only then
2. transfer \(X\) tokens from the caller to Dexter through a call to the token contract.

It turned out that the implementation would emit the operations in the reverse order: first 2, then 1. This was not an exploitable security issue — but it could have been, and such a violation of a specification complicates integration of Dexter with other contracts. The following example demonstrates why.

Consider a scenario where this error was not fixed, and where the caller is itself a smart contract. The developer of the calling contract would assume from the specification that when their contract receives the \(Y\) tez from Dexter, it had not yet payed the outstanding \(X\) tokens. Whereas in fact, the incoherent implementation of Dexter would have transferred the \(X\) tokens from the caller before sending the tez to the caller.

So the calling contract might think it had more tokens available than the actual balance, and in mistakenly attempting to spend them, there might be insufficient funds for the FA1.2 token transfer initiated by the token-to-tez trade.

This scenario demonstrates the importance of the finer details of a specification, and ensuring that the implementation satisfies it.

Deadline checks

Dexter’s entrypoints for adding and removing liquidity and for performing trades contain a deadline verification; so if an order fails its deadline verification it should be rejected.

We found a small divergence between the specification of deadlines and their implementation. The specification states that the deadline must be greater than the current time stamp — so an order handled exactly on the deadline should be rejected.

However, in some entrypoints the check was inclusive: an order handled exactly on the deadline was accepted. This does not seem to have been an exploitable security issue, but the process of finding and fixing the issue illustrates how formal verification traps errors that might otherwise sneak into production code.

Future work

As with any formal verification, there are limits to our development. Some are inherent to software verification, while others stem from limitations of Mi-Cho-Coq:

Formal verification of the soundness of Dexter’s specification

By soundness we mean conformity to some “common sense” economic properties; e.g. that an attacker can’t remove the funds of a liquidity provider without permission.

This is simple garbage in, garbage out: we can check whether an implementation satisfies its specification, but what if the specification’s wrong? For instance, a specification’s author might inadvertently permit an attack by which an attacker would remove funds that are not theirs, by simple human error or by not fully understanding the domain logic of the system.

Formal verification of Dexter’s inter-contract communication

Michelson contracts communicate by emitting transfer operations at the end of their execution. If the destination of the transfer is another Michelson contract, then that too will be executed, and in turn it may emit operations. Thus, a single contract’s execution may trigger a chain of multiple contract calls.

For example consider Dexter’s entrypoint tokenToXtz, which exchanges tokens for tez. It emits a transfer to the caller with the obtained tez, and a transfer to the token contract that moves the sold tokens to Dexter. We’d like to assert that after this operation sequence, Dexter indeed gets the sold tokens.

Currently we can’t do this in Mi-Cho-Coq: we can confirm that Dexter emits the corresponding call to FA1.2, but Mi-Cho-Coq does not implement the semantics of inter-contract communication², so we cannot specify (and so cannot verify) the final effect of the complete chain of contract calls.

Formal verification of Dexter’s temporal properties

Temporal properties concern the behavior of a system over time. For instance: we’d like to verify that a user who adds liquidity to Dexter, can always remove it later.

This requires reasoning over all possible sequences of contract calls in the blockchain, which is currently impossible in Mi-Cho-Coq: first, because it requires adding the semantics of inter-contract communication, as discussed above; and second, because it also requires modeling properties of the block chain, such that the level and timestamp of each block in the chain is strictly increasing.

Results

The proof of the contract is available in merge request !71 of the Mi-Cho-Coq repository.

Excluding comments and blank lines³ the development is 2983 = 272 + 775 + 919 + 1017 lines of Coq code, as follows:

• importing the contract into Mi-Cho-Coq takes 272 lines;
• the specification is 775 lines long;
• the proofs of the main theorems (see here for the proof of individual entrypoints and here for the proof of the full contract) span 919 lines total;
• additionally, the proofs of the main theorems use 76 lemmas, spanning 1017 lines total.

Our lemmas are largely reusable and we’ll add them to the Mi-Cho-Coq framework to help future contract certifications, by us or by others.

Moving forward

At Nomadic Labs we are proud to have participated in the development and the verification of Dexter; the first smart-contract for exchanging tokens on the Tezos blockchain.

This work:

1. improves the security of a key component of the Tezos blockchain,
2. has improved the open-source tooling for verifying smart contracts in Coq,
3. is a long-term investment in (and commitment to) future maintainability and security, and
4. defines more clearly what is assured, and what is not yet assured, of Dexter’s behaviour.

Extending Mi-Cho-Coq is active R&D at Nomadic Labs, and we see potential applications beyond functional smart-contract specifications.

For example: the Trail of Bits audit of earlier versions of Dexter revealed exploits related to inter-contract communication (which have been fixed), of a type which could not have been detected with Mi-Cho-Coq in its current form. Improving this requires a finer modeling of Tezos’ smart-contract execution model. Extending Mi-Cho-Coq in this direction, and proving such properties on contracts such as Dexter, is future work for the smart-contract verification team at Nomadic Labs.

Also, to further increase confidence in Dexter’s soundness, we envisage an equivalence proof between Dexter and Uniswap. They work on similar principles, and Uniswap has been extensively studied for security bugs, so a proof that Dexter is equivalent (in a suitable formal sense) to Uniswap, would extend the trust already held for Uniswap to Dexter.

Acknowledgments

Thanks to camlCase for their help during the verification effort, and to Trail of Bits for discussing the finer points of their audit. We are very happy to have worked with them.