Formal Verification of Embedded Systems for Remote Attestation
Formal Verification of Embedded Systems for Remote Attestation
复制标题
用于远程认证的嵌入式系统的形式验证
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
D. Vendraminetto
中科院分区：
文献类型：
--
作者：
G. Cabodi;P. Camurati;C. Loiacono;G. Pipitone;F. Savarese;D. Vendraminetto
嵌入式系统越来越普遍，相互依赖，在许多情况下对我们的日常生活和安全至关重要。由于这些设备越来越容易受到攻击，因此需要新的保护机制来以低成本提供所需的弹性和依赖性。远程证明（RA）是一种安全检查远程嵌入式设备内部状态的软硬件机制。本方案由以下人员执行：（1）证明器，其在给定秘密密钥及其实际状态的情况下，通过证明算法生成结果;（2）验证器，其在给定密钥、预期证明器实际状态的情况下，通过验证算法接受或拒绝结果。由于协议的安全性取决于其最薄弱的环节，因此对其安全要求进行全面验证至关重要。在本文中，我们提出了一种方法，形式化验证RA架构的硬件安全需求。首先对三种RA体系结构进行了分析和比较，然后定义了RA系统的安全属性，并使用一个完整的形式化验证框架进行了验证
Embedded systems are increasingly pervasive, interdependent and in many cases critical to our every day life and safety. As such devices are more and more subject to attacks, new protection mechanisms are needed to provide the required resilience and dependency at low cost. Remote attestation (RA) is a software-hardware mechanism that securely checks the internal state of remote embedded devices. This protocol is executed by: (1) a prover that, given a secret key and its actual state, generates a result through an attestation algorithm; (2) a verifier that, given the key, the expected prover actual state, accepts or rejects the result through a verification algorithm. As the security of a protocol is only as good as its weakest link, a comprehensive validation of its security requirements is paramount. In this paper, we present a methodology for formal verification of hardware security requirements of RA architectures. First we perform an analysis and a comparison of three selected RA architectures, then we define security properties for RA systems and we verify them using a complete framework for formal verification