The 8th Workshop on Formal Reasoning in Distributed Algorithms

Dates: October 4th and October 8th 2021

Online workshop from 4pm to 8pm CEST (time in Freiburg, Germany).

The workshop is organized as part of DISC 2021.

News

Program

  • Monday, October 4th
    • 4pm to 5pm: Keynote by Julian Loss, CISPA Helmholtz Center for Information Security
      Formal Security Guarantees for Distributed Consensus Algorithms (click to expand the abstract)

      Distributed Consensus is the fundamental problem of agreeing on a common output in a network of pairwise connected parties. It can be studied under various network and setup assumptions that determine the parameters for which a solution exists. Proving security and correctness of consensus algorithms is known to be a subtle and error-prone task. In this talk, we will focus on recent advances in the area of distributed consensus and explain some of the key challenges that arise. We also discuss how tools from formal verification could be helpful to address them.

    • 5pm to 5:40pm: Joseph Tassarotti, Boston College
      Modular Verification of Distributed Systems with Grove (click to expand the abstract)

      Grove is a Concurrent Separation Logic (CSL) framework for distributed systems, with a focus on modular verification of servers and client-side libraries. To enable this, Grove uses the CSL idea of ownership of resources. We introduce a duplicable ownership specification for unreliable remote procedure calls and an escrow pattern for proving ownership transfer over unreliable networks. Using Grove we developed and verified an example system written in Go consisting of an RPC library, a sharded key-value store with support for dynamically adding new servers and rebalancing shards, a lock service, and a bank application that supports atomic transfers across accounts that live in different shards. The proofs are mechanized in the Coq proof assistant using the Iris library and Goose tool for verifying Go.

    • 5:40pm to 5:50pm: break
    • 5:50pm to 6:30pm: Christopher Goes
      Formal reasoning about privacy and incentive compatibility in zero-knowledge protocol design (click to expand the abstract)

      Zero-knowledge proof systems (ZKPs) provide a means by which to separate verification of protocol compliance from contents of protocol interactions, allowing privacy for users of distributed systems with public replicated state, compact proofs of correct behaviour, and recursive proof recombination of sequenced state machine transitions. As a relatively recent entrant into the protocol architecture toolset, however, zero-knowledge proof constructions utilised in distributed systems are not well formalised, both in the sense of formalisation of the arithmetic circuits required by the structure of the proof systems and in the sense of reasoning about gestalt safety properties of protocols which utilise zero-knowledge proofs as components.
      In this talk, I will outline the design space of zero-knowledge proofs as constituent components of distributed systems, focusing on where they can provide otherwise unobtainable privacy or benefits to asymmetric complexities, then discuss the necessary components of a mature verification landscape in both senses of circuit verification and protocol verification as discussed above. Specifically, I will cover Heliax's development of the dependently-typed language Juvix which can compile to arithmetic circuits and reason about their properties like a proof assistant such as Agda or Coq, discuss our research into zero-knowledge proofs as possible constituent components of incentive-compatible sparse gossip networks and BFT-like consensus algorithms, and enumerate outstanding research questions (of which there are many!)

    • 6:30pm to 7:10pm: Bernhard Kragl
      The Civl Verifier (click to expand the abstract)

      Civl is a static verifier for concurrent programs designed around the conceptual framework of layered refinement, which views the task of verifying a program as a sequence of program simplification steps each justified by its own invariant. Civl verifies a layered concurrent program that compactly expresses all the programs in this sequence and the supporting invariants. In this talk we present the design and implementation of the Civl verifier.

    • 7:10pm to 8:00pm: discussion, maybe in breakout rooms
  • Friday, October 8th
    • 4pm to 5pm: Keynote by Jochen Hoenicke
      A compositional proof of the Mach shootdown algorithm for TLB consistency
      (joint work with Rupak Majumdar and Andreas Podelski)
    • 5pm to 5:40pm: Sreeja S Nair, Adlink Technology Labs, France
      Exploring the coordination lattice (click to expand the abstract)

      Distributed applications support concurrent operations on their replicas to ensure high availability and low latency. Too much concurrency might violate an application invariant. Verification can say if a distributed application with the given coordination is safe. The required coordination can be implemented in many ways, trading overhead against parallelism. This talk will focus on capturing different dimensions of the subclass of coordination, distributed locks, into a Coordination Lattice. In particular, for a given workload, we look into the impact of a coordination configuration, with granularity, mode, and placement dimensions, on the performance of a distributed application.

    • 5:40pm to 5:50pm: break
    • 5:50pm to 6:30pm: Karem Sakallah, University of Michigan
      Regularity, Quantification, and Hierarchical Strengthening: A New Approach to Verify Distributed Protocols (click to expand the abstract)

      Finite-state model checking has made significant advances in the last few years. For example, our AVR hardware model checker for safety properties successfully handled an industrial design containing over 60,000 state bits and was the overall winner in last year's hardware model checking competition. Three main ingredients made this possible: a) highly-scalable SAT and SMT solvers, b) approximate reachability algorithms based on IC3-style incremental induction, and c) equality abstraction of data.

      Inspired by our work on hardware model checking with AVR, we developed IC3PO, a new verifier that automatically produces quantified inductive invariants proving the correctness of unbounded distributed protocols. IC3PO takes advantage of the spatial and temporal regularity of unbounded protocols to reduce the unbounded verification problem to a sequence of small finite protocol instances (up to a cutoff size) that incrementally reveal the quantified strengthening assertions needed to establish inductiveness and prove safety.

      The talk will sketch the IC3 finite incremental induction algorithm and show how it is modified in IC3PO to automatically infer and generalize the quantifier prefixes in the finite strengthening assertions by taking advantage of spatial and temporal regularity.

      IC3PO also takes advantage of the hierarchical specification of complex protocols, such as Lamport's Paxos, using a top-down stepwise invariant strengthening procedure. Using a four-level hierarchy, the talk will conclude by describing how IC3PO automatically produced the same inductive invariant for Paxos as its manually-written proof.

      There is still much to explore in extending automatic verification to the domain of unbounded protocols. We believe this is a promising first step.

    • 6:30pm to 7:10pm: Roopsha Samanta, Purdue University
      Taming Unbounded Distributed Systems with Modular, Bounded Verification (click to expand the abstract)

      Modern distributed services are typically built in a modular fashion using core distributed protocols as building blocks. The ubiquity of some of these building blocks has sparked several valiant verification efforts for them in the last decade. Oddly, there have been far fewer verification efforts that go beyond core protocols and target distributed services built on top of such core protocols. In our Discover[i] project, we seek to develop modular, scalable, fully-automated verification approaches for distributed systems that mimic their modular design. In particular, we advocate an approach based on assuming that the underlying core protocols are verified separately and encapsulating their complexities within cleanly-defined abstractions.

      In this talk, I will present QuickSilver, a modeling and verification framework for distributed systems built on top of verified distributed agreement protocols such as consensus. I will show how our encoding of agreement protocols facilitates decidable and scalable verification for a broad class of systems including a datastore, a lock service, a surveillance system, and several other interesting case studies adapted from real-world applications.

    • 7:10pm to 8:00pm: discussion, maybe in breakout rooms

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 include the following topics, as they apply to distributed algorithms and systems:

  • formal modeling
  • model checking
  • interactive theorem proving
  • parameterized model checking
  • integration of different verification techniques
  • benchmarking
  • synthesis
  • run-time verification
  • testing
  • invariant inference

Organizers

Main organizers

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 1st 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 2nd FRIDA workshop took place in Grenoble as part of FORTE’15. The 3rd FRIDA workshop was organized in Marrakech as part of NETYS’16. The 4th FRIDA workshop took place in Vienna as part of DISC 2017. The 5th FRIDA workshop was co-located with CAV 2018, which was held as part of the Federated Logic Conference (FLoC). The 6th workshop was co-located with DISC 2019 in Budapest, Hungary. Finally, last year, FRIDA 2020 took place as an online workshop at QONFEST 2020.