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.

Tue 20 Jun

pldi-2017-papers
10:50 - 12:30: PLDI Research Papers - Static Analysis and Security at Aula Master
Chair(s): Mayur NaikGeorgia Tech
pldi-2017-papers149794860000010:50 - 11:15
Talk
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
pldi-2017-papers149795010000011:15 - 11:40
Talk
Qinheping HuUniversity of Wisconsin-Madison, Loris D'AntoniUniversity of Wisconsin–Madison
Media Attached
pldi-2017-papers149795160000011:40 - 12:05
Talk
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
pldi-2017-papers149795310000012:05 - 12:30
Talk
Goran DoychevIMDEA Software Institute, Boris KöpfIMDEA Software Institute, Spain
Media Attached