Formalising UPTANE in CSP for Security Testing

Rhys Kirk; Hoang Nga Nguyen; Jeremy Bryans; Siraj Shaikh; David Evans; David Price

Formalising UPTANE in CSP for Security Testing

Rhys Kirk, Hoang Nga Nguyen, Jeremy Bryans, Siraj Shaikh, David Evans, David Price

Centre for Future Transport and Cities

Idiada Automotive Technology UK Ltd.

Research output: Contribution to conference › Paper › peer-review

Abstract

Modern vehicles are susceptible to cybersecurity attacks due to the complexity of their electronics architecture and a progressive integration of connectivity technologies. A promising solution to resolve cybersecurity issues is Over-The-Air (OTA) updates. Recently, Uptane has been introduced and is currently considered as the de facto security standard for automotive OTA system solutions. To ensure that a system, Uptane, can deliver updates to secure a vehicle, the system itself must be secure as to not become an attack vector itself. To this end, we present a model-based security testing approach to OTA updates for automotive vehicles. This is done by modelling the OTA update system and the Dolev-Yao attackers in Communicating sequential processes (CSP). The combined models can be verified to generate security test cases and provide a comprehensive evaluation of attackers on the Uptane system.

Original language	English
Number of pages	9
Publication status	Accepted/In press - 1 Nov 2021
Event	The 21st IEEE International Conference on Software Quality, Reliability, and Security - International Academic Exchange Center of Hainan University, Haikou, China Duration: 6 Dec 2021 → 10 Dec 2021 Conference number: 7 https://qrs21.techconf.org/

Conference

Conference	The 21st IEEE International Conference on Software Quality, Reliability, and Security
Abbreviated title	QRS2021
Country/Territory	China
City	Haikou
Period	6/12/21 → 10/12/21
Internet address	https://qrs21.techconf.org/

Keywords

Automotive Cybersecurity
Uptane
CSP
Automotive OTA
Security Testing

Cite this

@conference{f525f0308b54402b91477862e8c4165e,

title = "Formalising UPTANE in CSP for Security Testing",

abstract = "Modern vehicles are susceptible to cybersecurity attacks due to the complexity of their electronics architecture and a progressive integration of connectivity technologies. A promising solution to resolve cybersecurity issues is Over-The-Air (OTA) updates. Recently, Uptane has been introduced and is currently considered as the de facto security standard for automotive OTA system solutions. To ensure that a system, Uptane, can deliver updates to secure a vehicle, the system itself must be secure as to not become an attack vector itself. To this end, we present a model-based security testing approach to OTA updates for automotive vehicles. This is done by modelling the OTA update system and the Dolev-Yao attackers in Communicating sequential processes (CSP). The combined models can be verified to generate security test cases and provide a comprehensive evaluation of attackers on the Uptane system.",

keywords = "Automotive Cybersecurity, Uptane, CSP, Automotive OTA, Security Testing",

author = "Rhys Kirk and Nguyen, {Hoang Nga} and Jeremy Bryans and Siraj Shaikh and David Evans and David Price",

year = "2021",

month = nov,

day = "1",

language = "English",

note = "The 21st IEEE International Conference on Software Quality, Reliability, and Security, QRS2021 ; Conference date: 06-12-2021 Through 10-12-2021",

url = "https://qrs21.techconf.org/",

}

TY - CONF

T1 - Formalising UPTANE in CSP for Security Testing

AU - Kirk, Rhys

AU - Nguyen, Hoang Nga

AU - Bryans, Jeremy

AU - Shaikh, Siraj

AU - Evans, David

AU - Price, David

N1 - Conference code: 7

PY - 2021/11/1

Y1 - 2021/11/1

N2 - Modern vehicles are susceptible to cybersecurity attacks due to the complexity of their electronics architecture and a progressive integration of connectivity technologies. A promising solution to resolve cybersecurity issues is Over-The-Air (OTA) updates. Recently, Uptane has been introduced and is currently considered as the de facto security standard for automotive OTA system solutions. To ensure that a system, Uptane, can deliver updates to secure a vehicle, the system itself must be secure as to not become an attack vector itself. To this end, we present a model-based security testing approach to OTA updates for automotive vehicles. This is done by modelling the OTA update system and the Dolev-Yao attackers in Communicating sequential processes (CSP). The combined models can be verified to generate security test cases and provide a comprehensive evaluation of attackers on the Uptane system.

AB - Modern vehicles are susceptible to cybersecurity attacks due to the complexity of their electronics architecture and a progressive integration of connectivity technologies. A promising solution to resolve cybersecurity issues is Over-The-Air (OTA) updates. Recently, Uptane has been introduced and is currently considered as the de facto security standard for automotive OTA system solutions. To ensure that a system, Uptane, can deliver updates to secure a vehicle, the system itself must be secure as to not become an attack vector itself. To this end, we present a model-based security testing approach to OTA updates for automotive vehicles. This is done by modelling the OTA update system and the Dolev-Yao attackers in Communicating sequential processes (CSP). The combined models can be verified to generate security test cases and provide a comprehensive evaluation of attackers on the Uptane system.

KW - Automotive Cybersecurity

KW - Uptane

KW - CSP

KW - Automotive OTA

KW - Security Testing

M3 - Paper

T2 - The 21st IEEE International Conference on Software Quality, Reliability, and Security

Y2 - 6 December 2021 through 10 December 2021

ER -

Formalising UPTANE in CSP for Security Testing

Abstract

Conference

Keywords

Fingerprint

Cite this