Dexter 2’s Formal Verification

Runtime Verification is thrilled to announce Dexter 2's formal verification completion.
Dexter 2 is an open-source, decentralized, non-custodial exchange for XTZ and FA1.2/FA2 tokens on the Tezos blockchain developed by the CamlCase team.

Dexter's Security Efforts

Dexter's engagement focused on formally verifying the bytecode using K-Michelson, an implementation of Michelson in the K framework. The CamlCase team is taking security seriously, as evidenced by the myriad of verification efforts and audits they have performed, including:

• Trail of Bits conducted an audit for the Dexter v1 smart contract, the Dexter frontend v0.8.2, and the Morley Framework implementation of the contract.
• CamlCase team conducted extensive property-based testing.
• Nomadic Labs conducted a formal verification of the functional specification of Dexter 2's smart contract using the Coq proof assistant with the Mi-Cho-Coq framework.

These security efforts cover a wide range of high-level source code audits and verification, but there is a slight chance that some bugs and security threats can be found on the low-level bytecode, but not the high-level source code. The CamlCase team wants to ensure the safety of their project, and so they contacted Runtime Verification to formally verify their V2 contract using K-Michelson to prove the absence of any security threat on the low-level bytecode.

Tezos and K-Michelson

To understand K-Michelson and how we formally verified the Michelson bytecode, we need to take a step back and briefly explain some Tezos features.

Tezos is an open-source platform for assets and applications that can evolve by upgrading itself. Developers can choose from a wide range of languages, high level and low level, to write their Tezos smart contracts. High-level languages include SmartPy, Ligo, and Lorentz and low-level languages include Michelson. It's important to understand that any smart contract written in a high-level language will eventually be compiled down to Michelson, the smart contract language of the Tezos blockchain. In the case of Dexter 2, their smart contracts are written in Ligo, a high-level language.

As a result of a previous engagement with Tezos, Runtime Verification developed a formal verification framework for the Michelson smart contract language called K-Michelson. K-Michelson allows us to execute or formally verify Michelson code and prove the correctness of smart contracts.

The engagement with CamlCase team consisted of verifying the Dexter contract in K at the level of Michelson. Formally verifying the bytecode level that runs on-chain allows us to spot any vulnerabilities introduced by the compiler.

Methodology

Runtime Verification team members Stephen Skeirik, Rikard Hjort, Nishant Rodrigues, and Daejun Park conducted Dexter's formal verification and published a detailed report on June 9th, 2021.

To start, a manual (on paper) formal audit was performed to prove invariants about the contract storage. This manual verification effort of high-level Dexter invariants assumed the functionally correct operation of the Dexter code, so that we did not have to worry about the correctness of the bytecode yet.

To accompany the high-level manual verification, the assumptions about the functionally correct operation of the Dexter code were mechanically specified and discharged with the K-Michelson prover. This ensures that the assumptions of the high-level invariant manual verification are actually met by the generated code. Separating the mechanically-checked functional correctness and the human-checked contract invariants allows the auditors to focus on the high-level properties and invariants that should hold throughout a contracts lifetime, while discharging correctness assumptions they need to be mechanically checked by the verification engineers.

Findings

Runtime Verification formalized and proved the high-level safety properties of the Dexter contract. Most importantly, it was demonstrated that the price of liquidity shares, measured in XTZ and tokens, never decreases. The team also identified several requirements on external contracts for the functional correctness and security of Dexter. It is important that the users ensure that such requirements are satisfied throughout the operation of Dexter, e.g. by ensuring that the token contracts they interact with are not upgradeable and behave correctly. The report provides several example scenarios where the requirements could be violated unless care is taken. Additionally, the mechanized functional correctness verification found that each contract entry point behaves as expected, and found no bugs introduced by the compiler.

About Dexter

Dexter is a decentralized, non-custodial exchange for XTZ and FA1.2 tokens on the Tezos blockchain. It removes the need for a centralized order book by automating a market for XTZ and FA1.2 in the logic of a smart contract. Each Dexter smart contract is associated with a unique XTZ / FA1.2 token pair. Any owner of XTZ and FA1.2 can become a liquidity provider by depositing an equal value of XTZ and FA1.2 into the smart contract.

About Runtime Verification

Runtime Verification is an American startup with a global presence. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field.