With the increased utilization, the small embedded and IoT devices have become an attractive target for sophisticated attacks that can exploit the devices security critical information and data in malevolent activities. Secure boot and Remote Attestation (RA) techniques verifies the integrity of the devices software state at boot-time and runtime. Correct implementation and formal verification of these security primitives provide strong security guarantees and enhance user confidence. The formal verification of these security primitives is considered challenging, as it involves complex hardware software interactions, semantics gaps and requires bit-precise reasoning. To address these challenges, this paper presents FVCARE an end to end system co-verification framework. It also defines the security properties for resilient small embedded systems. FVCARE divides the end to end system co verification problem into two modules: 1) verifying the (bit precise) initial system settings, registers, and access control policies by hardware verification techniques, and 2) verifying the system specification, security properties, and functional correctness using source-level software abstraction of the hardware. The evaluation of proposed techniques on SRACARE based systems demonstrates its efficacy in security co verification.

翻译：随着嵌入式及物联网设备的广泛应用，这些小型设备已成为复杂攻击的诱人目标，攻击者可利用设备安全关键信息与数据进行恶意活动。安全启动与远程证明（RA）技术可在启动时和运行时验证设备软件状态的完整性。这些安全原语的正确实现与形式化验证能提供强有力的安全保障，并增强用户信心。由于涉及复杂的软硬件交互、语义鸿沟及需进行比特精确推理，这些安全原语的形式化验证具有挑战性。为应对这些挑战，本文提出FVCARE——一种端到端系统协同验证框架，同时定义了弹性小型嵌入式系统的安全属性。FVCARE将端到端系统协同验证问题分解为两个模块：1）通过硬件验证技术验证（比特精确的）初始系统设置、寄存器及访问控制策略；2）利用硬件源码级软件抽象验证系统规范、安全属性及功能正确性。在基于SRACARE的系统上对提出技术的评估表明，其在安全协同验证中具有有效性。