NDLI: Polymorphic type inference for machine code

Please wait, while we are loading the content...

Into the depths of C: elaborating the de facto standards

Data-driven precondition inference with learned features

Coverage-directed differential testing of JVM implementations

Effective padding of multidimensional arrays to avoid cache conflict misses

Configuration synthesis for programmable analog devices with Arco

On the complexity and performance of parsing with derivatives

Stratified synthesis: automatically learning the x86-64 instruction set

Accepting blame for safe tunneled exceptions

MapReduce program synthesis

Event-driven network programming

Rehearsal: a configuration verification tool for puppet

Just-in-time static type checking for dynamic languages

Synthesizing transformations on hierarchically structured data

Higher-order and tuple-based massively-parallel prefix sums

Idle time garbage collection scheduling

Cardinalities and universal quantifiers for verifying parameterized systems

Precise, dynamic information flow for database-backed applications

Transactional data structure libraries

Living on the edge: rapid-toggling probes with cross-modification on x86

Cartesian hoare logic for verifying k-safety properties

Exposing errors related to weak memory in GPU applications

GreenWeb: language extensions for energy-efficient mobile web computing

From Datalog to flix: a declarative language for fixed points on lattices

Remix: online detection and repair of cache contention for the JVM

Occurrence typing modulo theories

Programmatic and direct manipulation, together at last

Temporal NetKAT

Toward compositional verification of interruptible OS kernels and device drivers

Types from data: making structured data first-class citizens in F#

Program synthesis from polymorphic refinement types

A distributed OpenCL framework using redundant computation and data replication

Assessing the limits of program-specific garbage collection performance

Ivy: safety verification by interactive generalization

End-to-end verification of information-flow security for C and assembly programs

FlexVec: auto-vectorization for irregular loops

Polymorphic type inference for machine code

Verifying bit-manipulations of floating-point

Lightweight computation tree tracing for lazy functional languages

Input responsiveness: using canary inputs to dynamically steer approximation

Latte: a language, compiler, and runtime for elegant and efficient deep neural networks

Statistical similarity of binaries

Refinement types for TypeScript

Fast synthesis of fast collections

SDNRacer: concurrency analysis for software-defined networks

Verified peephole optimizations for CompCert

Automatically learning shape specifications

A design and verification methodology for secure isolated regions

Verified lifting of stencil computations

Polymorphic type inference for machine code

Content Provider	ACM Digital Library
Author	Noonan, Matt Loginov, Alexey Cok, David
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. .
Starting Page	27
Ending Page	41
Page Count	15
File Format	PDF
ISBN	9781450342612
DOI	10.1145/2908080.2908119
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2016-06-02
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Pushdown automata Static analyiss Reverse engineering Type systems Binary analysis Polymorphism
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in