No Cover Image

Journal article 769 views 156 downloads

A formal framework for security testing of automotive over-the-air update systems

Rhys Kirk Orcid Logo, Hoang Nguyen Orcid Logo, Jeremy Bryans, Siraj Shaikh Orcid Logo, Charles Wartnaby

Journal of Logical and Algebraic Methods in Programming, Volume: 130, Start page: 100812

Swansea University Authors: Hoang Nguyen Orcid Logo, Siraj Shaikh Orcid Logo

  • 61305_VoR.pdf

    PDF | Version of Record

    © 2022 The Authors. This is an open access article under the CC- BY license

    Download (579.38KB)

Abstract

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...

Full description

Published in: Journal of Logical and Algebraic Methods in Programming
ISSN: 2352-2208
Published: Elsevier BV 2023
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa61305
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: 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.
Keywords: Automotive cybersecurity; Security testing; Automotive OTA; Uptane; CSP
College: Faculty of Science and Engineering
Start Page: 100812