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

最近的研究表明，在程序被翻译成机器代码后，检查它们的特性是多么重要。例如，许多安全漏洞依赖于在源代码级别不可见的平台特定特性，例如内存布局细节（例如，激活记录中变量的偏移量和结构字段之间的填充）。该项目的预期贡献包括(i)一个独立于语言的工具生成器，它根据给定指令集的语法和语义的正式规范，生成针对该指令集的动态分析、静态分析和符号评估组件的实现，以及（ii）各种原型语言特定应用程序（即特定的机器代码分析工具）。包括一种自动检测机器代码中的错误和安全漏洞的工具。其目的是确定确定的错误和漏洞，以及触发它们所需的信息。o检查机器代码序列属性的工具。o通过推断输入/输出和网络通信格式，以及通过总结组件客户端的行为来帮助检测组件之间的互操作性问题的工具。结果将帮助程序员创建正确、可靠和securesoftware系统通过为他们提供新的工具(a) verifyproperties程序的吗?(b)发现潜在的错误和安全漏洞。

Recent work has revealed how important it is to examine theproperties of programs after they have been translated to machinecode. For instance, many security exploits depend onplatform-specific features that are not visible at the source-codelevel, such as memory-layout details (e.g., the offsets of variablesin activation records and padding between fields of a structure). Theexpected contributions of the project include (i) alanguage-independent tool generator that, from a formal specificationof a given instruction set's syntax and semantics, generatesimplementations of dynamic-analysis, static-analysis, andsymbolic-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 securesoftware systems by providing them with new kinds of tools to (a) verifyproperties of a program?s behavior, and (b) find potential bugs andsecurity vulnerabilities.