On March 30, 2023 at 14:00 EEST, Denisa Diaconescu (University of Bucharest & Runtime Verification) will give a talk in the Logic Seminar.
Title: VLSM: A General Framework for Reasoning About Faulty Distributed Systems
Abstract:
Formally modeling and reasoning about distributed systems with faults is a challenging task [1]. Depending on the system model, an execution of a distributed protocol may be subject to many kinds of faults, from simple recoverable component crashes to Byzantine adversarial actions [4]. Each kind of failure may then require specific actions for evasion or recovery by the affected components.
To address this problem, we recently proposed the theory of Validating Labeled State transition and Message production systems (VLSMs) as a general approach to modeling and verifying distributed protocols executing in the presence of faults [5]. In particular, VLSM executions can be subject to equivocation behavior. Equivocation refers to claiming different beliefs about the state of the protocol to different parts of the system in order to steer the protocol-following components into making inconsistent decisions; messages received from equivocating components seem to be valid messages [3]. For example, if a system tries to come to a consensus about the value of a bit, an equivocating component may claim the bit is 0 to one part of the system, and 1 to the other. Equivocation behavior cannot be produced by a single protocol execution, but only by multiple protocol executions, i.e., an equivocating component behaves as if running multiple copies of the protocol.
Our VLSM-based modeling and verification methodology for distributed protocols follows the correct-by-construction approach for design and development [2]: we define an abstract class of protocols (satisfying some generic abstract properties), prove general results about protocols belonging to the class, and then obtain correct-by-construction protocols by concretely instantiating the abstract components, or, alternatively, prove that concrete protocols satisfy those requirements.
References:
[1] Pedro Fonseca, Kaiyuan Zhang, Xi Wang & Arvind Krishnamurthy (2017): An Empirical Study on the Correctness of Formally Verified Distributed Systems. In: European Conference on Computer Systems, pp. 328–343, doi:10.1145/3064176.3064183.
[2] David Gries (1981): The Science of Programming. Springer, doi:10.1007/978-1-4612-5983-1.
[3] Alexander Jaffe, Thomas Moscibroda & Siddhartha Sen (2012): On the price of equivocation in Byzantine agreement. In: Symposium on Principles of Distributed Computing, pp. 309–318, doi:10.1145/2332432.2332491.
[4] Leslie Lamport, Robert Shostak & Marshall Pease (1982): The Byzantine Generals Problem. ACM Transactions on Programming Languages and Systems 4(3), pp. 382–401, doi:10.1145/357172.357176.
[5] V. Zamfir, M. Calancea, D. Diaconescu, W. Kołowski, B. Moore, K. Palmskog, T. F. Șerbănuță, M. Stay, D. Trufaș, & J. Tušil (2022): Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems. arXiv:2202.12662 [cs.DC].
The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.