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

We propose a fully-automated technique for inverting functional programs that operate over lists such as string encoders and decoders. We consider programs that can be modeled using symbolic extended finite transducers (\SEFTs), an expressive model that can describe complex list-manipulating programs while retaining several decidable properties. Concretely, given a program $P$ expressed as an \SEFT, we propose techniques for: 1) checking whether $P$ is injective and, if that is the case, 2) building an \SEFT $P^{-1}$ describing its inverse. We first show that it is undecidable to check whether an \SEFT is injective and propose an algorithm for checking injectivity for a restricted, but a practical class of \SEFTs. We then propose an algorithm for inverting \SEFTs based on the following idea: if an \SEFT is injective, inverting it amounts to inverting all its individual transitions. We leverage recent advances program synthesis and show that the transition inversion problem can be expressed as an instance of the syntax-guided synthesis framework. Finally, we implement the proposed techniques in a tool called \genic and show that \genic can invert 13 out 14 real complex string encoders and decoders, producing inverse programs that are substantially identical to manually written ones.

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 Naik Georgia Tech
10:50
25m
Talk
Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels
PLDI Research Papers
Timos 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:15
25m
Talk
Automatic Program Inversion using Symbolic Transducers
PLDI Research Papers
Qinheping Hu University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin–Madison
Media Attached
11:40
25m
Talk
Control-Flow Recovery from Partial Failure Reports
PLDI Research Papers
Peter 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:05
25m
Talk
Rigorous Analysis of Software Countermeasures against Cache Attacks
PLDI Research Papers
Goran Doychev IMDEA Software Institute, Boris Köpf IMDEA Software Institute, Spain
Media Attached