SHCoT: Secure (and Verified) Hybrid Chain of Trust to Protect from Malicious Software in LightWeight Devices

Looking at the speed by which the software and the hardware evolve separately, there is no surprise that the interactions of the two may result in issues and appearance of back-doors to bypass the existing security. Lately, the hardware/software co-design gained lots of interest in both academia and industry, and proposed multiple hybrid solutions to enhance software/hardware interactions, security, and safety while guaranteeing good performance. In this paper, we focus on isolation and attestation to enforce the chain of trust in lightweight devices and detect malicious data and software locally and remotely. We present SHCoT, a hardware/software co-design to renew trust in devices. SHCoT is our first attempt to develop a formally verified hybrid solution to enhance existing solutions in the literature. While the work is still in progress, the first results show a partial verification of the security properties of SHCoT and small hardware/software cost.