Abstract:

Over the last decade, indistinguishability obfuscation (iO) has emerged as a seemingly omnipotent primitive with numerous applications to cryptography and beyond. Moreover, recent breakthrough work has demonstrated that iO can be realized from well-founded assumptions. A thorn to all this remarkable progress is a limitation of all known constructions of general-purpose iO: the security reduction  incurs a loss that is exponential in the input length} of the function. This ``input-length barrier'' to iO stems from the non-falsifiability of the iO definition and is  discussed in folklore as being possibly inherent. It has many negative consequences; notably, constructing iO for programs with inputs of unbounded length remains elusive due to this barrier. 

We present a new framework aimed towards overcoming the input-length barrier. Our approach relies on short mathematical proofs of functional equivalence of circuits (and Turing machines) to avoid the brute-force ``input-by-input'' check employed in prior works.

 - We show how to obfuscate circuits that have efficient proofs of equivalence in  Propositional Logic with a security loss independent of input length. 
 - Next, we show how to obfuscate Turing machines with unbounded length inputs, whose functional equivalence can be proven in Cook's Theory PV.
 - Finally, we demonstrate applications of our results to succinct non-interactive arguments and witness encryption, and provide guidance on using our techniques for building new applications.

To realize our approach, we depart from prior work and develop a new gate-by-gate obfuscation template that preserves the topology of the input circuit.