Sound Transpilation from Binary to Machine-Independent Code
Sound Transpilation from Binary to Machine-Independent Code
复制标题
从二进制到机器无关代码的声音转换
DOI：
10.1007/978-3-319-70848-5_13
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
R. Guanciale
中科院分区：
文献类型：
--
作者：
Roberto Metere;Andreas Lindner;R. Guanciale
为了处理现代指令集体系结构的复杂性和异构性，分析平台共享一个共同的设计，采用与硬件无关的中间表示法。由于这些平台提供的高度自动化，使用这些平台来验证系统到二进制级别是很有吸引力的。然而，它引入了信任从二进制代码到中间语言的转换的正确性的需要。实现高度信任是具有挑战性的，因为这种转换必须处理(I)指令的所有副作用，(Ii)多指令编码(例如，ARM拇指)，以及(Iii)可变指令长度(例如，Intel)。我们通过在交互式定理证明器HOL4中对这样的中间语言之一进行形式化建模并通过实现证明生成转换器来克服这些问题。该工具将ARMv8程序翻译成中间语言，并以模拟定理的形式生成HOL4证明，以证明翻译的正确性。我们还展示了如何利用转置定理将在中间语言上验证的性质转移到二进制代码上。
In order to handle the complexity and heterogeneity of modern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representations. The usage of these platforms to verify systems down to binary-level is appealing due to the high degree of automation they provide. However, it introduces the need for trusting the correctness of the translation from binary code to intermediate language. Achieving a high degree of trust is challenging since this transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encoding (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). We overcome these problems by formally modeling one of such intermediate languages in the interactive theorem prover HOL4 and by implementing a proof-producing transpiler. This tool translates ARMv8 programs to the intermediate language and generates a HOL4 proof that demonstrates the correctness of the translation in the form of a simulation theorem. We also show how the transpiler theorems can be used to transfer properties verified on the intermediate language to the binary code.
DOI：
10.1145/1315245.1315313
发表时间：
2007-10
期刊：
--
影响因子：
--
作者：
H. Shacham
通讯作者：
H. Shacham