Downloads: 0 | Views: 26
Informative Article | Software Engineering | India | Volume 10 Issue 12, December 2021 | Rating: 4.1 / 10
FVCARE: Formal Verification of Security Primitives in Resilient Embedded SoCs
Avani Dave
Abstract: With the increased utilization, the small embedded and IoT devices have become an attractive target for sophisticated attacks that can exploit the device?s security-critical information and data in malevolent activities. Secure boot and Remote Attestation (RA) techniques verifies the integrity of the device?s 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.
Keywords: secure boot, formal verification, resilient system, onboard recovery, attack resilient system, small embedded systems
Edition: Volume 10 Issue 12, December 2021,
Pages: 1503 - 1512