No Cover Image

Journal article 565 views 110 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)

Check full text

DOI (Published version): 10.1016/j.jlamp.2022.100812

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!
first_indexed 2022-10-13T12:21:47Z
last_indexed 2023-01-13T19:21:59Z
id cronfa61305
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2022-10-13T13:24:53.4928792</datestamp><bib-version>v2</bib-version><id>61305</id><entry>2022-09-22</entry><title>A formal framework for security testing of automotive over-the-air update systems</title><swanseaauthors><author><sid>cb24d5c5080534dc5b5e3390f24dd422</sid><ORCID>0000-0003-0260-1697</ORCID><firstname>Hoang</firstname><surname>Nguyen</surname><name>Hoang Nguyen</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>50117e8faac2d0937989e14847105704</sid><ORCID>0000-0002-0726-3319</ORCID><firstname>Siraj</firstname><surname>Shaikh</surname><name>Siraj Shaikh</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2022-09-22</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Journal of Logical and Algebraic Methods in Programming</journal><volume>130</volume><journalNumber/><paginationStart>100812</paginationStart><paginationEnd/><publisher>Elsevier BV</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>2352-2208</issnPrint><issnElectronic/><keywords>Automotive cybersecurity; Security testing; Automotive OTA; Uptane; CSP</keywords><publishedDay>1</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-01-01</publishedDate><doi>10.1016/j.jlamp.2022.100812</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2022-10-13T13:24:53.4928792</lastEdited><Created>2022-09-22T15:48:25.3104305</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Rhys</firstname><surname>Kirk</surname><orcid>0000-0001-6808-8051</orcid><order>1</order></author><author><firstname>Hoang</firstname><surname>Nguyen</surname><orcid>0000-0003-0260-1697</orcid><order>2</order></author><author><firstname>Jeremy</firstname><surname>Bryans</surname><order>3</order></author><author><firstname>Siraj</firstname><surname>Shaikh</surname><orcid>0000-0002-0726-3319</orcid><order>4</order></author><author><firstname>Charles</firstname><surname>Wartnaby</surname><order>5</order></author></authors><documents><document><filename>61305__25446__1133dea405b34d468a2830d2b61ce9ba.pdf</filename><originalFilename>61305_VoR.pdf</originalFilename><uploaded>2022-10-13T13:23:04.4983870</uploaded><type>Output</type><contentLength>593286</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>&#xA9; 2022 The Authors. This is an open access article under the CC- BY license</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>http://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling 2022-10-13T13:24:53.4928792 v2 61305 2022-09-22 A formal framework for security testing of automotive over-the-air update systems cb24d5c5080534dc5b5e3390f24dd422 0000-0003-0260-1697 Hoang Nguyen Hoang Nguyen true false 50117e8faac2d0937989e14847105704 0000-0002-0726-3319 Siraj Shaikh Siraj Shaikh true false 2022-09-22 SCS 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. Journal Article Journal of Logical and Algebraic Methods in Programming 130 100812 Elsevier BV 2352-2208 Automotive cybersecurity; Security testing; Automotive OTA; Uptane; CSP 1 1 2023 2023-01-01 10.1016/j.jlamp.2022.100812 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2022-10-13T13:24:53.4928792 2022-09-22T15:48:25.3104305 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Rhys Kirk 0000-0001-6808-8051 1 Hoang Nguyen 0000-0003-0260-1697 2 Jeremy Bryans 3 Siraj Shaikh 0000-0002-0726-3319 4 Charles Wartnaby 5 61305__25446__1133dea405b34d468a2830d2b61ce9ba.pdf 61305_VoR.pdf 2022-10-13T13:23:04.4983870 Output 593286 application/pdf Version of Record true © 2022 The Authors. This is an open access article under the CC- BY license true eng http://creativecommons.org/licenses/by/4.0/
title A formal framework for security testing of automotive over-the-air update systems
spellingShingle A formal framework for security testing of automotive over-the-air update systems
Hoang Nguyen
Siraj Shaikh
title_short A formal framework for security testing of automotive over-the-air update systems
title_full A formal framework for security testing of automotive over-the-air update systems
title_fullStr A formal framework for security testing of automotive over-the-air update systems
title_full_unstemmed A formal framework for security testing of automotive over-the-air update systems
title_sort A formal framework for security testing of automotive over-the-air update systems
author_id_str_mv cb24d5c5080534dc5b5e3390f24dd422
50117e8faac2d0937989e14847105704
author_id_fullname_str_mv cb24d5c5080534dc5b5e3390f24dd422_***_Hoang Nguyen
50117e8faac2d0937989e14847105704_***_Siraj Shaikh
author Hoang Nguyen
Siraj Shaikh
author2 Rhys Kirk
Hoang Nguyen
Jeremy Bryans
Siraj Shaikh
Charles Wartnaby
format Journal article
container_title Journal of Logical and Algebraic Methods in Programming
container_volume 130
container_start_page 100812
publishDate 2023
institution Swansea University
issn 2352-2208
doi_str_mv 10.1016/j.jlamp.2022.100812
publisher Elsevier BV
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description 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.
published_date 2023-01-01T04:20:03Z
_version_ 1763754328331386880
score 11.013731

Similar Items