3 Forsyte papers accepted at CAV 2019

Papers 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

Latest News

FORSYTE’s 2018 paper awards

FORSYTE has had a quite successful year: Adrian Rebola Pardo and his co-authors received the IJCAR best paper award for their paper Extended Resolution Simulates DRAT, Mitra Tabaei Befrouei and her co-authors received an OOPSLA 2018 Distinguished Paper award for their paper Randomized Testing of Distributed Systems with Probabilistic Guarantees, and Thomas Pani received the […]

Continue reading

OOPSLA Distinguished Paper Award

Mitra Tabaei Befrouei and her co-authors from MPI-SWS Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic, received an OOPSLA’18 Distinguished Paper Award for their contribution “Randomized Testing of Distributed Systems with Probabilistic Guarantees” (Open Access article). Congratulations!

Continue reading

Zvonimir Rakamiric visiting FORSYTE

Prof. Zvonimir Rakamiric from the School of Computing at the University of Utah is spending his sabbatical with the FORSYTE group at TU Wien. He is generously sponsored by the Wolfgang Pauli Institute and a Pauli Fellow.

Continue reading

Helmut Veith Stipend Award Ceremony

The Vice Rector for Academic Affairs of TU Wien, Kurt Matyas, will award the scholarship recipient of the Helmut Veith Stipend at the award ceremony on Friday, April 06, 2018 in the Kontaktraum, starting at 17:05.

Continue reading

Full news archive