3 Forsyte papers accepted at CAV 2019
Thursday, Apr 18, 2019Papers co-authored by Jure Kukovec, Marijana Lazić, and Josef Widder were accepted to be presented at the 31st International Conference on Computer-Aided Verification.
Title: Reachability Analysis for AWS-based Networks
Authors: J. Backes, S. Bayless, B. Cook, C. Dodge, A. Gacek, A.J. Hu, T. Kahsai, B. Kocik, E. Kotelnikov, J. Kukovec, S. McLaughlin, J. Reed, N. Rungta, J. Sizemore, M. Stalzer, P. Srinivasan, P. Subotić, C. Varming, B. Whaley, Y. Wu
Abstract: Cloud services provide the ability to provision virtual networked infrastructure on demand over the internet. The rapid growth of these virtually provisioned cloud networks has increased the demand for automated reasoning tools capable of identifying misconfigurations or security vulnerabilities. This type of automation gives customers the assurance they need to deploy sensitive workloads. It can also dramatically reduce the cost and time-to-market for regulated customers looking to establish compliance certification for cloud-based applications. In this industrial case-study, we describe a new network reachability reasoning tool, called Tiros, that uses off-the-shelf automated theorem proving tools to fill this need. Tiros is the foundation of a recently introduced network security analysis feature in the Amazon Inspector service now available to millions of customers building applications in the cloud.
Tiros is also used within Amazon Web Services (AWS) to automate the checking of compliance certification and adherence to security invariants for many AWS services that build on existing AWS networking features.
Title: Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics
Authors: Idan Berkovits, Marijana Lazić, Giuliano Lossa, Oded Padon and Sharon Shoham
Abstract: Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only if it has received an acknowledgment from at least half of its peers. Verification of threshold-based protocols is extremely challenging as it involves two kinds of reasoning: first-order reasoning about the unbounded state of the protocol, together with reasoning about sets and cardinalities. In this work, we develop a new methodology for decomposing the verification task of such protocols into two decidable logics: EPR and BAPA. Our key insight is that such protocols use thresholds in a restricted way as a mean to obtain certain properties of “intersection” between sets. We define a language for expressing such properties, and present two translations: to EPR and BAPA. The EPR translation allows us to verify the protocol while assuming these properties, and the BAPA translation allows us to verify the correctness of the properties. We further develop an algorithm for automatically generating the properties needed for verifying a given protocol, facilitating a fully automated deductive verification. Using this technique we have verified several challenging benchmarks, including Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos.
Title: Communication-closed asynchronous protocols
Authors: Andrei Damian, Cezara Dragoi, Alexandru Militaru and Josef Widder.
Abstract: The verification of asynchronous fault-tolerant distributed
systems is challenging due to the exponential number of
interleavings, unbounded message buffers, and network
failures (e.g., processes crash or message loss). We propose a
method that, for a class of protocols, reduces the verification
of asynchronous fault-tolerant protocols to the verification of a
round-based synchronous ones. Synchronous protocols are easier
to verify due to fewer interleavings, bounded message buffers
etc. We implemented our reduction method and applied it to
several state machine replication and consensus algorithms, among
which are Multi-Paxos and Chandra&Toueg’s atomic broadcast. The
resulting synchronous protocols are verified using existing
deductive verification methods.
Preliminary version: https://hal.inria.fr/hal-01991415v1