CISPA
Browse
cispa_all_3075.pdf (401.17 kB)

Canonical Representations of k-Safety Hyperproperties

Download (401.17 kB)
conference contribution
posted on 2023-11-29, 18:11 authored by Bernd FinkbeinerBernd Finkbeiner, Lennart Haas, Hazem Torfah
Hyperproperties elevate the traditional view of trace properties form sets of traces to sets of sets of traces and provide a formalism for expressing information-flow policies. For trace properties, algorithms for verification, monitoring, and synthesis are typically based on a representation of the properties as omega-automata. For hyperproperties, a similar, canonical automata-theoretic representation is, so far, missing. This is a serious obstacle for the development of algorithms, because basic constructions, such as learning algorithms, cannot be applied. In this paper, we present a canonical representation for the widely used class of regular k-safety hyperproperties, which includes important polices such as noninterference. We show that a regular k-safety hyperproperty S can be represented by a finite automaton, where each word accepted by the automaton represents a violation of S. The representation provides an automata-theoretic approach to regular k-safety hyperproperties and allows us to compare regular k-safety hyperproperties, simplify them, and learn such hyperproperties. We investigate the problem of constructing automata for regular k-safety hyperproperties in general and from formulas in HyperLTL, and provide complexity bounds for the different translations. We also present a learning algorithm for regular k-safety hyperproperties based on the L* learning algorithm for deterministic finite automata.

History

Preferred Citation

Bernd Finkbeiner, Lennart Haas and Hazem Torfah. Canonical Representations of k-Safety Hyperproperties. In: IEEE Computer Security Foundations Symposium (CSF). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

IEEE Computer Security Foundations Symposium (CSF)

Legacy Posted Date

2020-05-25

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3075, title = "Canonical Representations of k-Safety Hyperproperties", author = "Finkbeiner, Bernd and Haas, Lennart and Torfah, Hazem", booktitle="{IEEE Computer Security Foundations Symposium (CSF)}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC