A Formal DSL For Legally-Binding Smart contracts

Funding: ANR Smart IoT for Mobility (SIM) - AAPG 2019

Starting date: between September 1st, 2019 - February 28th 2020

Context:

The ANR Project “Smart IoT for Mobility” aims to develop, in close collaboration with the private partners Renault Software Labs and Symag, solutions for automatically adopting the negotiation problems, through Smart Contracts, of “Smart Service Books” (virtual passports or maintenance notebooks) all in blockchains that will ensure both the compensation of each partner (via traceability) but also the sharing of data (the privacy) and business models with partners with converging and divergent interests.

Blockchains are a distributed ledger of information that cannot be altered and therefore guarantee that it does not contain any bug. The main innovation is in the fact that transactions can be exchanged without the need of a trusted third party – typically the banks, the insurance experts or any other actor involved in the ecosystem. Smart contracts were described for the first time by Nick Szabo in the late 1990s [Szabo, 1997]. He had envisioned the creation of programs associated with contracts that could be both “trustless” and “self-enforcing”, which would increase their effectiveness and remove ambiguities, as well as the prohibitive cost of application. Smart contracts are both encoded as blockchain transactions (so are non alterable) and use blockchain to enforce transactions automatically. Therefore they need to be absolutely flawless.

In these blockchains, the most significant innovation results from the smart contracts that are programs that can be reviewed by anyone and that are designed to execute the terms and the clauses of a legal contract automatically when new data are available. Smart contracts can thus be understood – from final users’ side – as one of the main transformations in the digital world and locate therefore their acceptability at the heart of their diffusion (as digital innovations). Smart contracts can fix the limits of a contract: from the beginning to the end.

In the scope of this project, the use-case that is under consideration is the “Smart Service Book” used in the context of the Renault Use-Case for their vehicles.

Mission

The goal is to devise a meta-language for the description of smart contracts. Up to now, languages for smart contracts are ad-hoc and largely depend on the underlying hyperledger. Having a formal language to describe smart contracts would help with the combination of several technologies. It is a challenge since it needs to be used by non-specialist and be accepted as a legal document or at least as an acceptable evidence to establish the responsibility. The doctoral student will mainly be involved in a task which defines the meta language of contract, the associated Domain Specific Language (DSL) in relation to the needs of lawyers. The thesis will include an implementation of this DSL (syntax, semantics) and its use in the GEMOC environment for the modeling, simulation and verification of smart contracts. An experiment of smart contracts will be carried out by implementing them as web services through the BlockSy environment and executing them on existing public blockchains (e.g., Ethereum or Hyperledger).

Partners

  • Renault Software Labs
  • Symag, subsidiary of BNP Paribas
  • Laboratoire I3S
  • Laboratoire LEAT
  • Laboratoire Gredeg

Positions

  • PhD Computer Science: 36 months
  • Post-doc position: 12 months
  • Research Engineer position: 12 months

Requirements and application