Hyperproperty

Hyperproperties are defined in terms of traces of a computational system. A trace is a sequence of states; a system is a set of traces. Intuitively, a program corresponds to the set of all of its possible execution traces, given any inputs. Formally, the set of traces over a set of states $\backslash Sigma$ is $\backslash Phi\backslash triangleq\backslash Sigma^\backslash omega$.

This representation is expressive enough to encompass several computational models, including labeled transition systems{{sfn|Clarkson|Schneider|2010|loc=p. 23: "A labeled transition system [...] can be encoded as a set of traces."}} and state machines.{{sfn|Clarkson|Schneider|2010|loc=p. 25: "A state machine M [...] can be encoded as a set of traces."}}

A trace property is a set of traces. Safety and liveness properties are trace properties. Formally, a trace property is an element of $\backslash mathbb\{P\}(\backslash Phi)$, where $\backslash mathbb\{P\}$ is the powerset operator. A hyperproperty is a set of trace properties, that is, an element of $\backslash mathbb\{P\}(\backslash mathbb\{P\}(\backslash Phi))$.

Trace properties may be divided into safety properties (intuitively, properties that ensure "bad things don't happen") and liveness properties ("good things do happen"), and every trace property is the intersection of a safety property and a liveness property.{{Cite journal |last1=Alpern |first1=Bowen |last2=Schneider |first2=Fred B. |date=1985-10-07 |title=Defining liveness |url=https://dx.doi.org/10.1016/0020-0190%2885%2990056-0 |journal=Information Processing Letters |language=en |volume=21 |issue=4 |pages=181–185 |doi=10.1016/0020-0190(85)90056-0 |issn=0020-0190}} Analogously, hyperproperties may be divided into hypersafety and hyperliveness hyperproperties, and every hyperproperty is an intersection of a safety hyperproperty and a liveness hyperproperty.{{sfn|Clarkson|Schneider|2010|p=21}}

$k$-safety properties are safety hyperproperties such that every violation of the property can be witnessed by a set of at most $k$ traces.{{Cite book |last1=Finkbeiner |first1=Bernd |last2=Haas |first2=Lennart |last3=Torfah |first3=Hazem |title=2019 IEEE 32nd Computer Security Foundations Symposium (CSF) |chapter=Canonical Representations of k-Safety Hyperproperties |date=June 2019 |chapter-url=https://ieeexplore.ieee.org/document/8823753 |pages=17–1714 |doi=10.1109/CSF.2019.00009|isbn=978-1-7281-1407-1 |s2cid=201848133 }}

• Every safety property can be lifted to a 1-safety hyperproperty that expresses the same condition.{{sfn|Clarkson|Schneider|2010|loc=p. 11: "Safety properties lift to safety hyperproperties"}}
• $k$-safety hyperproperties:
• $k=1$ (lifts of safety properties):
• false, defined to be the set containing the empty set. Formally, $\backslash mathbf\{false\}\backslash triangleq\; \backslash \{\backslash emptyset\backslash \}$. This hyperproperty is not satisfied by any system.{{sfn|Clarkson|Schneider|2010|loc=p. 15: "The hyperproperty false, defined as \{\emptyset\}, is hypersafety but not hyperliveness".}}
• true, defined to be the set of all traces. Formally, $\backslash mathbf\{true\}\backslash triangleq\; \backslash Phi$. This hyperproperty is satisfied by all systems.{{sfn|Clarkson|Schneider|2010|p=44}}
• Access control{{sfn|Clarkson|Schneider|2010}}
• $k=2$:
• Monotonicity{{sfn|Sousa|Dillig|2016}}
• Injectivity{{sfn|Sousa|Dillig|2016}}
• Symmetry, anti-symmetry, and asymmetry{{sfn|Sousa|Dillig|2016}}
• Observational determinism{{sfn|Clarkson|Schneider|2010|loc=p. 13: "observational determinism OD (2.6) cannot be expressed as a 2-safety property, but it is a 2-safety hyperproperty"}}
• Noninterference
• $k=3$
• Transitivity{{sfn|Sousa|Dillig|2016}}
• $k=4$
• Associativity{{sfn|Sousa|Dillig|2016}}

Since hyperproperties are exactly the elements of the power set $\backslash mathbb\{P\}(\backslash mathbb\{P\}(\backslash Phi))$, they are closed under intersection and union.

The lower Vietoris topology of a standard topology on trace properties yields a topology on the set of hyperproperties.{{sfn|Clarkson|Schneider|2010|p=19}}

Several program logics{{sfn|Sousa|Dillig|2016}}{{Cite arXiv |last1=Dardinier |first1=Thibault |last2=Müller |first2=Peter |date=2023-01-24 |title=Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version) |class=cs.LO |eprint=2301.10037 }} have been developed for checking that a program conforms to a hyperproperty.

HyperLTL{{Cite journal |last1=D'Osualdo |last2=Farzan |last3=Dreyer |date=2022 |title=Proving hypersafety compositionally |url=https://dl.acm.org/doi/abs/10.1145/3563298 |journal=Proceedings of the ACM on Programming Languages |language=en |volume=6 |issue=OOPSLA2 |pages=289–314 |arxiv=2209.07448 |doi=10.1145/3563298|s2cid=252284134 }} and some model checking algorithms{{Cite book |last1=Finkbeiner |first1=Bernd |last2=Rabe |first2=Markus N. |last3=Sánchez |first3=César |title=Computer Aided Verification |chapter=Algorithms for Model Checking HyperLTL and HyperCTL $$^*$$ |date=2015 |editor-last=Kroening |editor-first=Daniel |editor2-last=Păsăreanu |editor2-first=Corina S.|editor2-link= Corina Păsăreanu |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |volume=9206 |pages=30–48 |doi=10.1007/978-3-319-21690-4_3 |isbn=978-3-319-21690-4 |doi-access=free}}{{Cite book |last1=Hsu |first1=Tzu-Han |last2=Sánchez |first2=César |last3=Bonakdarpour |first3=Borzoo |title=Tools and Algorithms for the Construction and Analysis of Systems |chapter=Bounded Model Checking for Hyperproperties |date=2021 |editor-last=Groote |editor-first=Jan Friso |editor2-last=Larsen |editor2-first=Kim Guldstrand |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |volume=12651 |pages=94–112 |doi=10.1007/978-3-030-72016-2_6 |isbn=978-3-030-72016-2 |pmc=7979203}} have been developed for checking that a finite state system conforms to a hyperproperty.

{{Reflist}}

• {{Cite journal |last1=Clarkson |first1=Michael R. |last2=Schneider |first2=Fred B. |date=2010-09-20 |editor-last=Sabelfeld |editor-first=Andrei |title=Hyperproperties |url=https://www.medra.org/servlet/aliasResolver?alias=iospress&doi=10.3233/JCS-2009-0393 |journal=Journal of Computer Security |volume=18 |issue=6 |pages=1157–1210 |doi=10.3233/JCS-2009-0393|s2cid=218604768 }}
• {{Cite book |last1=Sousa |first1=Marcelo |last2=Dillig |first2=Isil |title=Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation |chapter=Cartesian hoare logic for verifying k-safety properties |date=2016-06-02 |chapter-url=https://doi.org/10.1145/2908080.2908092 |series=PLDI '16 |location=New York, NY, USA |publisher=Association for Computing Machinery |pages=57–69 |doi=10.1145/2908080.2908092 |isbn=978-1-4503-4261-2|s2cid=17433405 }}

{{Program analysis}}

Category:Program analysis