(2019) Canonical Representations of k-Safety Hyperproperties.
|
Text
FHT19.pdf Download (410kB) | Preview |
Abstract
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Conference: | CSF IEEE Computer Security Foundations Symposium (was CSFW) |
| Depositing User: | Bernd Finkbeiner |
| Date Deposited: | 25 May 2020 11:29 |
| Last Modified: | 11 May 2021 13:49 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3075 |
Actions
Actions (login required)
 |
View Item |