SHF: Medium: MACANTOK -- a MAchine-Code-ANalysis TOol Kit -- and its Applications

University Of Wisconsin-Madison, Madison WI

Investigators

Abstract

Recent work has revealed how important it is to examine the properties of programs after they have been translated to machine code. For instance, many security exploits depend on platform-specific features that are not visible at the source-code level, such as memory-layout details (e.g., the offsets of variables in activation records and padding between fields of a structure). The expected contributions of the project include (i) a language-independent tool generator that, from a formal specification of a given instruction set's syntax and semantics, generates implementations of dynamic-analysis, static-analysis, and symbolic-evaluation components tailored to that instruction set, and (ii) a variety of prototype language-specific applications (i.e., specific machine-code-analysis tools), including o A tool to automate the detection of bugs and security vulnerabilities in machine code. The aim is to identify definite bugs and vulnerabilities, and information about what is required to trigger them. o A tool to check sequencing properties on machine code. o A tool that can aid in detecting interoperability problems among components by inferring input/output and network-communication formats, and by summarizing the behavior of a component's client. The results will help programmers create correct, reliable, and secure software systems by providing them with new kinds of tools to (a) verify properties of a program?s behavior, and (b) find potential bugs and security vulnerabilities.