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.
Thu 24 Oct Times are displayed in time zone: Beirut change
11:00 - 12:30 | |||
11:00 22mTalk | Asphalion: Trustworthy Shielding against Byzantine Faults OOPSLA Ivana VukoticSnT, University of Luxembourg, Vincent RahliUniversity of Birmingham, Paulo Esteves-VeríssimoSnT, University of Luxembourg DOI | ||
11:22 22mTalk | DProf: Distributed Profiler with Strong Guarantees OOPSLA DOI | ||
11:45 22mTalk | A Fault-Tolerant Programming Model for Distributed Interactive Applications OOPSLA Ragnar MogkTechnische Universität Darmstadt, Joscha DrechslerTechnische Universität Darmstadt, Guido SalvaneschiTechnische Universität Darmstadt, Mira MeziniTechnische Universität Darmstadt DOI | ||
12:07 22mTalk | Language-Integrated Privacy-Aware Distributed Queries OOPSLA 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 DOI |