...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >TrABin: Trustworthy analyses of binaries
【24h】

TrABin: Trustworthy analyses of binaries

机译：交易：二进制文件的可信赖分析

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: the adoption of hardware-independent intermediate representations, a mechanism to translate architecture dependent code to this representation, and a set of architecture independent analyses that process the intermediate representation.The usage of these platforms to verify software introduces the need for trusting both the correctness of the translation from binary code to intermediate language (called transpilation) and the correctness of the analyses. Achieving a high degree of trust is challenging since the transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encodings (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). Similarly, analyses can use complex transformations (e.g. loop unrolling) and simplifications (e.g. partial evaluation) of the artifacts, whose bugs can jeopardize correctness of the results.We overcome these problems by developing a binary analysis platform on top of the interactive theorem prover HOL4. First, we formally model a binary intermediate language and we prove correctness of several supporting tools (i.e. a type checker). Then, we implement two proof-producing transpilers, which respectively translate ARMv8 and CortexMO programs to the intermediate language and generate a certificate. This certificate is a HOL4 proofdemonstrating correctness of the translation. As demonstrating analysis, we implement a proof-producing weakest precondition generator, which can be used to verify that a given loop-free program fragment satisfies a contract. Finally, we use an AES encryption implementation to benchmark our platform. (C) 2019 Elsevier B.V. All rights reserved.
机译：验证微内核，设备驱动程序和加密例程需要在二进制级别进行分析。为了使这些分析自动化，近年来，已经引入了几种二进制分析平台。这些平台具有共同的设计：采用与硬件无关的中间表示形式，将依赖于体系结构的代码转换为该表示形式的机制，以及一组处理中间表示形式的与体系结构无关的分析。需要信任从二进制代码到中间语言的翻译的正确性（称为翻译）和分析的正确性。实现高度信任具有挑战性，因为编译必须处理（i）指令的所有副作用，（ii）多种指令编码（例如ARM Thumb）和（iii）可变指令长度（例如Intel）。同样，分析可以使用人工制品的复杂转换（例如，展开循环）和简化（例如，部分评估），其错误可能会损害结果的正确性。我们通过在交互式定理证明人HOL4之上开发一个二进制分析平台来克服这些问题。首先，我们对二进制中间语言进行正式建模，并证明了几种支持工具（即类型检查器）的正确性。然后，我们实现了两个产生证明的编译器，它们分别将ARMv8和CortexMO程序转换为中间语言并生成证书。该证书是HOL4证明翻译正确性的证明。作为演示分析，我们实现了产生证明的最弱前提条件生成器，该生成器可用于验证给定的无循环程序片段是否满足合同规定。最后，我们使用AES加密实现对我们的平台进行基准测试。 （C）2019 Elsevier B.V.保留所有权利。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号