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 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 Naik Georgia Tech 10:5025mTalk Decomposition Instead of Self-Composition for Proving the Absence of Timing ChannelsPLDI Research PapersTimos Antonopoulos Yale University, Paul Gazzillo Yale University, Michael Hicks University of Maryland, College Park, Eric Koskinen Yale University, Tachio Terauchi JAIST, Shiyi Wei University of Maryland, College Park Media Attached 11:1525mTalk Automatic Program Inversion using Symbolic TransducersPLDI Research PapersQinheping Hu University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin–Madison Media Attached 11:4025mTalk Control-Flow Recovery from Partial Failure ReportsPLDI Research PapersPeter Ohmann University of Wisconsin - Madison, Alexander L. Brooks University of Wisconsin, Madison, Loris D'Antoni University of Wisconsin–Madison, Ben Liblit University of Wisconsin–Madison Pre-print Media Attached 12:0525mTalk Rigorous Analysis of Software Countermeasures against Cache AttacksPLDI Research PapersGoran Doychev IMDEA Software Institute, Boris Köpf IMDEA Software Institute, Spain Media Attached