FuzziCAT: Fuzzing for Contracts Administering Tokens

Blockchains, such as Tezos, implement tokens: cryptographically secured assets
representing the ownership of a value. Chains typically have one native token (in
the case of Tezos; the tez), but also allow developers to create additional tokens for
other types of value. In Tezos, this is done by writing a smart contract: a small piece
of software deployed on-chain. The smart contract defines how tokens are created,
removed and transferred between users.
The interoperability and security of token contracts is paramount: they form key com-
ponents in larger systems of interacting smart contracts, handle large financial val-
ues. The FA2 standard has been proposed as a common interface all token contracts
should expose. Nomadic Labs have formalized the FA2 standard using Mi-Cho-Coq,
a Coq-based smart contract verification platform for Tezos. This has allowed us to
prove FA2 compliance of specific contracts. Recently, we have derived a test suite
from the formalization, allowing us to detect non-compliant contracts automatically.

Goals of the internship

The goal of the internship is to increase the FA2 test suite’s coverage by connecting
it to the Monolith fuzzer.
The intern will extract an executable compliance monitor in OCaml from the FA2 Coq
specification. The monitor will serve as the reference implementation for FA2 con-
tracts. Then, the behavior of a candidate FA2 contract can be automatically com-
pared and tested in Monolith against this reference. The end-result will be a tool that
uses Monolith’s fuzzing and property-based testing techniques to automatically find
non-compliances in FA2 contracts.

Requirements

Requirements are (in decreasing order of importance):
• Familiarity with functional programming, e.g. OCaml, Haskell or Scala.
• Experience with the Coq proof assistant.
• Familiarity with the extraction mechanism of Coq is a plus.
Further reading
• FA2 – Multi-Asset Interface
• FA1.2 Approvable Ledger, formal verification by Nomadic Labs
• Formal Verification of ERC20 Contracts
• ERC20 Token Verifier
• Strong Automated Testing of OCaml Libraries

Internship Context

You will work at the Nomadic Labs’ offices in Paris.
Participating in a large scale open-source project you will have to rapidly learn to
use collaborative tools (Git, merge request, issues, gitlab, continuous integration,
documentation) and to communicate about your work. The final results might be
presented at an international conference or workshop.
You will have a designated advisor at Nomadic Labs and will have to work indepen-
dently and to propose thoroughly-considered solutions to the different problems you
will have to solve. You will be encouraged to seek advice from members of the team.

Intellectual Property

All material produced (essays, documentation, code, etc.) will be released under an
open source license (e.g. MIT or CC).