Decomposition instead of self-composition for proving the absence of timing channels
Abstract
We present a novel approach to proving the absence of timing channels. The idea is to partition the program's execution traces in such a way that each partition component is checked for timing attack resilience by a time complexity analysis and that per-component resilience implies the resilience of the whole program. We construct a partition by splitting the program traces at secret-independent branches. This ensures that any pair of traces with the same public input has a component containing both traces. Crucially, the per-component checks can be normal safety properties expressed in terms of a single execution. Our approach is thus in contrast to prior approaches, such as self-composition, that aim to reason about multiple ( k ≥ 2) executions at once.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jun 14, 2017
- Source ID
- 10.1145/3140587.3062378
Entities
People
- Eric Koskinen
- Michael Hicks
- Paul Gazzillo
- Shiyi Wei
- Tachio Terauchi
- Timos Antonopoulos
Organizations
- Defense Advanced Research Projects Agency
- Japan Advanced Institute of Science and Technology
- Japan Society for the Promotion of Science
- Ministry of Education, Culture, Sports, Science and Technology
- National Science Foundation
- University of Maryland
- Yale University