Linear Types for secure data

Tutors : Pietro Abate, Julien Tesson

Blockchains are decentralized ledgers managed using a distributed peer-to-peer network. Tezos is a blockchain and a smart contract platform developed with a focus on governance and security. The Tezos code base is entirely written in OCaml which is a strongly typed functional language.

The client part interacting with the Tezos blockchain, so-called digital wallets, is the software component (sometimes coupled with a hardware secure storage) entrusted with managing the private keys and identities of each user.

Goals

To enhance the security of this critical component, we envisage encoding the type holding sensitive data using linear types. Linear types guarantee that their values are used only once; thus, they can be used to statically analyze the behavior of programs, such as resource usage and communication protocol.

In particular, the internship involves studying a recent paper "Lightweight linearly-typed programming with lenses and monads"1 to catch at eventual secret leaks at compile time, encoding a lock-and-wipe system to make sure secrets are never written to disk, and to integrate this library into the current Tezos client implementation.

Possible challenges:

  • Studying encoding linear types in OCaml using lenses and monads.
  • Learning about possible secret leaks scenarios.
  • Learning and modifying the code base of Tezos.
  • Creating and designing a formal specification of the encoding of secrets using linear types.

Requirements

You should have knowledge of the OCaml programming language and have attended an introductory course in type theory.

You will work with the Nomadic Labs core development team.

Internship Context

You will work at the Nomadic Labs' offices in Paris or Grenoble.

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.

Intellectual Property

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