How to Win First-Order Safety Games
share
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 properties. In order to automatically synthesize predicates to enforce safety or noninterference, we generalize FO transition systems to FO safety games. For the important case of 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 noninterference properties. Based on general techniques for second-order quantifier elimination, we provide abstraction and refinement techniques to synthesize FO-expressible strategies that enforce safety. We demonstrate the usefulness of our approach by automatically inferring nontrivial FO specifications for message passing in a leader election protocol as well as for a conference management system to exclude unappreciated disclosure of reports.
READ FULL TEXT