Scalable Methods for Exhaustive Security Verification in Embedded Systems

Beschreibung

Embedded systems are ubiquitous and have become an integral part of modern technology. Until recently, security considerations were primarily confined to the software running on these systems. However, new security research has demonstrated attacks on the hardware of embedded systems, raising fundamental questions about their trustworthiness. To break this cycle of new attacks and patches, we need new methods that can detect entire classes of security problems in hardware. This thesis focuses on developing such methods. We develop verification methods following a structured strategy. First, we create a precise threat model of a security problem in embedded systems, which we formalize using mathematical notation. Based on this formalized threat model, we derive security properties in a standard property language which can be verified using commercial property checkers. The property checks constitute exhaustive proofs w.r.t. the analyzed threat models. Accordingly, our verification methods detect all targeted security problems and can prove their absence in a secure design. We verify the properties on hardware models at the Register Transfer Level (RTL) because these models capture all information relevant to our security analysis. RTL models also have a well-defined relationship to subsequent design steps, ensuring that the verification results are valid in the finished product. Finally, we integrate the derived properties into iterative verification flows. We target security problems that include functional bugs causing security violations, timing side channels, dangerous cross-modular effects, and problematic interactions between hardware and firmware in embedded processors and SoCs. We use symbolic formulations of hardware behavior and communication bottlenecks in hardware models to achieve scalable proofs. We evaluated all proposed verification methods in multiple case studies and detected multiple bugs and vulnerabilities in the analyzed designs.

Autor*in

Johannes Müller

Themen in »Scalable Methods for Exhaustive Security Verification in Embedded Systems«

Formal Verification Hardware Security Embedded Systems

Stimmen zu »Scalable Methods for Exhaustive Security Verification in Embedded Systems«

Details

Link teilen