Hyperproperties

By Michael R. Clarkson, Fred B. Schneider. IEEE Computer Security Foundations Symposium, 2010

681 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Sociology and Political Science

View Paper: https://www.semanticscholar.org/paper/15ea0a6ac7b5849e8fc06057bd45ce08fe20985d

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Sociology and Political Science

Citations in the corpus

A design and verification methodology for secure isolated regions (2016, background): “Confidentiality is typically defined as a hyper-property [12], where we require that the adversary cannot infer secret state based on observations.”
A Roadmap Toward the Resilient Internet of Things for Cyber-Physical Systems (2018, background): “Although reasoning about a single trace can provide an insight about safety properties, this is generally not sufficient to capture important information-flow security properties [119] such as noninterference, non-inference and infor-”
A Formal Foundation for Secure Remote Execution of Enclaves (2017, background): “Non-Interference and Hyperproperties: The security properties of secure measurement, integrity, and confidentiality are formulated as 2-safety observational determinism properties [45, 55], which is a restricted class of hyperproperties [17].”
Probabilistic relational reasoning for differential privacy (2012, methodology): “In contrast, privacy is a 2-safety property [11, 33], that is, a (universally quantified) property about two runs of a program.”
Probabilistic Relational Reasoning for Differential Privacy (2013, methodology): “In contrast, privacy is a 2-safety property [Terauchi and Aiken 2005; Clarkson and Schneider 2010], that is, a (universally quantified) property about two runs of a program.”
Proving Differential Privacy in Hoare Logic (2014, methodology): “These hyperproperties [17] encompass many standard security analyses, and lie outside the scope of standard veriﬁcation tools—to date, there is no generally applicable method or tool for verifying hyperproperties.”
Moat: Verifying Confidentiality of Enclave Programs (2015, background): “Then, Validity of this theorem implies that we can replace G with H while proving any safety property or k-safety hyperprop-erty of enclave behaviour [16].”
Verified Computational Differential Privacy with Applications to Smart Metering (2013, background): “Moreover, we show how various notions of differential privacy can be cast in a programming language setting as program equivalences, which can in turn be captured as judgments in a relational Hoare logic.”
Computer-Aided Verification for Mechanism Design (2015, methodology): “Finally, RSM runs the well-known Vickrey-Clarke-Groves mechanism [26, 9, 15] to match each replica with a surrogate in this market.”
Temporal Logics for Hyperproperties (2013, methodology): “] ory of hyperproperties [16] generalizes the theory of trace properties to security policies, showing that certain classes of security policies are amenable to verification with invariance arguments [2] and with stepwise refinement [74].”
Computer Aided Verification (2017, neutral): “The properties we wish to establish, i.e. bounds on minimal and maximal ages, are actually hyperproperties [6]: they are not properties of individual reachable states but rather of the entire set of reachable states.”