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 DayTue 20 JunDisplayed 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:5025mTalk Decomposition Instead of Self-Composition for Proving the Absence of Timing ChannelsPLDI Research PapersTimos 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:1525mTalk Automatic Program Inversion using Symbolic TransducersPLDI Research PapersQinheping HuUniversity of Wisconsin-Madison, Loris D'AntoniUniversity of Wisconsin–Madison Media Attached 11:4025mTalk Control-Flow Recovery from Partial Failure ReportsPLDI Research PapersPeter 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:0525mTalk Rigorous Analysis of Software Countermeasures against Cache AttacksPLDI Research PapersGoran DoychevIMDEA Software Institute, Boris KöpfIMDEA Software Institute, Spain Media Attached