Advancing remote attestation via computer-aided formal verification of designs and synthesis of executables: opinion
Advancing remote attestation via computer-aided formal verification of designs and synthesis of executables: opinion
复制标题
通过计算机辅助形式验证设计和可执行文件的综合来推进远程认证：意见
DOI：
10.1145/3317549.3323403
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Tsudik, Gene
中科院分区：
文献类型：
--
作者：
Eldefrawy, Karim;Tsudik, Gene
嵌入式/智能/物联网设备的远程证明（RA）是当今安全领域的一个非常重要的问题。RA使验证者能够测量不受信任的远程设备（prover）的当前内存状态。RA帮助验证者在prover中建立静态或动态的信任根。尽管之前做了很多工作，但不幸的是，最先进的RA技术仍然缺乏任何坚实的基础，并且没有提供铁一般的安全性，安全性或鲁棒性保证。本文认为，计算机辅助形式验证，和合成的可执行文件，RA协议和混合（软件-硬件）架构是必需的，目前尚未解决。我们相信，这是可以实现的，目前（计算机辅助）的正式方法框架和工具，这可以帮助推进和成熟RA研究，如果用来建立更严格和明确的安全参数。为了支持我们的观点，我们强调了几个例子，在设计和安全分析ofRA技术的细微问题被错过了。尽管这种协议具有欺骗性的简单性，但手动分析和特别实现通常会导致底层处理器和系统架构中的重要细节的过度简化（以及随后的掩盖）。计算机辅助的形式验证迫使对这些细节进行更严格和更有纪律的考虑，否则，验证就会失败。我们提出的研究方向的主要目标是增加对当前和未来RA技术及其实现的正确性和安全性保证的信心。
Remote Attestation (RA) of embedded/smart/IoT devices is a very important issue on today's security landscape.RA enables a verifier to measures the current internal memory state of an untrusted remote device (prover).RA helps the verifier establish a static or dynamic root of trust in prover. Despite much prior work, state-of-the-artRA techniques unfortunately still lack any solid foundation and offer no ironclad security, safety or robustness guarantees. This paper argues thatcomputer-aided formal verification, and synthesis of executables, ofRA protocols and hybrid (software-hardware) architectures is required and currently unaddressed. We believe that this is achievable with current (computer-aided) formal methods frameworks and tools, and that this can help advance and matureRA research if used to establish more rigorous and clear security arguments. To support our opinion, we highlight several examples where subtle issues were missed in the design and security analysis ofRA techniques. Despite deceptive simplicity of such protocols, manual analyses and ad hoc implementations often lead to over-simplification of (and subsequent glossing over) important details in the underlying processor and system architectures. Computer-aided formal verification forces a more scrupulous and disciplined consideration of such details, since, otherwise, verification simply fails. The key objective of the research direction we propose is to increase confidence in correctness and security guarantees of current and futureRA techniques and their implementations.
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
用于安全功能评估的快速且经过验证的软件堆栈
DOI：
10.1145/3133956.3134017
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Almeida J
通讯作者：
Almeida J