Formally verified big step semantics out of x86-64 binaries
Formally verified big step semantics out of x86-64 binaries
复制标题
从 x86-64 二进制文件中正式验证大步语义
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
B. Ravindran
中科院分区：
文献类型：
--
作者：
Ian Roessle;Freek Verbeek;B. Ravindran
本文提出了一种生成反编译的x86-64机器代码和大步语义之间的形式证明等价定理的方法。这些证明是建立在两个额外的贡献之上的。首先，一个强大的和测试的正式x86-64机器模型包含1625指令的小步语义。第二，反编译成逻辑的方法，支持x86-64汇编和机器代码在大规模。这项工作实现了黑盒二进制验证，即，源代码不可用的二进制文件的形式验证。因此，它可以应用于由遗留组件组成的安全关键系统，或者由于专有原因而无法获得源代码的组件。该方法通过利用机器学习的语义来构建正式的机器模型，从而最大限度地减少可信代码库。我们应用的方法，几个案例研究，包括二进制文件，严重依赖于SSE 2浮点指令集，和二进制文件，通过编译代码，获得内联汇编成C代码。
This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x86-64 machine model containing small step semantics for 1625 instructions. Second, a decompilation-into-logic methodology supporting both x86-64 assembly and machine code at large scale. This work enables black-box binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safety-critical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machine-learned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floating-point instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code.
CakeML 的新的经过验证的编译器后端
DOI：
10.1145/2951913.2951924
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Tan Y
通讯作者：
Tan Y