Formally Verifying the Security and Privacy of an Adopted Standard for Software-Update in Cars: Verifying Uptane 2.0

Ioana Boureanu

doi:10.1109/SMC53992.2023.10394216

Back

Formally Verifying the Security and Privacy of an Adopted Standard for Software-Update in Cars: Verifying Uptane 2.0

Conference proceeding

Open access

Formally Verifying the Security and Privacy of an Adopted Standard for Software-Update in Cars: Verifying Uptane 2.0

Ioana Boureanu

Conference proceedings / IEEE International Conference on Systems, Man, and Cybernetics

2023 IEEE International Conference on Systems, Man, and Cybernetics (SMC) (Honolulu, Oahu, HI, USA, 01/10/2023–04/10/2023)

29/01/2024

DOI: https://doi.org/10.1109/SMC53992.2023.10394216

Abstract

— In this paper, we formally analyse the security of Uptane 2.0 – the latest version 1 of a framework for over-the-air (online) delivery of software to cars. We are doing so by using the threat model and security requirements found in standard document that accompanies Uptane 2.0, as well as a modulation of this threat model and requirements added by ourselves, for a deeper analysis. To undertake this verification, we use the well-known formal protocol-verifier and theorem prover called Tamarin. We discuss our responsible disclosure to and work with the Uptane Alliance.

Files and links (1)

pdf

uptane461.03 kBDownload View

Author's Accepted Manuscript Open Access

Metrics

71 File views/ downloads

31 Record Views

Details

Title: Formally Verifying the Security and Privacy of an Adopted Standard for Software-Update in Cars: Verifying Uptane 2.0
Creators: Ioana Boureanu (Author) - University of Surrey, School of Computer Science and Electronic Engineering
Publication Details: Conference proceedings / IEEE International Conference on Systems, Man, and Cybernetics
Conference: 2023 IEEE International Conference on Systems, Man, and Cybernetics (SMC) (Honolulu, Oahu, HI, USA, 01/10/2023–04/10/2023)
Publisher: IEEE
Publication Date: 29/01/2024
Date accepted for publication: 27/05/2023
Grants: AutoPaSS: Automatic Verification of Complex Privacy Requirements in Unbounded- Size Secure Systems, EP/S024565/1, Engineering and Physical Sciences Research Council (United Kingdom, Swindon) - EPSRC
Identifiers: 99847966502346
Copyright: © 2023 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.”
Academic Unit: School of Computer Science and Electronic Engineering
Language: English
Resource Type: Conference proceeding

Formally Verifying the Security and Privacy of an Adopted Standard for Software-Update in Cars: Verifying Uptane 2.0

Abstract

Files and links (1)

Metrics

Details

Usage Policy