• We show how to verify a large and complex system, named UniSUF, by employing problem decomposition techniques and rigorous reasoning. • We formally verify that UniSUF ensures security and correctness in terms of confidentiality, integrity, authenticity, freshness, order, and liveness. 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.

Abstract The automotive industry is increasingly facing growing cybersecurity challenges as vehicles become more connected and autonomous. Modern cars equipped with sophisticated electronic systems are becoming more susceptible to cyber threats. Enhancing detection and forensic capabilities within automotive systems is essential to mitigate these risks. This work builds on and extends a previous systematic literature review of automotive digital forensics, covering 2006 to early 2021. However, recent advances in the field have introduced new challenges and opportunities, particularly in light of an evolving, dynamic threat landscape and growing vehicle complexity. These developments have driven numerous advances, particularly in artificial intelligence, machine learning, and blockchain technologies. In response, we review the latest state-of-the-art developments from 2021 to 2025, addressing critical challenges and technical solutions to provide a comprehensive understanding of the evolving landscape and its implications for both researchers and practitioners. By categorizing and comparing these advancements with prior research, we highlight key trends and innovations, analyze security concerns, and ultimately offer valuable insights into future research directions and emerging trends.

A modern vehicle is no longer merely a transportation vessel. It has become a complex cyber-physical system containing over 100M lines of software code controlling various functionalities such as safety-critical steering, brake, and engine control. The amount of code is anticipated to rise to around 300M lines of code by 2030. Furthermore, even well-tested code will contain more than one bug per 1000 lines of code. Thus, it can be expected that there will be around 100k bugs in a modern vehicle and around 300k bugs in a few years, where some might have a safety-critical impact. Automotive companies are transforming into software companies with more software developed in-house. The ability to hastily and securely patch vulnerabilities has become vital and is a prerequisite when securing modern cars. The UN Regulation No. 156 and the ISO 24089 emphasize the ability to update vehicle software securely.Consequently, we focus on securing the vehicle software update process. Our contributions include defining an attacker model and general security requirements. We further map these requirements to common security goals and directives to ensure broad coverage. Additionally, we present UniSUF, a secure and versatile approach to vehicle software updates. We identify entities involved during vehicle software updates, perform a threat assessment, and map the identified threats to security goals and requirements. The results highlight a secure framework with high industrial relevance that can be used as a reference architecture to guide securing similar software update systems within automotive and related areas such as cyber-physical systems, internet-of-things, and smart cities.

Container-based virtualization is gaining popularity in different domains, as it supports continuous development and improves the efficiency and reliability of run-time environments. Different techniques are proposed for monitoring the security of containers. However, there are no guidelines supporting the selection of suitable techniques for the tasks at hand. We aim to support the selection and design of techniques for monitoring container-based virtualization environments. : First, we review the literature and identify techniques for monitoring containerized environments. Second, we classify these techniques according to a set of categories, such as technical characteristic, applicability, effectiveness, and evaluation. We further detail the pros and cons that are associated with each of the identified techniques. As a result, we present CONSERVE, a multi-dimensional decision support framework for an informed and optimal selection of a suitable set of container monitoring techniques to be implemented in different application domains. A mix of eighteen researchers and practitioners evaluated the ease of use, understandability, usefulness, efficiency, applicability, and completeness of the framework. The evaluation shows a high level of interest, and points out to potential benefits.

Vehicles have become complex computer systems with multiple communication interfaces. In the future, vehicles will have even more connections to e.g., infrastructure, pedestrian smartphones, cloud, road-side-units and the Internet. External and physical interfaces, as well as internal communication buses have shown to have potential to be exploited for attack purposes. As a consequence, there is an increase in regulations which demand compliance with vehicle cyber resilience requirements. However, there is currently no clear guidance on how to comply with these regulations from a technical perspective.To address this issue, we have performed a comprehensive threat and risk analysis based on published attacks against vehicles from the past 10 years, from which we further derive necessary security and resilience techniques. The work is done using the SPMT methodology where we identify vital vehicle assets, threat actors, their motivations and objectives, and develop a comprehensive threat model. Moreover, we develop a comprehensive attack model by analyzing the identified threats and attacks. These attacks are filtered and categorized based on attack type, probability, and consequence criteria. Additionally, we perform an exhaustive mapping between asset, attack, threat actor, threat category, and required mitigation mechanism for each attack, resulting in a presentation of a secure and resilient vehicle design. Ultimately, we present the Resilient Shield a novel and imperative framework to justify and ensure security and resilience within the automotive domain.