Towards Formal Security Verification of Over-the-Air Update Protocol: Requirements, Survey and UpKit Case Study

Abstract

The fast growing number of connected devices through the Internet of Things requires the capability of performing secure and efficient over-the-air updates in order to manage the deployment of innovative features and to correct security issues. Pushing an updated image in a device requires a complex protocol exposed to security threats which could be exploited to block, spy or even take control of the updated device. Hence, such update protocols need to be carefully designed and verified. In the scope of this paper, we review some representative update protocols and related threats based on MQTT, TUF (Uptane) and the blockchain. We then show how the adequate management of those threats can be verified using a formal modelling and verification approach using the Tamarin tooling. Our work is applied to the concrete case of the UpKit protocol which exhibits an interesting design.