Fuzzicat: Fuzzing for Contracts Administering Tokens - Paris, France - Nomadic Labs

Nomadic Labs
Nomadic Labs
Entreprise vérifiée
Paris, France

il y a 2 semaines

Sophie Dupont

Posté par:

Sophie Dupont

beBee Recruiter
Description
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

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

  • FA
  • Multi-Asset Interface
  • FA
1.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 opensource 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).
Plus d'emplois de Nomadic Labs
Voir tous les emplois de Nomadic Labs