Matt Noonan
Abstract
For many compiled languages, source-level types are erased very early in the compilation process. As a result, further compiler passes may convert type-safe source into type-unsafe machine code. Type-unsafe idioms in the original source and type-unsafe optimizations mean that type information in a stripped binary is essentially nonexistent. The problem of recovering high-level types by performing type inference over stripped machine code is called type reconstruction, and offers a useful capability in support of reverse engineering and decompilation. In this paper, we motivate and develop a novel type system and algorithm for machine-code type inference. The features of this type system were developed by surveying a wide collection of common source- and machine-code idioms, building a catalog of challenging cases for type reconstruction. We found that these idioms place a sophisticated set of requirements on the type system, inducing features such as recursively-constrained polymorphic types. Many of the features we identify are often seen only in expressive and powerful type systems used by high-level functional languages. Using these type-system features as a guideline, we have developed Retypd: a novel static type-inference algorithm for machine code that supports recursive types, polymorphism, and subtyping. Retypd yields more accurate inferred types than existing algorithms, while also enabling new capabilities such as reconstruction of pointer const annotations with 98% recall. Retypd can operate on weaker program representations than the current state of the art, removing the need for high-quality points-to information that may be impractical to compute.
- ISO/IEC TR 19768:2007: Technical report on C++ library extensions, 2007.Google Scholar
- O. Agesen. Constraint-based type inference and parametric polymorphism. In Static Analysis Symposium, pages 78–100, 1994.Google ScholarCross Ref
- R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, 1993. Google ScholarDigital Library
- L. O. Andersen. Program analysis and specialization for the C programming language. PhD thesis, University of Cophenhagen, 1994.Google Scholar
- G. Balakrishnan, R. Gruian, T. Reps, and T. Teitelbaum. CodeSurfer/x86 – a platform for analyzing x86 executables. In Compiler Construction, pages 250–254, 2005. Google ScholarDigital Library
- G. Balakrishnan and T. Reps. Analyzing Memory Accesses in x86 Executables, in Compiler Construction, pages 5–23, 2004.Google ScholarCross Ref
- A. Carayol and M. Hague. Saturation algorithms for modelchecking pushdown systems. In International Conference on Automata and Formal Languages, pages 1–24, 2014.Google Scholar
- D. Caucal. On the regular structure of prefix rewriting. Theoretical Computer Science, 106(1):61–86, 1992. Google ScholarDigital Library
- J. Eifrig, S. Smith, and V. Trifonov. Sound polymorphic type inference for objects. In Object-Oriented Programming, Systems, Languages, and Applications, pages 169–184, 1995. Google ScholarDigital Library
- K. ElWazeer, K. Anand, A. Kotha, M. Smithson, and R. Barua. Scalable variable and data type detection in a binary rewriter. In Programming Language Design and Implementation, pages 51–60, 2013. Google ScholarDigital Library
- J. S. Foster, R. Johnson, J. Kodumal, and A. Aiken. Flowinsensitive type qualifiers. ACM Transactions on Programming Languages and Systems, 28(6):1035–1087, 2006. Google ScholarDigital Library
- M. Fähndrich and A. Aiken. Making set-constraint program analyses scale. In Workshop on Set Constraints, 1996.Google Scholar
- D. Gopan, E. Driscoll, D. Nguyen, D. Naydich, A. Loginov, and D. Melski. Data-delineation in software binaries and its application to buffer-overrun discovery. In International Conference on Software Engineering, pages 145–155, 2015. Google ScholarDigital Library
- D. Greenfieldboyce and J. S. Foster. Type qualifier inference for Java. In Object-Oriented Programming, Systems, Languages, and Applications, pages 321–336, 2007. Google ScholarDigital Library
- Hex-Rays. Hex-Rays IdaPro. http://www.hex-rays.com/ products/ida/, 2015.Google Scholar
- D. Kozen, J. Palsberg, and M. I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5(01):113–125, 1995.Google ScholarCross Ref
- J. Lee, T. Avgerinos, and D. Brumley. TIE: Principled reverse engineering of types in binary programs. In Network and Distributed System Security Symposium, pages 251–268, 2011.Google Scholar
- J. Lim and T. Reps. TSL: A system for generating abstract interpreters and its application to machine-code analysis. ACM Transactions on Programming Languages and Systems, 35(1): 4, 2013. Google ScholarDigital Library
- Z. Lin, X. Zhang, and D. Xu. Automatic reverse engineering of data structures from binary execution. In Network and Distributed System Security Symposium, 2010.Google Scholar
- S. Marlow, A. R. Yakushev, and S. Peyton Jones. Faster laziness using dynamic pointer tagging. In International Conference on Functional Programming, pages 277–288, 2007. Google ScholarDigital Library
- L. Mauborgne and X. Rival. Trace partitioning in abstract interpretation based static analyzers. In Programming Languages and Systems, pages 5–20, 2005. Google ScholarDigital Library
- M. Noonan, A. Loginov, and D. Cok. Polymorphic type inference for machine code (extended version). URL http: //arxiv.org/abs/1603.05495. Google ScholarDigital Library
- J. Palsberg and P. O’Keefe. A type system equivalent to flow analysis. ACM Transactions on Programming Languages and Systems, 17(4):576–599, 1995. Google ScholarDigital Library
- J. Palsberg, M. Wand, and P. O’Keefe. Type inference with non-structural subtyping. Formal Aspects of Computing, 9(1): 49–67, 1997.Google ScholarCross Ref
- F. Pottier and D. Rémy. The essence of ML type inference. In B. C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10. MIT Press, 2005.Google Scholar
- J. Rehof and M. Fähndrich. Type-based flow analysis: From polymorphic subtyping to cfl-reachability. In Principles of Programming Languages, pages 54–66, 2001. Google ScholarDigital Library
- J. Richard Büchi. Regular canonical systems. Archive for Mathematical Logic, 6(3):91–111, 1964.Google ScholarCross Ref
- E. Robbins, J. M. Howe, and A. King. Theory propagation and rational-trees. In Principles and Practice of Declarative Programming, pages 193–204, 2013. Google ScholarDigital Library
- M. Robertson. A Brief History of InvSqrt. PhD thesis, University of New Brunswick, 2012.Google Scholar
- E. J. Schwartz, J. Lee, M. Woo, and D. Brumley. Native x86 decompilation using semantics-preserving structural analysis and iterative control-flow structuring. In USENIX Security Symposium, pages 353–368, 2013. Google ScholarDigital Library
- M. Siff, S. Chandra, T. Ball, K. Kunchithapadam, and T. Reps. Coping with type casts in C. In Software Engineering—ESEC/FSE’99, pages 180–198, 1999. Google ScholarDigital Library
- A. Slowinska, T. Stancescu, and H. Bos. Howard: A dynamic excavator for reverse engineering data structures. In Network and Distributed System Security Symposium, 2011.Google Scholar
- B. Steensgaard. Points-to analysis in almost linear time. In Principles of Programming Languages, pages 32–41, 1996. Google ScholarDigital Library
- Z. Su, A. Aiken, J. Niehren, T. Priesnitz, and R. Treinen. The first-order theory of subtyping constraints. In Principles of Programming Languages, pages 203–216, 2002. Google ScholarDigital Library
Index Terms
- Polymorphic type inference for machine code
Recommendations
Polymorphic type inference for machine code
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and ImplementationFor many compiled languages, source-level types are erased very early in the compilation process. As a result, further compiler passes may convert type-safe source into type-unsafe machine code. Type-unsafe idioms in the original source and type-unsafe ...
Type inference, principal typings, and let-polymorphism for first-class mixin modules
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingA mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Type inference, principal typings, and let-polymorphism for first-class mixin modules
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingA mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Comments