Asphalion: Trustworthy shielding against byzantine faults

Ivana Vukotic, Vincent Rahli, Paulo Esteves-Veríssimo

Research output: Contribution to journalArticlepeer-review

1 Scopus citations


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.

Original languageEnglish (US)
Article numberA138
JournalProceedings of the ACM on Programming Languages
Issue numberOOPSLA
StatePublished - Oct 2019

Bibliographical note

Publisher Copyright:
© 2019 Association for Computing Machinery. All rights reserved.


  • Byzantine faults
  • Compositional reasoning
  • Coq
  • Distributed systems
  • Fault-tolerance
  • Formal verification
  • Hybrid protocols
  • Knowledge calculus
  • MinBFT
  • Monad
  • Step-indexing

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality


Dive into the research topics of 'Asphalion: Trustworthy shielding against byzantine faults'. Together they form a unique fingerprint.

Cite this