Write a Blog >>
Tue 20 Jun 2017 10:50 - 11:15 at Aula Master - Static Analysis and Security Chair(s): Mayur Naik

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.

Conference Day
Tue 20 Jun

Displayed 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
25m
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
25m
Talk
Automatic Program Inversion using Symbolic Transducers
PLDI Research Papers
Qinheping HuUniversity of Wisconsin-Madison, Loris D'AntoniUniversity of Wisconsin–Madison
Media Attached
11:40
25m
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
25m
Talk
Rigorous Analysis of Software Countermeasures against Cache Attacks
PLDI Research Papers
Goran DoychevIMDEA Software Institute, Boris KöpfIMDEA Software Institute, Spain
Media Attached