Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels
We describe a novel technique for proving $k$-safety properties (non-interference, determinism, etc.) via a decomposition that enables one to leverage non-relational reasoning techniques. The key is the inter-operation of the following principles. First, we observe that many $k$-safety properties of interest have a particular structure that we call $\psi$\emph{-quotient partitionability} where $\psi$ is a $k$-ary formula. Second, we develop a partitioning strategy of execution traces based on the $k$-safety property $\Phi$ of interest such that if $\psi$ holds for $k$ traces then they must be in the same partition. Finally, within a partition component $T_i$, we observe that we can prove $k$-safety by instead proving a universal property: all traces within the partition satisfy some common property $P_i$, chosen to be strong enough that it implies the $k$-safety property $\Phi$ of any $k$-tuple of traces in components $T_i$.
We apply this strategy to the task of discovering timing side channels. A key feature of our approach is a demand-driven partitioning strategy that uses high/low-annotated regex-like \emph{trails} to reason about one partition component of execution traces at a time. We have applied our technique in a prototype implementation tool called {\sc Blazer}, based on WALA, PPL, Z3, and the brics automaton library. We have proved non-interference of (or synthesized an attack specification for) 25 programs written in Java bytecode, including 7 classic examples from the literature, and 6 examples extracted from the DARPA STAC challenge problems.
Tue 20 Jun Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:50 - 12:30: Static Analysis and SecurityPLDI Research Papers at Aula Master Chair(s): Mayur NaikGeorgia Tech | |||
10:50 - 11:15 Talk | Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels PLDI Research Papers Timos AntonopoulosYale University, Paul GazzilloYale University, Michael HicksUniversity of Maryland, College Park, Eric KoskinenYale University, Tachio TerauchiJAIST, Shiyi WeiUniversity of Maryland, College Park Media Attached | ||
11:15 - 11:40 Talk | Automatic Program Inversion using Symbolic Transducers PLDI Research Papers Media Attached | ||
11:40 - 12:05 Talk | Control-Flow Recovery from Partial Failure Reports PLDI Research Papers Peter OhmannUniversity of Wisconsin - Madison, Alexander L. BrooksUniversity of Wisconsin, Madison, Loris D'AntoniUniversity of Wisconsin–Madison, Ben LiblitUniversity of Wisconsin–Madison Pre-print Media Attached | ||
12:05 - 12:30 Talk | Rigorous Analysis of Software Countermeasures against Cache Attacks PLDI Research Papers Media Attached |