{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:13:54Z","timestamp":1784182434929,"version":"3.55.0"},"reference-count":114,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/3360564","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Asphalion: trustworthy shielding against Byzantine faults"],"prefix":"10.1145","volume":"3","author":[{"given":"Ivana","family":"Vukotic","sequence":"first","affiliation":[{"name":"University of Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vincent","family":"Rahli","sequence":"additional","affiliation":[{"name":"University of Birmingham, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paulo","family":"Esteves-Ver\u00edssimo","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"DSN","year":"2014"},{"key":"e_1_2_2_2_1","volume-title":"Revisiting Fast Practical Byzantine Fault Tolerance. CoRR abs\/1712.01367","author":"Abraham Ittai","year":"2017"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.OPODIS.2017.25"},{"key":"e_1_2_2_4_1","volume-title":"Modeling in Event-B - System and Software Engineering","author":"Abrial Jean-Raymond","year":"1895"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_3"},{"key":"e_1_2_2_8_1","volume-title":"OPODIS","volume":"95","author":"Aspnes James","year":"2018"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90035-E"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064213"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2542181"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","volume-title":"Interactive Theorem Proving and Program Development","author":"Bertot Yves","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2014.43"},{"key":"e_1_2_2_15_1","volume-title":"Component Specification Using Event Classes. In CBSE 2009 (LNCS), Grace A. Lewis, Iman Poernomo, and Christine Hofmeister (Eds.)","volume":"5582","author":"Bickford Mark","year":"2009"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32275-7_30"},{"key":"e_1_2_2_17_1","volume-title":"Languages for Distributed Algorithms Workshop. http:\/\/www.nuprl.org\/documents\/Bickford\/LOE- LADA2012","author":"Bickford Mark","year":"2012"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281136"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1243418.1243422"},{"key":"e_1_2_2_20_1","unstructured":"BPaxos 2018. Mechanically Checked Safety Proof of a Byzantine Paxos Algorithm. http:\/\/lamport.azurewebsites.net\/tla\/ byzpaxos.html  BPaxos 2018. Mechanically Checked Safety Proof of a Byzantine Paxos Algorithm. http:\/\/lamport.azurewebsites.net\/tla\/ byzpaxos.html"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45174-8_7"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933057.2933120"},{"key":"e_1_2_2_24_1","unstructured":"Miguel Castro and Barbara Liskov. 1999a. A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm. Technical Memo MIT-LCS-TM-590. MIT.  Miguel Castro and Barbara Liskov. 1999a. A Correctness Proof for a Practical Byzantine-Fault-Tolerant Replication Algorithm. Technical Memo MIT-LCS-TM-590. MIT."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/296806.296824"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/214451.214456"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01843569"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04420-5_10"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_11"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-009-0084-6"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_12"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294280"},{"key":"e_1_2_2_34_1","unstructured":"R.L. Constable S.F. Allen H.M. Bromley W.R. Cleaveland J.F. Cremer R.W. Harper D.J. Howe T.B. Knoblock N.P. Mendler P.Panangaden J.T. Sasaki and S.F. Smith. 1986. Implementing mathematics with the Nuprl proof development system. Prentice-Hall Inc. Upper Saddle River NJ USA.  R.L. Constable S.F. Allen H.M. Bromley W.R. Cleaveland J.F. Cremer R.W. Harper D.J. Howe T.B. Knoblock N.P. Mendler P.Panangaden J.T. Sasaki and S.F. Smith. 1986. Implementing mathematics with the Nuprl proof development system. Prentice-Hall Inc. Upper Saddle River NJ USA."},{"key":"e_1_2_2_35_1","unstructured":"Coq 2019. The Coq Proof Assistant. http:\/\/coq.inria.fr\/  Coq 2019. The Coq Proof Assistant. http:\/\/coq.inria.fr\/"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-004-0110-7"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/RELDIS.2004.1353018"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxs148"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36080-8_21"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3087801.3087839"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2833312.2833321"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276529"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2015.2495213"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.90"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90014-9"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098243.3098261"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050038"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10181-1_20"},{"key":"e_1_2_2_54_1","volume-title":"Technical Report MIT\/LCS\/TR-961. Laboratory for Computer Science","author":"Garland S.","year":"2004"},{"key":"e_1_2_2_55_1","volume-title":"Garland and Nancy Lynch","author":"Stephen","year":"2000"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0097-7"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3212734"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1146\/annurev.cs.02.060187.000345"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/79147.79161"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.251.22"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146638"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"e_1_2_2_64_1","volume-title":"The SPIN Model Checker - primer and reference manual","author":"Holzmann Gerard J."},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022969405325"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2168836.2168866"},{"key":"e_1_2_2_67_1","volume-title":"USENIX Security Symposium, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 279\u2013296","author":"Kokoris-Kogias Eleftherios","year":"2016"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.03.006"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_2_74_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2004"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357176"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.OPODIS.2017.32"},{"key":"e_1_2_2_77_1","volume-title":"TrInc: Small Trusted Hardware for Large Distributed Systems. In USENIX","author":"Levin Dave","year":"2009"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21461-5_16"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978389"},{"key":"e_1_2_2_80_1","unstructured":"Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann.  Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann."},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_12"},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/2069216.2069252"},{"key":"e_1_2_2_84_1","volume-title":"Computational Lambda-Calculus and Monads","author":"Moggi Eugenio"},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_2_86_1","unstructured":"OCaml2C 2019. Interfacing C with OCaml. https:\/\/caml.inria.fr\/pub\/docs\/manual- ocaml\/intfc.html  OCaml2C 2019. Interfacing C with OCaml. https:\/\/caml.inria.fr\/pub\/docs\/manual- ocaml\/intfc.html"},{"key":"e_1_2_2_87_1","volume-title":"2014 USENIX Annual Technical Conference, USENIX ATC \u201914","author":"Ongaro Diego","year":"2014"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.345827"},{"key":"e_1_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_2_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_2_92_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02252679"},{"key":"e_1_2_2_93_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2017.39"},{"key":"e_1_2_2_94_1","volume-title":"Constable","author":"Rahli Vincent","year":"2015"},{"key":"e_1_2_2_95_1","volume-title":"Constable","author":"Rahli Vincent","year":"2017"},{"key":"e_1_2_2_96_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2012.6459943"},{"key":"e_1_2_2_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_22"},{"key":"e_1_2_2_98_1","volume-title":"Eighth Workshop on Hot Topics in System Dependability (HotDep\u201912)","author":"Schiper Nicolas"},{"key":"e_1_2_2_99_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2014.45"},{"key":"e_1_2_2_100_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2002.1022311"},{"key":"e_1_2_2_101_1","unstructured":"SecureBlue 2019. Secure Blue. https:\/\/researcher.watson.ibm.com\/researcher\/view_page.php?id=6904  SecureBlue 2019. Secure Blue. https:\/\/researcher.watson.ibm.com\/researcher\/view_page.php?id=6904"},{"key":"e_1_2_2_102_1","volume-title":"Programming and Proving with Distributed Protocols. In POPL","author":"Sergey Ilya","year":"2018"},{"key":"e_1_2_2_103_1","unstructured":"SGX 2019. SGX. https:\/\/software.intel.com\/en- us\/sgx  SGX 2019. SGX. https:\/\/software.intel.com\/en- us\/sgx"},{"key":"e_1_2_2_104_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2018.00018"},{"key":"e_1_2_2_105_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_2_2_107_1","unstructured":"TrustZone 2019. ARM TrustZone. https:\/\/www.arm.com\/products\/security- on- arm\/trustzone  TrustZone 2019. ARM TrustZone. https:\/\/www.arm.com\/products\/security- on- arm\/trustzone"},{"key":"e_1_2_2_108_1","volume-title":"Dilma Da Silva and Bryan Ford (Eds.)","author":"Porter Donald E."},{"key":"e_1_2_2_109_1","doi-asserted-by":"publisher","DOI":"10.1109\/SRDS.2007.20"},{"key":"e_1_2_2_110_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87779-0_32"},{"key":"e_1_2_2_111_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122480.1122497"},{"key":"e_1_2_2_112_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2002.1024739"},{"key":"e_1_2_2_113_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDSN.2000.857587"},{"key":"e_1_2_2_115_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2010.19"},{"key":"e_1_2_2_116_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2011.221"},{"key":"e_1_2_2_117_1","volume-title":"Asphalion: Trustworthy Shielding Against Byzantine Faults.","author":"Vukotic Ivana","year":"2019"},{"key":"e_1_2_2_118_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_119_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360564","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360564","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360564"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":114,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360564"],"URL":"https:\/\/doi.org\/10.1145\/3360564","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}