Proving Memory Access Violations in Isabelle/HOL
Proving Memory Access Violations in Isabelle/HOL
复制标题
证明 Isabelle/HOL 中的内存访问冲突
DOI：
10.1145/3563822.3568010
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Ahmadi S
中科院分区：
文献类型：
--
作者：
Ahmadi S
安全关键应用程序通常依赖于存储器隔离机制来确保关键数据的完整性（例如，键）和程序指令（例如，实现证明协议）。这些包括基于软件的安全微监控器（SµV）或基于硬件的安全微监控器（例如，TrustLite或SMART）。在这里，我们必须保证对应于程序的汇编级指令没有违反强加的内存访问限制。我们在两种实现远程证明协议的架构（SµV和TrustLite）上演示了我们的方法。我们扩展的方法的基础上的二进制分析平台（BAP）生成编译汇编为一个给定的C程序，这是翻译成一个汇编中间语言（BIL），并最终伊莎贝尔/HOL理论。在我们的扩展中，我们开发了一个对手模型，并定义了一致性谓词施加的架构。我们生成一组程序，涵盖所有可能的情况下，其中一个汇编级指令试图违反至少一个一致性谓词。这表明SµV和TrustLite的内存访问限制都是动态保持的。此外，我们引入一致性谓词的汇编级指令，可以改变控制流，提高TrustLite的内存保护单元。
Security-critical applications often rely on memory isolation mechanisms to ensure integrity of critical data (e.g., keys) and program instructions (e.g., implementing an attestation protocol). These include software-based security microvisor (SµV) or hardware-based (e.g., TrustLite or SMART). Here, we must guarantee that none of the assembly-level instructions corresponding to a program violate the imposed memory access restrictions. We demonstrate our approach on two architectures (SµV and TrustLite) on which remote attestation protocols are implemented. We extend an approach based on the Binary Analysis Platform (BAP) to generate compiled assembly for a given C program, which is translated to an assembly intermediate language (BIL) and ultimately to Isabelle/HOL theories. In our extension, we develop an adversary model and define conformance predicates imposed by an architecture. We generate a set of programs covering all possible cases in which an assembly-level instruction attempts to violate at least one of the conformance predicates. This shows that the memory access restriction of both SµV and TrustLite are dynamically maintained. Moreover, we introduce conformance predicates for assembly-level instructions that can change the control flow, which improve TrustLite’s memory protection unit.
登录
查看更多内容
用于远程认证的嵌入式系统的形式验证
DOI：
--
发表时间：
2015
期刊：
影响因子：
--
作者：
G. Cabodi;P. Camurati;C. Loiacono;G. Pipitone;F. Savarese;D. Vendraminetto
通讯作者：
D. Vendraminetto
验证 Isabelle/HOL 中的安全推测
DOI：
--
发表时间：
2021
期刊：
World Congress on Formal Methods
影响因子：
--
作者：
Mattison Griffin;Brijesh Dongol
通讯作者：
Brijesh Dongol
DOI：
10.1145/3098243.3098261
发表时间：
2017-03
期刊：
Proceedings of the 10th ACM Conference on Security and Privacy in Wireless and Mobile Networks
影响因子：
--
作者：
Karim M. El Defrawy;Norrathep Rattanavipanon;G. Tsudik
通讯作者：
Karim M. El Defrawy;Norrathep Rattanavipanon;G. Tsudik
用 C 语言对微控制器进行编程
DOI：
--
发表时间：
2016
期刊：
影响因子：
--
作者：
J. Schreiber
通讯作者：
J. Schreiber