Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards a Formal Verification of Secure Vehicle Software Updates

Martin Slind Hagen, Emil Lundqvist, Alex Phu, Yenan Wang, Kim Strandberg, Elad Michael Schiller

TL;DR

This work addresses the urgent need for secure software updates in software-defined vehicles by formalizing UniSUF and proving its security properties under a Dolev-Yao adversary using ProVerif. The authors introduce a modular, design-by-verification approach, decomposing the update process into sub-problems (preparation, encapsulation, decapsulation) and mapping each to precise security requirements (confidentiality, integrity, authenticity, freshness, order, liveness). They develop a ProVerif-based framework with novel techniques to model the multi-ECU update flow, symbolic execution, and verification of critical properties like inter-/intra-round uniqueness and termination, demonstrating that UniSUF can satisfy the specified guarantees in their formal model. While the results provide strong design-time security assurances, the authors acknowledge that translating these guarantees to real-world implementations requires further study, especially regarding broader attacker models and scalability to large vehicular networks.

Abstract

With the rise of software-defined vehicles (SDVs), where software governs most vehicle functions alongside enhanced connectivity, the need for secure software updates has become increasingly critical. Software vulnerabilities can severely impact safety, the economy, and society. In response to this challenge, Strandberg et al. [escar Europe, 2021] introduced the Unified Software Update Framework (UniSUF), designed to provide a secure update framework that integrates seamlessly with existing vehicular infrastructures. Although UniSUF has previously been evaluated regarding cybersecurity, these assessments have not employed formal verification methods. To bridge this gap, we perform a formal security analysis of UniSUF. We model UniSUF's architecture and assumptions to reflect real-world automotive systems and develop a ProVerif-based framework that formally verifies UniSUF's compliance with essential security requirements - confidentiality, integrity, authenticity, freshness, order, and liveness - demonstrating their satisfiability through symbolic execution. Our results demonstrate that UniSUF adheres to the specified security guarantees, ensuring the correctness and reliability of its security framework.

Towards a Formal Verification of Secure Vehicle Software Updates

TL;DR

This work addresses the urgent need for secure software updates in software-defined vehicles by formalizing UniSUF and proving its security properties under a Dolev-Yao adversary using ProVerif. The authors introduce a modular, design-by-verification approach, decomposing the update process into sub-problems (preparation, encapsulation, decapsulation) and mapping each to precise security requirements (confidentiality, integrity, authenticity, freshness, order, liveness). They develop a ProVerif-based framework with novel techniques to model the multi-ECU update flow, symbolic execution, and verification of critical properties like inter-/intra-round uniqueness and termination, demonstrating that UniSUF can satisfy the specified guarantees in their formal model. While the results provide strong design-time security assurances, the authors acknowledge that translating these guarantees to real-world implementations requires further study, especially regarding broader attacker models and scalability to large vehicular networks.

Abstract

With the rise of software-defined vehicles (SDVs), where software governs most vehicle functions alongside enhanced connectivity, the need for secure software updates has become increasingly critical. Software vulnerabilities can severely impact safety, the economy, and society. In response to this challenge, Strandberg et al. [escar Europe, 2021] introduced the Unified Software Update Framework (UniSUF), designed to provide a secure update framework that integrates seamlessly with existing vehicular infrastructures. Although UniSUF has previously been evaluated regarding cybersecurity, these assessments have not employed formal verification methods. To bridge this gap, we perform a formal security analysis of UniSUF. We model UniSUF's architecture and assumptions to reflect real-world automotive systems and develop a ProVerif-based framework that formally verifies UniSUF's compliance with essential security requirements - confidentiality, integrity, authenticity, freshness, order, and liveness - demonstrating their satisfiability through symbolic execution. Our results demonstrate that UniSUF adheres to the specified security guarantees, ensuring the correctness and reliability of its security framework.

Paper Structure

This paper contains 79 sections, 4 theorems, 12 equations, 33 figures, 16 tables.

Table of Contents

  1. Introduction
  2. Existing Solutions and Their Shortcomings
  3. Our Contribution
  4. Related Work
  5. Formal Verification Tools
  6. Formal Verification of Automotive and IoT Software Update Protocols
  7. Preliminaries
  8. System Settings
  9. Threat Model
  10. Cryptographic Primitives, Notations, and Assumptions
  11. Update Rounds
  12. Problem Definition
  13. UniSUF Architecture
  14. Cryptographic Materials
  15. System Entities
  16. ...and 64 more sections

Key Result

Lemma 6.1

Consider an entity $E$ and a handling $e(r,\ d,\ \ell)$, $E$ executes $e(r,\ d,\ \ell)$ at most once.

Figures (33)

  • Figure 1: High-level overview of the UniSUF architecture showing the main entities and update flow. \ref{['ch:subproblems']} details the architecture components, see Figures \ref{['fig:preparation']} to \ref{['fig:stream_update_to_ecu']}.
  • Figure 2: Different cryptographic materials in UniSUF are shown, each with its respective key. Figure derived from UniSUF.
  • Figure 3: Internal structure of a VUUP file. The blue items are used in the download process, while the green ones are used for the installation process. Note that the VUUP content has been signed by $VCM\xspace_{Cert}$. The figure is derived from UniSUF.
  • Figure 4: Different cryptographic materials in UniSUF and how they are encrypted. Figure derived from UniSUF.
  • Figure 5: Diagram of all the entities and their communication in UniSUF. Dotted arrows denote communication channels between entities from different modules. The black arrows denote secure communications, while the sole red arrow denotes an insecure communication link.
  • ...and 28 more figures

Theorems & Definitions (6)

  • Lemma 6.1
  • proof
  • Corollary 6.1.1
  • Lemma 6.2
  • proof
  • Corollary 6.2.1