PositionNomadic Labs is looking for a MechaTez: Formally Verifying Critical Features of Tezos Protocols intern.
Tutors: Thomas Letan and Yann Régis-Gianas
One of the distinguishing feature of Tezos is its self-amendment property. Every now and then, the Tezos ecosystem is asked through a vote procedure to decide how the chain will evolve. What that means in practice is that software updates (called protocols in Tezos) are regularly proposed, elected, and finally automatically deployed. In practice, a new protocol is deployed every three or four months.
The downside of this approach is that deploying a protocol takes time, and is not suited to deal with the discovery of critical bugs after said protocol has been deployed. Furthermore, the Tezos blockchain is used to manage sensitive, valuable assets that a bug could jeopardize.
As a consequence, it is essential to ensure the quality of a protocol prior to proposing it to the ecosystem. One possible approach to is to rely on formal methods to formally verify the correctness of (critical part of) a protocol. Because Tezos protocols are developed in OCaml, the Verification team of Nomadic Labs is exploring the use of FreeSpec to tackle this challenge. FreeSpec is a reasoning framework for the Coq theorem prover. The resulting project is called MechaTez.
The goal of this internship is to take part in the MechaTez project. More precisely, the intern will leverage MechaTez to formally verify one feature of Tezos, either one that is already integrated into the codebase or one that is still in development. This implies:
• understanding the OCaml implementation of said feature,
• porting this implementation in Coq,
• formalizing both the properties of the feature and the hypotheses it relies on,
• proving the correctness of the Coq model wrt. these properties,
• validating of the Coq model against the original implementation.
We are interested in proving functional correctness (wrt. a formal specification) and security properties (e.g., storage integrity, secret confidentiality, resistance against cache poisoning, etc.).
Because MechaTez is still in a early stage, the intern will be encouraged to contribute to the ecosystem supporting MechaTez, notably FreeSpec (the reasoning framework) and coqffi (a tool used in MechaTez to generate Coq FFI modules for the OCaml protocol implementation).
The successful applicant should have a good knowledge of the OCaml programing language. They should be familiar with at least one theorem prover, more prefer-ably Coq. Finally, they should be familiar with Hoare Logic, and formal verification of software programs.
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 independently 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.
All material produced (essays, documentation, code, etc.) will be released under an open source license (e.g. MIT or CC).
➡️ If you don’t meet all the criteria above, but think you can still be an asset to us, please consider applying.