Towards a Formal Verification of Secure Vehicle Software Updates
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917095427538944 |
|---|---|
| author | Hagen, Martin Slind Lundqvist, Emil Phu, Alex Wang, Yenan Strandberg, Kim Schiller, Elad Michael |
| author_facet | Hagen, Martin Slind Lundqvist, Emil Phu, Alex Wang, Yenan Strandberg, Kim Schiller, Elad Michael |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_15479 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards a Formal Verification of Secure Vehicle Software Updates Hagen, Martin Slind Lundqvist, Emil Phu, Alex Wang, Yenan Strandberg, Kim Schiller, Elad Michael Cryptography and Security Distributed, Parallel, and Cluster Computing Logic in Computer Science 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. |
| title | Towards a Formal Verification of Secure Vehicle Software Updates |
| topic | Cryptography and Security Distributed, Parallel, and Cluster Computing Logic in Computer Science |
| url | https://arxiv.org/abs/2511.15479 |