CISPA
Browse
Beutner24.pdf (694.62 kB)

Automated Software Verification of Hyperliveness

Download (694.62 kB)
conference contribution
posted on 2024-03-15, 10:08 authored by Raven BeutnerRaven Beutner
Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification of $k$-safety properties, i.e., properties that state that all $k$-tuples of execution traces satisfy a given property. In this paper, we study the automated verification of richer properties that combine universal and existential quantification over executions. Concretely, we consider $\forall^k\exists^l$ properties, which state that for all $k$ executions, there exist $l$ executions that, together, satisfy a property. This captures important non-$k$-safety requirements, including hyperliveness properties such as generalized non-interference, opacity, refinement, and robustness. We design an automated constraint-based algorithm for the verification of $\forall^k\exists^l$ properties. Our algorithm leverages a sound-and-complete program logic and a (parameterized) strongest postcondition computation. We implement our algorithm in a tool called ForEx and report on encouraging experimental results.

History

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Tools and Algorithms for Construction and Analysis of Systems (TACAS)

BibTeX

@conference{Beutner:2024, title = "Automated Software Verification of Hyperliveness", author = "Beutner, Raven", year = 2024, month = 3 }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC