Transforming out timing leaks

By Johan Agat. ACM-SIGACT Symposium on Principles of Programming Languages, 2000

356 citations recorded by the source corpus.

One aspect of security in mobile code is privacy: private (or secret) data should not be leaked to unauthorised agents. Most of the work on secure information flow has until recently only been concerned with detecting direct and indirect flows. Secret information can however be leaked to the attacker also through covert channels. It is very reasonable to assume that the attacker, even as an external observer, can monitor the timing (including termination) behaviour of the program. Thus to claim a program secure, the security analysis must take also these into account. In this work we present a surprisingly simple solution to the problem of detecting timing leakages to external observers. Our system consists of a type system in which well-typed programs do not leak secret information directly, indirectly or through timing, and a transformation for removing timing leakages. For any program that is well typed according to Volpano and Smith [VS97a], our transformation generates a program that is also free of timing leaks.

Subfields: Artificial Intelligence, Computer Networks and Communications, Signal Processing

View Paper: https://www.semanticscholar.org/paper/dcc291e4b7ab1f1553114a7d4de068b08d4ee394

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 Computer Networks and Communications

In Signal Processing

Citations in the corpus

Language-based information-flow security (2003, methodology): “Agat’s approach [10] to closing timing leaks is based on another example of a well-studied technique in programming languages,program transformation .”
Observational determinism for concurrent program security (2003, methodology): “They use a novel probabilistic bisimulation approach to specify noninterference properties, and have used the techniques to prove correct Agat’s program transformation for eliminating timing channels [3].”
AEGIS: architecture for tamper-evident and tamper-resistant processing (2003, background): “Once the data arrives, the decryption of four chunks (B[1], B[2], B[3] and B[4])”
Differential Privacy Under Fire (2011, background): “Language-based designs can eliminate them for certain types of programs [1], but only at the expense of severely limiting the expressiveness of the programming language.”
Aegis: A Single-Chip Secure Processor (2007, methodology): “For more general programs, Agat proposed program transformations that ensure all execution paths depending on sensitive data carry out the same number of operations [1].”
Distributed Differential Privacy and Applications (2015, background): “Language-based designs can eliminate them for certain types of programs (Agat, 2000), but only at the expense of severely limiting the expressiveness of the programming language.”
CacheAudit: A Tool for the Static Analysis of Cache Side Channels (2013, methodology): “Finally, our work goes beyond language-based approaches that consider caching [7, 25] in that we rely on more realistic models of caches and aim for more permissive, quantitative guarantees.”
ObliVM: A Programming Framework for Secure Computation (2015, background): “In SCVM [15], a histogram program is as below. for (public int i=0; i<n; ++i) c[i] = 0; for (public int i=0; i<m; ++i) c[a[i]] ++; This program counts the frequency of each values in [0..n − 1] in the array a of size m.”