Hyperproperty

In computer science, hyperproperties are a formalism for describing properties of computational systems. Hyperproperties generalize safety and liveness properties, and can express properties such as non-interference and observational determinism.

Definitions

Traces and systems

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 $\Sigma$ is $\Phi \triangleq \Sigma ^{\omega }$ .

This representation is expressive enough to encompass several computational models, including labeled transition systems[1] and state machines.[2]

Hyperproperties

A trace property is a set of traces. Safety and liveness properties are trace properties. Formally, a trace property is an element of $\mathbb {P} (\Phi )$ , where $\mathbb {P}$ is the powerset operator. A hyperproperty is a set of trace properties, that is, an element of $\mathbb {P} (\mathbb {P} (\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.[3] Analogously, hyperproperties may be divided into hypersafety and hyperliveness hyperproperties, and every hyperproperty is an intersection of a safety hyperproperty and a liveness hyperproperty.[4]

$k$ -safety properties are safety hyperproperties such that every violation of the property can be witnessed by a set of at most $k$ traces.[5]

Examples

Every safety property can be lifted to a 1-safety hyperproperty that expresses the same condition.[6]
$k$ $k$ -safety hyperproperties:
- $k=1$ $k=1$ (lifts of safety properties):
  - false, defined to be the set containing the empty set. Formally, $\mathbf {false} \triangleq \{\emptyset \}$ . This hyperproperty is not satisfied by any system.[7]
  - true, defined to be the set of all traces. Formally, $\mathbf {true} \triangleq \Phi$ . This hyperproperty is satisfied by all systems.[8]
  - Access control[9]
- $k=2$ $k=2$ :
  - Monotonicity[10]
  - Injectivity[10]
  - Symmetry, anti-symmetry, and asymmetry[10]
  - Observational determinism[11]
  - Noninterference
- $k=3$ $k=3$
  - Transitivity[10]
- $k=4$ $k=4$
  - Associativity[10]

Properties

Since hyperproperties are exactly the elements of the power set $\mathbb {P} (\mathbb {P} (\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.[12]

Applications

Several program logics[10][13] (most notably, HyperLTL[14]) and model checking algorithms[15][16] have been developed for checking that a system conforms to a hyperproperty.

References

Notes

Clarkson & Schneider, p. 23: "A labeled transition system [...] can be encoded as a set of traces.".
Clarkson & Schneider, p. 25: "A state machine M [...] can be encoded as a set of traces.".
Alpern, Bowen; Schneider, Fred B. (1985-10-07). "Defining liveness". Information Processing Letters. 21 (4): 181–185. doi:10.1016/0020-0190(85)90056-0. ISSN 0020-0190.
Clarkson & Schneider, p. 21.
Finkbeiner, Bernd; Haas, Lennart; Torfah, Hazem (June 2019). "Canonical Representations of k-Safety Hyperproperties". 2019 IEEE 32nd Computer Security Foundations Symposium (CSF): 17–1714. doi:10.1109/CSF.2019.00009. ISBN 978-1-7281-1407-1. S2CID 201848133.
Clarkson & Schneider, p. 11: "Safety properties lift to safety hyperproperties".
Clarkson & Schneider, p. 15: "The hyperproperty false, defined as \{\emptyset\}, is hypersafety but not hyperliveness"..
Clarkson & Schneider, p. 44.
Clarkson & Schneider.
Sousa & Dillig.
Clarkson & Schneider, p. 13: "observational determinism OD (2.6) cannot be expressed as a 2-safety property, but it is a 2-safety hyperproperty".
Clarkson & Schneider, p. 19.
Dardinier, Thibault; Müller, Peter (2023-01-24). "Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)". arXiv:2301.10037 [cs.LO].
Clarkson, Michael R.; Finkbeiner, Bernd; Koleini, Masoud; Micinski, Kristopher K.; Rabe, Markus N.; Sánchez, César (2014). Abadi, Martín; Kremer, Steve (eds.). "Temporal Logics for Hyperproperties". Principles of Security and Trust. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. 8414: 265–284. doi:10.1007/978-3-642-54792-8_15. ISBN 978-3-642-54792-8. S2CID 8938993.
Finkbeiner, Bernd; Rabe, Markus N.; Sánchez, César (2015). Kroening, Daniel; Păsăreanu, Corina S. (eds.). "Algorithms for Model Checking HyperLTL and HyperCTL$^*$". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing. 9206: 30–48. doi:10.1007/978-3-319-21690-4_3. ISBN 978-3-319-21690-4.
Hsu, Tzu-Han; Sánchez, César; Bonakdarpour, Borzoo (2021). Groote, Jan Friso; Larsen, Kim Guldstrand (eds.). "Bounded Model Checking for Hyperproperties". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing. 12651: 94–112. doi:10.1007/978-3-030-72016-2_6. ISBN 978-3-030-72016-2. PMC 7979203.

Sources

Clarkson, Michael R.; Schneider, Fred B. (2010-09-20). Sabelfeld, Andrei (ed.). "Hyperproperties". Journal of Computer Security. 18 (6): 1157–1210. doi:10.3233/JCS-2009-0393. S2CID 218604768.
Sousa, Marcelo; Dillig, Isil (2016-06-02). "Cartesian hoare logic for verifying k-safety properties". Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '16. New York, NY, USA: Association for Computing Machinery: 57–69. doi:10.1145/2908080.2908092. ISBN 978-1-4503-4261-2. S2CID 17433405.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[FOOTNOTEClarksonSchneiderp._23:_"A_labeled_transition_system_[...]_can_be_encoded_as_a_set_of_traces."-1] Clarkson & Schneider, p. 23: "A labeled transition system [...] can be encoded as a set of traces.".

[FOOTNOTEClarksonSchneiderp._25:_"A_state_machine_M_[...]_can_be_encoded_as_a_set_of_traces."-2] Clarkson & Schneider, p. 25: "A state machine M [...] can be encoded as a set of traces.".

[3] Alpern, Bowen; Schneider, Fred B. (1985-10-07). "Defining liveness". Information Processing Letters. 21 (4): 181–185. doi:10.1016/0020-0190(85)90056-0. ISSN 0020-0190.

[FOOTNOTEClarksonSchneider21-4] Clarkson & Schneider, p. 21.

[5] Finkbeiner, Bernd; Haas, Lennart; Torfah, Hazem (June 2019). "Canonical Representations of k-Safety Hyperproperties". 2019 IEEE 32nd Computer Security Foundations Symposium (CSF): 17–1714. doi:10.1109/CSF.2019.00009. ISBN 978-1-7281-1407-1. S2CID 201848133.

[FOOTNOTEClarksonSchneiderp._11:_"Safety_properties_lift_to_safety_hyperproperties"-6] Clarkson & Schneider, p. 11: "Safety properties lift to safety hyperproperties".

[FOOTNOTEClarksonSchneiderp._15:_"The_hyperproperty_false,_defined_as_\{\emptyset\},_is_hypersafety_but_not_hyperliveness".-7] Clarkson & Schneider, p. 15: "The hyperproperty false, defined as \{\emptyset\}, is hypersafety but not hyperliveness"..

[FOOTNOTEClarksonSchneider44-8] Clarkson & Schneider, p. 44.

[FOOTNOTEClarksonSchneider-9] Clarkson & Schneider.

[FOOTNOTESousaDillig-10] Sousa & Dillig.

[FOOTNOTEClarksonSchneiderp._13:_"observational_determinism_OD_(2.6)_cannot_be_expressed_as_a_2-safety_property,_but_it_is_a_2-safety_hyperproperty"-11] Clarkson & Schneider, p. 13: "observational determinism OD (2.6) cannot be expressed as a 2-safety property, but it is a 2-safety hyperproperty".

[FOOTNOTEClarksonSchneider19-12] Clarkson & Schneider, p. 19.

[13] Dardinier, Thibault; Müller, Peter (2023-01-24). "Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)". arXiv:2301.10037 [cs.LO].

[14] Clarkson, Michael R.; Finkbeiner, Bernd; Koleini, Masoud; Micinski, Kristopher K.; Rabe, Markus N.; Sánchez, César (2014). Abadi, Martín; Kremer, Steve (eds.). "Temporal Logics for Hyperproperties". Principles of Security and Trust. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. 8414: 265–284. doi:10.1007/978-3-642-54792-8_15. ISBN 978-3-642-54792-8. S2CID 8938993.

[15] Finkbeiner, Bernd; Rabe, Markus N.; Sánchez, César (2015). Kroening, Daniel; Păsăreanu, Corina S. (eds.). "Algorithms for Model Checking HyperLTL and HyperCTL$^*$". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing. 9206: 30–48. doi:10.1007/978-3-319-21690-4_3. ISBN 978-3-319-21690-4.

[16] Hsu, Tzu-Han; Sánchez, César; Bonakdarpour, Borzoo (2021). Groote, Jan Friso; Larsen, Kim Guldstrand (eds.). "Bounded Model Checking for Hyperproperties". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing. 12651: 94–112. doi:10.1007/978-3-030-72016-2_6. ISBN 978-3-030-72016-2. PMC 7979203.