Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Thu 24 Oct 2019 11:00 - 11:22 at Olympia - Distributed Systems

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.

This program is tentative and subject to change.

Thu 24 Oct

11:00 - 12:30: OOPSLA - Distributed Systems at Olympia
splash-2019-oopsla11:00 - 11:22
Ivana VukoticSnT, University of Luxembourg, Vincent RahliUniversity of Birmingham, Paulo Esteves-VeríssimoSnT, University of Luxembourg
splash-2019-oopsla11:22 - 11:45
Zachary BenavidesUC Riverside, Keval VoraSimon Fraser University, Rajiv GuptaUC Riverside
splash-2019-oopsla11:45 - 12:07
Ragnar MogkTechnische Universität Darmstadt, Joscha DrechslerTechnische Universität Darmstadt, Guido SalvaneschiTechnische Universität Darmstadt, Mira MeziniTechnische Universität Darmstadt
splash-2019-oopsla12:07 - 12:30
Guido SalvaneschiTechnische Universität Darmstadt, Mirko KöhlerTechnische Universität Darmstadt, Daniel SokolowskiTechnische Universität Darmstadt, Philipp HallerKTH Royal Institute of Technology, Sebastian ErdwegJGU Mainz, Mira MeziniTechnische Universität Darmstadt