TL;DR: A flaw was found in the camlCase’s Dexter contract. The funds have been removed from the contract and returned to their original holders.
A high level explanation follows; technical details of the Dexter flaw will be described in a separate post to come.
As many of you know, we have been working on a new Tezos upgrade proposal. This proposal, if accepted, will change the calling convention from breadth first ordering to depth first ordering. In the course of reviewing potentially affected contracts, we stumbled into an unrelated but serious flaw in Dexter permitting unauthorized withdrawal of funds.
We provided information on the vulnerability to camlCase, and, following responsible disclosure policies, we have waited to make a public statement until public discussion of the vulnerability would no longer harm the participants in Dexter.
Since then, a so-called “White Knight” operation has been conducted in which the funds were removed from the contract using the bug itself and then returned to their rightful owners. We are informed that this operation has now concluded, and all funds are safe.
Given the apparent substantial community interest in availability of a distributed exchange contract, a team led by Nomadic Labs has, in the interim, rewritten the contract to avoid this bug, and is in the process of proving that this particular class of bugs cannot re-occur. We will be releasing both the code and specification for this contract shortly.
When we first published our blog post announcing the formal verification of the Dexter contract, we wrote some important things about what we had verified:
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.
We then went on to list several limitations, including this:
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.
Unfortunately, our words have proven prophetic.
We again note that formal verification can only check if a contract meets a given specification, but not if the specification is incorrect.
As we have noted, we will soon be publishing the specification of the new contract. We invite interested members of the community to examine the new specification and provide feedback on whether our belief that the proper safety and correctness properties are now present is correct.
We look forward to the deployment and adoption of this new distributed exchange contract by interested parties once the community is satisfied that it is secure.