TrABin：二进制代码的可信分析

微内核、设备驱动和加密例程的验证需要在二进制层面进行分析。为自动化这些分析，近年来已引入若干二进制分析平台。这些平台具有共同设计：采用硬件无关的中间表示、将体系结构相关代码翻译为该表示的机制，以及一组处理中间表示的体系结构无关分析。使用这些平台验证软件带来了对二进制代码到中间语言翻译（称为转译）的正确性和分析正确性的信任需求。实现高度信任具有挑战性，因为转译须处理（i）指令的所有副作用，（ii）多种指令编码（如ARM Thumb），以及（iii）可变指令长度（如Intel）。类似地，分析可使用复杂的变换（如循环展开）与简化（如部分求值）处理工件，其缺陷会危及结果正确性。我们通过在交互式定理证明器HOL4之上开发二进制分析平台克服这些问题。首先，我们形式化建模二进制中间语言并证明若干支撑工具（即类型检查器）的正确性。然后，我们实现两个证明生成型转译器，分别将ARMv8和CortexM0程序翻译为中间语言并生成证书。该证书是证明翻译正确性的HOL4证明。作为演示性分析，我们实现了一个证明生成型最弱前置条件生成器，可用于验证给定无循环程序片段满足某契约。最后，我们使用一个AES加密实现来对我们的平台进行基准测试。