FRIDA 2019

The 6th Workshop on Formal Reasoning in Distributed Algorithms

Co-located with DISC 2019 (Budapest, Hungary) on October 18, 2019

Important Dates

Program

Abstracts

Hagit Attiya, The Technion, Israel

In the eye of the beholder—the role of the observer in observational refinement

Observational refinement is a methodology for specifying how programs interact with libraries and implementations. The talk will describe several scenarios in which characteristics of the program influence the resulting specifications. Examples include linearizability and related notions, or specifying the expected behavior of transactional memory.

Cezara Dragoi, ENS and INRIA, France

Communication-Closed Asynchronous Protocols

Fault-tolerant distributed systems are implemented over asyn-chronous networks, so that they use algorithms for asynchronous models with faults. Due to asynchronous communication and the occurrence of faults (e.g., process crashes or the network dropping messages) the implementations are hard to understand and analyze. In contrast, synchronous computation models simplify design and reasoning. In this paper, we bridge the gap between these two worlds. For a class of asynchronous protocols, we introduce a procedure that, given an asynchronous protocol , soundly computes its round-based synchronous counterpart. This class is defined by properties of the sequential code. We computed the synchronous counterpart of known consensus and leader election protocols, such as, Paxos, and Chandra and Toueg’s consensus. Using Verifast we checked the sequential properties required by the rewriting. We verified the round-based synchronous counterpart of Multi-Paxos, and other algorithms, using existing deductive verification methods for synchronous protocols.

Annie Liu, Stony Brook University, USA

Y. Annie Liu, Bo Lin, Scott Stoller, and Saksham Chand

Distributed Algorithms Made Clear: for Understanding by Humans and Reasoning by Machines

This talk will discuss DistAlgo, a language for distributed algorithms, and challenges for formal verification using existing tools. DistAlgo allows English and pseudocode descriptions of distributed algorithms to be captured completely and precisely at a high level, and be directly executable, without adding, removing, or reformulating algorithm details to fit lower-level, more abstract, or less direct languages.  Formal verification for such high-level specifications has the hope of being more understandable by humans and more automatable by formal verification tools.

More information about DistAlgo can be found at http://distalgo.cs.stonybrook.edu/tutorial

Vincent Rahli, University of Birmingham, UK

Asphalion: Trustworthy Shielding Against Byzantine Faults

Byzantine fault-tolerant state-machine replication (BFT-SMR) is a technique for hardening systems to tolerate arbitrary faults. Although robust, BFT-SMR protocols are very costly in terms of the number of required replicas (3f+1 to tolerate f faults) and of exchanged messages. However, with “hybrid” architectures, where “normal” components trust some “special” components to provide properties in a trustworthy manner, the cost of using BFT can be dramatically reduced. Unfortunately, even though such hybridization techniques decrease the message/time/space complexity of BFT protocols, they also increase their structural complexity.

Therefore, we introduce Asphalion, the first theorem prover-based framework for verifying implementations of hybrid systems and protocols. It relies on three novel languages: (1) HyLoE: a Hybrid Logic of Events to reason about hybrid fault models; (2) MoC: a Monadic Component language to implement systems as collections of interacting hybrid components; and (3) LoCK: a sound Logic of events-based Calculus of Knowledge to reason about both homogeneous and hybrid systems at a high-level of abstraction (thereby allowing reusing proofs, and capturing the high-level logic of distributed systems). In addition, Asphalion supports compositional reasoning, e.g., through mechanisms to lift properties about trusted-trustworthy components, to the level of the distributed systems they are integrated in. As a case study, we have verified crucial safety properties (e.g., agreement) of several implementations of hybrid protocols.

Marijana Lazic, TU Munich, Germany

Parameterized Verification of Randomized Consensus Algorithms under Round-Rigid Adversaries

Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized consensus algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where processes enter round r only after all processes finished round r−1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or’s and Bracha’s seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.

This is joint work with Nathalie Bertrand, Igor Konnov and Josef Widder.

Vincent Gramoli, University of Sydney, Australia

Formal Verification of Blockchain Byzantine Fault Tolerance 

Bio: Vincent Gramoli is an Associate Professor in Distributed Computing at the University of Sydney. He has been affiliated with Cornell University in the US, INRIA in France, EPFL in Switzerland and CSIRO in Australia. He is the Chair of the Blockchain Technical Committee for the Australian Computer Society and a Future Fellow of the Australian Research Council.

Faith Ellen, University of Toronto, Canada

Proving the Correctness of an Optimal Implementation of Fetch-and-Increment

In 2013, Philipp Woelfel and I presented a wait-free implementation of a Fetch-and-Increment object shared by n processes from LL/SC objects and registers. The step complexity of each fetch-and-increment operation takes O(log n) steps, which matches a known lower bound. For modularity, the implementation uses aggregator objects, which we introduced and  implemented from LL/SC objects and registers. In this talk, I will discuss our hand-written proof of correctness of this implementation and some of the reasons why it is difficult.

Bernhard Kragl, IST Austria, Austria

Inductive Sequentialization of Asynchronous Programs

Asynchronous programs are notoriously difficult to reason about because they spawn computation tasks which take effect asynchronously in a non-deterministic way. This complexity can be amplified even more by the execution platform, for instance, when programs execute over an unreliable network where messages can be reordered, dropped, or duplicated. Devising inductive invariants for such programs requires apprehending complex relationships between an unbounded number of computation tasks in arbitrarily long executions.

We propose a proof methodology, called inductive sequentialization, that sidesteps this complexity. This methodology provides a novel induction argument for the verification of an asynchronous program, and supports establishing a sequential reduction, i.e., a sequential program which captures every behavior of the original program, up to reordering of commutative actions. The essence of our methodology is a proof rule that combines commutativity arguments, induction, and abstraction in order to establish the soundness of a given sequential reduction. We have successfully applied inductive sequentialization to a diverse set of message-passing protocols, including leader election protocols, Two-Phase Commit, and Paxos. The sequential reductions we obtain correspond to executions of these protocols in an idealized synchronous environment where processes act in a fixed order and at the same speed. These are generally the simplest executions to reason about.

Roman Kuznets, TU Wien, Austria

Byzantine Causal Cone

To prove the correctness of a given distributed algorithm, it is necessary to verify that each action is taken only when the global system state allows it. However, due to the incomplete local view of each agent, the Knowledge of Preconditions Principle (KoP), formulated by Yoram Moses, lifts preconditions to the epistemic level. KoP states that, for any condition that is specified as necessary for an agent to perform a certain action, this agent knowing that the condition is fulfilled is also necessary for performing this action. It is well known that causality in asynchronous distributed systems, i.e., those where agents do not have access to a global synchronized clock, is governed solely by messages the agents exchange: an agent cannot know what happened to another agent without a chain of messages delivering this information, leading to the concept of a causal cone, first introduced by Leslie Lamport.

In this talk, we discuss the impact of byzantine failures on causality in asynchronous systems. If any agent can arbitrarily violate its protocol, e.g., send incorrect information, possibly different information to different respondents, then a simple chain of messages is not sufficient anymore. We provide an elaborate modeling and analysis framework for multi-agent systems with byzantine faults and use it to describe the byzantine analog of Lamport’s causal cone, the limitations on what can be known in principle, as well as the necessary conditions for achievable states of knowledge in fault-tolerant distributed systems.

This is joint work with Kristina Fruzsa, Laurent Prosperi and Ulrich Schmid.

András Vörös, Budapest University of Technology and Economics, Hungary

Modeling, verification and code generation for distributed reactive controllers – An engineer-centric toolchain

The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous, and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provided the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this talk, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting a case study from the cyber-physical system domain.

Swen Jacobs, CISPA Helmholtz Center for Information Security, Germany

Parameterized Reasoning for Distributed Systems with Consensus

Programmers make building distributed systems tractable by using a wide variety of abstractions to compose complex systems out of smaller components — for example, managing coordination between distributed processes using libraries that provide locking or consensus. Unfortunately, verification techniques for distributed systems typically do not match this style of programming, and modeling distributed systems often requires erasing these layers of abstraction to represent an entire program as a monolithic whole. We are working on a new approach to automatically verifying distributed systems that use consensus as a component, based on the following ingredients: i) a new system model that offers a consensus abstraction to provide global semantics for consensus while eliding specific algorithmic details, ii) a new abstract model that pushes the frontiers of decidability for parameterized verification of distributed systems and can capture programs that use our consensus abstraction. Given these ingredients, we present a sound and relatively complete parameterized verification procedure for safety properties of distributed systems that use consensus. We further show how to use this procedure to synthesize correct systems given partial process definitions. We have implemented to approach in a prototype tool, and show on several case studies that we are able to successfully synthesize and verify distributed systems that build on consensus without having to reason directly about the internals of consensus.

Summary of the workshop

Distributed algorithms is an active research field; their applications range from Internet applications over cloud computing to safety-critical control systems. Whereas many applications are of critical importance, the correctness of distributed algorithms is usually based on very subtle mathematical arguments. Consequently, one easily can make mistakes with hand-written proofs, which reduces the trust in the correctness of these systems.

In the last decades, formal methods were proven to be useful for the verification of many hardware and software systems. For distributed algorithms, the application of formal methods was limited: formal methods have been used for finding bugs in distributed algorithms, and to a much smaller extent formal methods were used in computer-aided verification of simple distributed algorithms. However, to verify more involved distributed algorithms, one cannot easily apply existing verification tools. To be eventually able to do this, an interdisciplinary effort from the concerned fields of formal methods, logic in computer science, and distributed algorithm theory is required.

The topics of interest for the FRIDA workshop are:

• models for distributed algorithms
• model checking
• proof assistants & theorem proving
• parameterized model checking
• integration of different verification techniques
• concurrency
• distributed algorithm theory
• benchmark distributed algorithms
• fault tolerance
• synthesis
• automated code generation for distributed systems
• run-time verification of distributed systems

Organization

• Swen Jacobs (CISPA Helmholtz Center for Information Security)
• Igor Konnov (INRIA Nancy & LORIA)
• Stephan Merz (INRIA Nancy & LORIA)
• Josef Widder (TU Wien)

Previous editions

Starting a productive dialogue between distributed algorithms and verification communities was the goal of a successful Dagstuhl Seminar “Formal Verification of Distributed Algorithms”which was held in April 2013. During this seminar, the participants agreed that a series of workshops should be held in order to strengthen the community that does research on these issues. The 1^st workshop on Formal Reasoning in Distributed Algorithms took place in Vienna as part of the Vienna Summer of Logic’14 and Federated Logic Conference’14. The 2^ndFRIDA workshop took place in Grenoble as part of FORTE’15. The 3^rd FRIDA workshop was organized in Marrakech as part of NETYS’16. The 4^th FRIDA workshop took place in Vienna as part of DISC 2017. The 5^th FRIDA workshop was co-located with CAV 2018, which was held as part of the Federated Logic Conference (FLoC).