Secure Information Flow as a Safety Problem

By Tachio Terauchi, A. Aiken. Sensors Applications Symposium, 2005

300 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Information Systems, Signal Processing

View Paper: https://www.semanticscholar.org/paper/7c555dfba844337d9ed1d56c231d99448069d83e

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 Information Systems

In Signal Processing

Citations in the corpus

Proving differential privacy with shadow execution (2019, background): “, x + x̂†), as is standard in self-composition [4, 38].”
Temporal Logics for Hyperproperties (2013, methodology): “This is essentially the self-composition construction, as used in previous work [8, 16, 66].”
Synthesizing coupling proofs of differential privacy (2017, background): “, in translation-validation [37, 38], security problems [18, 43], and Java code [41].”
Probabilistic relational reasoning for differential privacy (2012, background): “In contrast, privacy is a 2-safety property [11, 33], that is, a (universally quantified) property about two runs of a program.”
Proving Differential Privacy in Hoare Logic (2014, background): “Such approaches include self-composition [7], product programs [38], and type-directed product programs [35].”
A Formal Foundation for Secure Remote Execution of Enclaves (2017, methodology): “However, the properties we consider are 2-safety properties [67] that are variants of observational determinism [45, 55].”
Noninterference via Symbolic Execution (2012, methodology): “Then the variables are made symbolic and a type-directed transformation adopted from the work of Terauchi and Aiken [20] is applied to the program.”
An empirical study of privacy-violating information flows in JavaScript web applications (2010, methodology): “These include type systems [31, 23], model checking [28], Hoarelogics [1], and dataflow analyses [18, 26].”
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.”
Hyperproperties (2010, methodology): “For example, consider the hyperproperty 10This conclusion resolves the conjecture of Terauchi and Aiken that (termination-sensitive) secure information flow over infinite traces is “2- liveness [sic],” for some definition of 2-liveness.”
Declassification: Dimensions and principles (2009, unknown): “[7, 20, 73]).”