Some of the recent blockchain proposals, such as Stellar and Ripple, allow for open membership while using quorum-like structures typical for classical Byzantine consensus with closed membership. This is achieved by constructing quorums in a decentralised way: each participant independently chooses whom to trust, and quorums arise from these individual decisions. Unfortunately, the consensus protocols underlying such blockchains are poorly understood, and their correctness has not been rigorously investigated. In this paper we rigorously prove correct the Stellar Consensus Protocol (SCP), with our proof giving insights into the protocol structure and its use of lower-level abstractions. To this end, we first propose an abstract version of SCP that uses as a black box Stellar's federated voting primitive (analogous to reliable Byzantine broadcast), previously investigated by García-Pérez and Gotsman. The abstract consensus protocol highlights a modular structure in Stellar and can be proved correct by reusing the previous results on federated voting. However, it is unsuited for realistic implementations, since its processes maintain infinite state. We thus establish a refinement between the abstract protocol and the concrete SCP that uses only finite state, thereby carrying over the result about the correctness of former to the latter. Our results help establish the theoretical foundations of decentralised blockchains like Stellar and gain confidence in their correctness. This joint work with Maria A. Schett will be presented at OPODIS 2019.

In this talk I will briefly explain how refinement types can are used for program verification. Refinement types use the modularity of types to reduce program verification into SMT decidable queries. The talk relies on a PLMW@ICFP 30 minutes presentation, so there will be plenty of time for Q&A.

Modern software engineering deals with demanding problems that yield large and complex software. The area of Model-Driven Software Engineering tackles this issue by using models during the development process, but it does not address some of the communication problems among different stakeholders. Domain-Specific Modelling Languages (DSML) aim at involving domain experts with non-technical profiles in that process. DSMLs define concepts with different levels of abstraction, but traditional modelling does not allow enough flexibility to organise them adequately. Multilevel Modelling (MLM) approaches provide an unbounded number of levels of abstraction, plus other features that perfectly fit DSMLs. Their development can also benefit from Model Transformations (MT), especially when these encode the behaviour of DSMLs. MTs can be exploited by MLM, becoming a precise and reusable definition of behaviour. In this talk, I outline the work that I presented in my PhD thesis, consisting of a MLM and Multilevel MT approach which tackles open issues in the field and compares it with the state of the art through literature review and experiments, providing its formalisation and its implementation in the tool MultEcore, together with case studies.

The general idea of STARKs is to transform a claim on a certain computation to another claim on the low-degreeness of one polynomial. This construction has gained a lot of attention during the past year, leading to several implementations in the wild. During this talk, we will explain how to build a STARK using genSTARK, one of these libraries. We will also share its complexity analysis based on the different parameters involved in Pedersen commitments computation, assuming very little mathematical background. Only some basic cooking notions will be expected from the audience. I will do a 30min rehearsal for my talk at the ZKProof Community Event in Amsterdam on October 29. This is a presentation of the summer internship I did at QEDIT, Tel Aviv.

We consider the problem of proving in zero knowledge that an element of a public set satisfies a given property without disclosing the element, i.e. that for some u, “u ∈ S and P(u) holds”. This problem arises in many applications (anonymous cryptocurrencies, credentials or whitelists) where, for privacy or anonymity reasons, it is crucial to hide certain data while ensuring properties of such data. We design new modular and efficient constructions for this problem through new commit-and- prove zero-knowledge systems for set membership, i.e. schemes proving u ∈ S for a value u that is in a public commitment c_u . Being commit-and-prove, our solutions can act as plug-and-play modules in statements of the form “u ∈ S and P(u) holds” (by combining our set membership system with any other commit-and-prove scheme for P(u)). Also, they work with Pedersen commitments over prime order groups which makes them compatible with popular systems such as Bulletproofs or Groth16. Both public parameters and proofs in our solutions have constant-size (i.e., independent of the size of the sets). Compared to previous work that achieves similar properties—Camenisch and Lysyanskaya (CRYPTO 2002) and the clever techniques combining zkSNARKs and Merkle Trees in Zcash—our protocols offer more flexibility and 4× faster proving time for a set of size 2^60.

We study the problem of decentralized monitoring of stream runtime verification specifications. Decentralized monitoring uses distributed monitors that communicate via a synchronous network, a communication setting common in many cyber-physical systems like automotive CPSs. Previous approaches to decentralized monitoring were restricted to logics like LTL logics that provide Boolean verdicts. We solve here the decentralized monitoring problem for the more general setting of stream runtime verification. Additionally, our solution handles network topologies while previous decentralized monitoring works assumed that every pair of nodes can communicate directly. We also introduce a novel property on specifications, called decentralized efficient monitorability, that guarantees that the online monitoring can be performed with bounded resources. Finally, we report the results of an empirical evaluation of an implementation and compare the expressive power and efficiency against state-of-the-art decentralized monitoring tools like Themis.

Modern data stores achieve scalability by partitioning data into shards and fault-tolerance by replicating each shard across several servers. A key component of such systems is a Transaction Certification Service (TCS), which atomically commits a transaction spanning multiple shards. Existing TCS protocols require 2f+1 crash-stop replicas per shard to tolerate f failures. In this work we present atomic commit protocols that require only f+1 replicas and reconfigure the system upon failures using an external reconfiguration service. We furthermore rigorously prove that these protocols correctly implement a recently proposed TCS specification. We present protocols in two different models--the standard asynchronous message-passing model and a model with Remote Direct Memory Access (RDMA), which allows a machine to access the memory of another machine over the network without involving the latter's CPU. Our protocols are inspired by a recent FARM system for RDMA-based transaction processing. Our work codifies the core ideas of FARM as distributed TCS protocols, rigorously proves them correct and highlights the trade-offs required by the use of RDMA.