CISPA
Browse

How to Win First-Order Safety Games

Download (1.02 MB)
conference contribution
posted on 2023-11-29, 18:15 authored by Helmut Seidl, Christian Müller, Bernd FinkbeinerBernd Finkbeiner
First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Functional correctness or noninterference of these systems have conveniently been formulated as safety or hypersafety properties, respectively. In this article, we take the step from verification to synthesis---tackling the question whether it is possible to automatically synthesize predicates to enforce safety or hypersafety properties like noninterference. For that, we generalize FO transition systems to FO safety games. For FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of properties---for example noninterference. We identify a non-trivial sub-class where invariants can be proven inductive and FO winning strategies be effectively constructed. We also show how the extraction of weakest FO winning strategies can be reduced to SO quantifier elimination itself. We demonstrate the usefulness of our approach by automatically synthesizing nontrivial FO specifications of messages in a leader election protocol as well as for paper assignment in a conference management system to exclude unappreciated disclosure of reports.

History

Preferred Citation

Helmut Seidl, Christian Müller and Bernd Finkbeiner. How to Win First-Order Safety Games. In: Verification, Model Checking and Abstract Interpretation (VMCAI). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Verification, Model Checking and Abstract Interpretation (VMCAI)

Legacy Posted Date

2021-03-04

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3377, title = "How to Win First-Order Safety Games", author = "Seidl, Helmut and Müller, Christian and Finkbeiner, Bernd", booktitle="{Verification, Model Checking and Abstract Interpretation (VMCAI)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC