Logo image
Back
A Comprehensive, Automated Security Analysis of the Uptane Automotive Over-the-Air Update Framework
Conference proceeding   Open access

A Comprehensive, Automated Security Analysis of the Uptane Automotive Over-the-Air Update Framework

Robert Lorch, Daniel Larraz, Cesare Tinelli and Omar Chowdhury
Proceedings of the 27th International Symposium on Research in Attacks, Intrusions and Defenses, pp.594-612
ACM Other Conferences
RAID '24: The 27th International Symposium on Research in Attacks, Intrusions and Defenses
09/30/2024
DOI: 10.1145/3678890.3678927
Appears in  UI Libraries Support Open Access
url
https://doi.org/10.1145/3678890.3678927View
Published (Version of record) Open Access

Abstract

We present our experience of formally verifying the desired security properties of the Uptane over-the-air (OTA) software update framework against a set of applicable threat models. Uptane is gaining traction in the automobile industry and is widely considered the next de-facto standard for OTA automobile software updates. The security of Uptane is of utmost importance because modern automobiles rely on software for their safety-critical functionalities and, especially, require OTA software updates to add new safety features or patch bugs in existing ones. Design flaws in Uptane can either violate the integrity of the updates to be installed or prevent vehicles from installing new updates, both of which can cause severe safety issues. Previous approaches to protocol verification either fail to capture the necessary features of Uptane or suffer from termination issues due to Uptane’s complexity. A key component of our approach lies in the eager combination of an infinite-state model checker and a cryptographic protocol verifier, where (in contrast to prior lazy approaches) we are able to eliminate a key manual step in the workflow while enabling reasoning over more fine-grained message structures. In addition, our approach utilizes two proven soundness- and completeness-preserving state-space-reduction optimizations for computational tractability, as well as a meta-level analysis technique that makes it feasible to reason over Uptane’s set of optional protocol features. Our approach is able to discover six new vulnerabilities while rediscovering all five known ones. While there have been previous analyses of Uptane’s security properties, they either missed design flaws identified by our approach or suffered from coverage and termination issues. The Uptane standards body has positively acknowledged our findings and has suggested updates to the protocol specification documents to address them.
 Security and privacy -- Formal methods and theory of security -- Logic and verification UIOWA OA Agreement

Details

Metrics

79 Record Views
2 Times Cited - Web of Science
Logo image