Asphalion: trustworthy shielding against Byzantine faults

Research output: Contribution to journalConference articlepeer-review

Standard

Asphalion : trustworthy shielding against Byzantine faults. / Vukotic, Ivana; Rahli, Vincent; Veríssimo, Paulo Jorge Esteves.

In: Proceedings of the ACM on Programming Languages, Vol. 3, No. OOPSLA, 138, 10.10.2019.

Research output: Contribution to journalConference articlepeer-review

Harvard

APA

Vancouver

Author

Vukotic, Ivana ; Rahli, Vincent ; Veríssimo, Paulo Jorge Esteves. / Asphalion : trustworthy shielding against Byzantine faults. In: Proceedings of the ACM on Programming Languages. 2019 ; Vol. 3, No. OOPSLA.

Bibtex

@article{3231a98319f14c878abd88ca879a56ad,
title = "Asphalion: trustworthy shielding against Byzantine faults",
abstract = "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. ",
author = "Ivana Vukotic and Vincent Rahli and Ver{\'i}ssimo, {Paulo Jorge Esteves}",
year = "2019",
month = oct,
day = "10",
doi = "10.1145/3360564",
language = "English",
volume = "3",
journal = "Proceedings of the ACM on Programming Languages",
issn = "2475-1421",
publisher = "Association for Computing Machinery ",
number = "OOPSLA",
note = "SPLASH/OOPSLA 2019 ; Conference date: 23-10-2019 Through 25-10-2019",

}

RIS

TY - JOUR

T1 - Asphalion

T2 - SPLASH/OOPSLA 2019

AU - Vukotic, Ivana

AU - Rahli, Vincent

AU - Veríssimo, Paulo Jorge Esteves

PY - 2019/10/10

Y1 - 2019/10/10

N2 - 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.

AB - 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.

U2 - 10.1145/3360564

DO - 10.1145/3360564

M3 - Conference article

VL - 3

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - OOPSLA

M1 - 138

Y2 - 23 October 2019 through 25 October 2019

ER -