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 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:50 - 12:30 | |||
10:50 25mTalk | 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 25mTalk | Automatic Program Inversion using Symbolic Transducers PLDI Research Papers Media Attached | ||
11:40 25mTalk | 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 25mTalk | Rigorous Analysis of Software Countermeasures against Cache Attacks PLDI Research Papers Media Attached |