Towards a Formal Verification of Secure Vehicle Software Updates

TL;DR

This paper performs a formal security verification of the UniSUF framework for secure vehicle software updates, ensuring it meets key security properties in automotive systems.

Contribution

It introduces a formal verification approach for UniSUF using ProVerif, validating its security guarantees in real-world automotive scenarios.

Findings

UniSUF satisfies confidentiality, integrity, and authenticity requirements.

Formal analysis confirms UniSUF's compliance with security guarantees.

The approach enhances trust in secure vehicle software update frameworks.

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.