Automatic Program Inversion using Symbolic Transducers
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 Times are displayed in 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:50 - 11:15 Talk | Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels PLDI Research Papers 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 | ||
11:15 - 11:40 Talk | Automatic Program Inversion using Symbolic Transducers PLDI Research Papers Media Attached | ||
11:40 - 12:05 Talk | Control-Flow Recovery from Partial Failure Reports PLDI Research Papers 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 | ||
12:05 - 12:30 Talk | Rigorous Analysis of Software Countermeasures against Cache Attacks PLDI Research Papers Media Attached |