2018-01057 - Static analysis of byzantine consensus
Le descriptif de l’offre ci-dessous est en Anglais

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : Doctorant

Contexte et atouts du poste

Fault-tolerant consensus protocols (benign and byzantine) are at the core distributed systems, e.g., Amazon Dynamo, Apache Zookeeper, blockchain technologies. To ensure availability in the presence of faults, or to avoid a central authority, an application is deployed on several replicas. A client of the application communicates with any of these replicas, inducing a change in the application state. A consensus protocol is in charged to keep the replicas consistent, that is all replicas see the same set of client interactions (in the same order). 

Due to the multiple sources of non-determinism, e.g., network reliability, cheating participants, the development of these systems is challenging and highly error prone.  The goal of this project is develop static analysis techniques that increase the confidence we have in fault-tolerant byzantine protocols and implementations. 

The phd position is within the team ANTIQUE, formed of leading experts in abstract interpretation, one of the main automated verification techniques. ANTIQUE focuses on developing automated techniques to compute semantic properties of programs. The team is affiliated with INRIA Paris and is located at Ecole Normale Superior (rue d'ULM, Paris).  The working environment pares two of the best french institutions in formal methods and programming languages.  The phd position is funded by the french national research agency, in the context of the project SAFTA, i.e., static analysis of fault-tolerant algorithms. 

Mission confiée

Byzantine fault-tolerant protocols are among the most challenging systems when it comes to ensuring their correctness. Is is well known that the consensus problem is unsolvable over asynchronous networks under the presence of faults. Hence, algorithms and systems designers struggle to find conditions under which this problem can be solved.  These conditions are incomparable, leading to different protocols. Moreover, the design of a consensus protocol is not only constraint by the network behaviors, but also by requirements that come from the client. A simple example would be a client that wants the order of its commands to be preserved or not, and a more complex one being a system tolerant to malicious clients which try to destabilize it. 

Designing automated verification techniques for byzantine systems requires connecting three research areas: distributed algorithms (designing  algorithmic solutions to fundamental problems), systems (focused on implementing  and optimizing algorithms), and formal verification which uses mathematical models to rigorously check that the algorithms and their implementations respect the intended specifications. 

The candidate’s main activity consists in exploring the three research areas mentioned above and  to design and implement  a verification method for byzantine protocols. The techniques preferred in the group use SMT-solvers, refinement, and abstract interpretation. The projects aims for a high degree of automation, using a reduced amount of user input. For a better knowledge of the proposed research topic please do not hesitate to contact us or to check the webpage https://www.di.ens.fr/~cezarad/. We are interesting in theoretical foundational solutions that can be prototyped, preferably as extensions of our current infrastructure. 

The recruited person will primarily work with Cezara Dragoi. This research is embeded in a collaboration with researchers from other institutes, for example (INRIA Nancy),  Josef Widder (TU Wien), Damien Zufferey (MPI Kaiserslautern). 

Principales activités

Main activities :

  • participate at group meetings and seminars at ENS and INRIA
  • read and write research papers
  • prototype research ideas

Compétences

Technical skills and level required : distributed systems, formal methods, SMT-solvers, abstract interpretation, are highly appreciated but not mandatory. 

Languages : English (mandatory), French (optional), C++, Go, Java. 

Relational skills : team work 

 

Avantages sociaux

  • Subsidised catering service
  • Partially-reimbursed public transport