Hi everyone,
Tomorrow noon at 4310 John will give a talk about Decomposition Instead of Self-Composition fo k-Safety.
Abstract:
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.
Best,
Qinheping Hu
![[Computer Systems Lab]](http://www.cs.wisc.edu/pics/csl_logo.gif){kind=logo}