Journal article 683 views 123 downloads
A formal framework for security testing of automotive over-the-air update systems
Journal of Logical and Algebraic Methods in Programming, Volume: 130, Start page: 100812
Swansea University Authors:
Hoang Nguyen , Siraj Shaikh
-
PDF | Version of Record
© 2022 The Authors. This is an open access article under the CC- BY license
Download (579.38KB)
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...
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>© 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.021648 |