BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code
Recovering high-level type information in binaries is a key task in reverse engineering and binary analysis. Binaries contain very little explicit type information. The structure of binary code is incredibly flexible allowing for ad-hoc subtyping and polymorphism. Prior work has shown that precise type inference on binary code requires expressive subtyping and polymorphism. Implementations of these type system features in a binary type inference algorithm have thus-far been too inefficient to achieve widespread adoption. Recent advances in traditional type inference have achieved simple and efficient principal type inference in an ML like language with subtyping and polymorphism through the framework of algebraic subtyping. BinSub, a new binary type inference algorithm, recognizes the connection between algebraic subtyping and the type system features required to analyze binaries effectively. Using this connection, BinSub achieves simple, precise, and efficient binary type inference. We show that BinSub maintains a similar precision to prior work, while achieving a 63x improvement in average runtime for 1568 functions. We also present a formalization of BinSub and show that BinSub’s type system maintains the expressiveness of prior work.
Sun 20 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30 | Types, Control-flow and trace partitioningSAS at San Gabriel Chair(s): Michele Pasqua University of Verona | ||
11:00 30mFull-paper | BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code SAS Ian Smith Trail of Bits Pre-print | ||
11:30 30mFull-paper | Full Control-Flow Sensitivity for Definitional Interpreters SAS Kimball Germane Brigham Young University Pre-print | ||
12:00 30mFull-paper | Trace Partitioning as an Optimization Problem SAS Charles Babu M CEA-List, Matthieu Lemerre Université Paris-Saclay - CEA LIST, Sébastien Bardin CEA LIST, University Paris-Saclay, Jean-Yves Marion LORIA Pre-print |