FVCARE：弹性嵌入式 SoC 中安全原语的形式化验证
密码学与安全
2023-04-25 v1 硬件体系结构
摘要
随着利用率的提升，小型嵌入式与 IoT 设备已成为复杂攻击的有吸引力的目标，此类攻击可利用设备的安全关键信息与数据从事恶意活动。安全启动与远程证明（RA）技术在启动期与运行期验证设备软件状态的完整性。这些安全原句的正确实现与形式化验证提供了强安全保证并增强用户信心。这些安全原语的形式化验证被视为具挑战性，因其涉及复杂的软硬件交互、语义鸿沟并需要位精确推理。为应对这些挑战，本文提出 FVCARE 这一端到端系统协同验证框架。其亦定义了弹性小型嵌入式系统的安全属性。FVCARE 将端到端系统协同验证问题划分为两个模块：1）通过硬件验证技术验证（位精确的）初始系统设置、寄存器与访问控制策略；2）利用硬件的源码级软件抽象验证系统规范、安全属性与功能正确性。所提技术在基于 SRACARE 的系统上的评估证明了其在安全协同验证中的有效性。
引用
@article{arxiv.2304.11489,
title = {FVCARE:Formal Verification of Security Primitives in Resilient Embedded SoCs},
author = {Avani Dave and Nilanjan Banerjee and Chintan Patel},
journal= {arXiv preprint arXiv:2304.11489},
year = {2023}
}