Research On Secure Boot Of Embedded Devices Based On Formal Methods

With the incoming Internet of Everything era,the security issues of various embedded devices have aroused wide attention in both academia and industry.To address these threats in the boot phrase of embedded devices,ARM,Intel,AMD,etc.have adopted their own hardware-assisted secure boot solutions.However,the existing schemes lack strict security assurances.This dissertation utilizes the automatic theorem proof system(Isabelle/HOL)to study the secure boot mechanism of embedded devices based on formal methods.This dissertation focuses on the secure boot technology of embedded devices with masterslave chips based on the ARMv8 architecture.Existing solutions to strengthen secure boot of devices are summarized,and the threats that exist in the boot phrase of master-slave chip devices are pointed out.A boot scheme of device security check mechanism based on formal verification is proposed and implemented,with completed formal verification and system comprehensive test.The main research work and contributions of this dissertation are summarized as follows:1.A DICE-based processor secure boot scheme for embedded devices with ARMv8 architecture is proposed.We analyze the existing security protection solutions of the master-slave chip in embedded devices,and point out the security threats that exists in the boot phrase.Then we propose a countermeasure which utilizes DICE to realize the security verification when the master-slave chip device boots.The chip identity private key which is generated from DICE is utilized to run the identity authentication protocol to realize the security verification of chip identity,ensuring the trust of the device's slave chip and laying the foundation for the establishment of chain of trust for the device.2.A formal model for security check mechanism is designed and implemented.We analyze the security assets of the system,establish the threat model during the device boots,and propose security objectives based on the threats.A formal model of the security check mechanism is established in Isabelle/HOL language.Model requirements are given,and the security check process of master-slave chip is described in the model instance.Then we complete the formal proof of the model instance through step-by-step derivation.The result shows that the security check mechanism described by our model can achieve the security objectives of the scheme,which lays a theoretical foundation for the realization of the device secure boot enhancement scheme.3.An enhanced scheme for processor secure boot based on master-slave chip check mechanism is proposed,with simulation implementation and test evaluation.Based on the security check mechanism that is formal verified,we design a two-stage secure boot enhanced scheme including pre-processing and normal boot,and conduct a comprehensive test and evaluation of the system,including functional tests,system tests,performance tests,and security tests.The result shows that the solution can ensure the trust of the identities of both the master and the slave chip,preventing further expansion of the attack surface.