A Formal Framework for Security Testing of Automotive Over-The-Air Update Systems

Rhys Kirk, Hoang Nga Nguyen, Jeremy Bryans, Siraj Shaikh, Charlie Wartnaby

Research output: Contribution to journalArticlepeer-review


Modern vehicles are comparable to desktop computers due to the increase in connectivity. This fact also extends to potential cyber-attacks. A solution for preventing and mitigating cyber attacks is Over-The-Air (OTA) updates. This solution has also been used for both desktops and mobile phones. The current de facto OTA security system for vehicles is Uptane, which is developed to solve the unique issues vehicles face. The Uptane system needs to have a secure method of updating; otherwise, attackers will exploit it. To this end, we have developed a comprehensive and model-based security testing approach by translating Uptane and our attack model into formal models in Communicating Sequential Processes (CSP). These are combined and verified to generate an exhaustive list of test cases to see to which attacks Uptane may be susceptible. Security testing is then conducted based on these generated test cases, on a test-bed running an implementation of Uptane. The security testing result enables us to validate the security design of Uptane and some vulnerabilities to which it is subject.
Original languageEnglish
Number of pages28
JournalJournal of Logical and Algebraic Methods in Programming
Publication statusIn preparation - 2022


Dive into the research topics of 'A Formal Framework for Security Testing of Automotive Over-The-Air Update Systems'. Together they form a unique fingerprint.

Cite this