The rise in Connected and Automated Vehicles (CAVs) and Intelligent Transport Systems (ITSs) introduced by OEMs has increased the demand for modern vehicle sophistication. This sophistication involves a variety of software capabilities and functionalities embedded in over 100 ECUs in a vehicle. This has led to the need for over-the-air (OTA) updates. OTA updates can be delivered wirelessly, eliminating the need to bring vehicles to the garage for updates. This is more convenient for owners, reduces costs for OEMs, and reduces greenhouse gas emissions. There exist different OTA update considerations that are adopted by automotive OEMs, such as the Uptane framework, Open Mobile Alliance Device Management (OMA-DM) standard, and the general ISO 24089 standard, including subvariance of Uptane and OMA-DM. However, the systematic implementation of security-by-design applying ISO 21434 in OTA systems is less employed, and there remains a gap in this practice of security-by-design that the automotive industry can adapt to ensure a systematic approach to secure OTA update technology. OTA update security hinges on identifying vulnerability pathways for potential malicious attacks. Therefore, identifying and mitigating potential vulnerabilities throughout the OTA update process is critical for robust security. This paper proposes an adaptable security-by-design approach to OTA update, built and extended from our work Iyieke et al. (2023). The adaptable security-by-design approach is then applied to a developed prototype OTA update system based on the Uptane framework as implemented by Toradex. Security-by-design is a well-established concept in enterprise systems, but is still developing in the cyber–physical system of automotive cybersecurity. Our proposed approach covers the security engineering lifecycle, the logical security layered concept, and the security architecture. A threat analysis and risk assessment (TARA) is performed based on the international automotive cybersecurity standard ISO/SAE 21434. The highest threats identified from the TARA are formalized, and corresponding mitigation actions are defined according to UNECE WP29. Penetration testing is conducted to verify the approach’s capability to reinforce the security of the OTA update systems against some of the identified risks and threats. Our proposed approach provides a systematic and adaptable security-by-design approach to ensure secure OTA updates in modern vehicles; OEMs and other stakeholders can use it to develop secure OTA systems regardless of the OTA update technology used.

Safety and security interdependencies have been of interest for researchers for several decades. However, in practice, they are not given the necessary consideration yet due to various reasons, such as lack of understanding and reluctance to change current practices. This research is aimed at advancing the state of the art in this area by developing a practical, easy to adapt and to use methodology for managing interdependencies and trade-offs throughout the development lifetime of cyber physical systems. The methodology is named TOMSAC, short for Trade-Off Management between Safety And Cyber security.

Modern vehicles are comparable to desktop computers due to the increase in connectivity. This fact also extends to potential cyber-attacks. A solution for preventing and mitigating cyber attacks is Over-The-Air (OTA) updates. This solution has also been used for both desktops and mobile phones. The current de facto OTA security system for vehicles is Uptane, which is developed to solve the unique issues vehicles face. The Uptane system needs to have a secure method of updating; otherwise, attackers will exploit it. To this end, we have developed a comprehensive and model-based security testing approach by translating Uptane and our attack model into formal models in Communicating Sequential Processes (CSP). These are combined and verified to generate an exhaustive list of test cases to see to which attacks Uptane may be susceptible. Security testing is then conducted based on these generated test cases, on a test-bed running an implementation of Uptane. The security testing result enables us to validate the security design of Uptane and some vulnerabilities to which it is subject.

Modern automotive platforms are cyber-physical in nature and increasingly connected. Cybersecurity testing of such platforms is expensive and carries safety concerns, making it challenging to perform tests for vulnerabilities and refine test methodologies. We propose a testbed, built over a Controller Area Network (CAN) simulator, and validate it against a real-world demonstration of a weakness in a test vehicle using aftermarket On Board Diagnostic (OBD) scanners (dongles).

Maintaining semantic consistency of data is a significant problem in distributed information systems, particularly those on which a business may depend. Our current work aims to use Event-B and the Rodin tools to support the specification and design of such systems in a way that integrates well into existing development processes. This paper presents Event-B patterns that may be used to represent recovery from time-bounded inconsistency and illustrates their use in a model derived from industrial applications.

Distributed information systems are critical to the functioning of many businesses; designing them to be dependable is a challenging but important task. We report our experience in using formal methods to enhance processes and tools for development of business information software based on service-oriented architectures. In our work, which takes place in an industrial setting, we focus on the configuration of middleware, verifying application-level requirements in the presence of faults. In pilot studies provided by SAP, we used the Event-B formalism and the open Rodin tools platform to prove properties of models of business protocols and expose weaknesses of certain middleware configurations with respect to particular protocols. We then extended the approach to use models automatically generated from diagrammatic design tools, opening the possibility of seamless integration with current development environments. Increased automation in the verification process, through domain-specific models and theories, is a goal for future work.

Abstract The paper discusses the GOLD project (Grid‐based Information Models to Support the Rapid Innovation of New High Value‐Added Chemicals) whose principal aim is to carry out research and development into enabling technologies to support the formation, operation and termination of virtual organizations. The paper discusses the outcome of this research, which is the GOLD Middleware infrastructure. The infrastructure has been implemented in the form of a set of Middleware components, which address issues such as trust, security, contract monitoring and enforcement, information management and coordination. We discuss all these issues in turn and more importantly we demonstrate how current WS standards can be used to implement these issues. In addition, the paper follows a top down approach starting with a brief outline on the architectural elements derived during the requirements engineering phase and demonstrates how these elements were mapped onto actual services that were implemented according to service‐oriented architecture principles and related technologies. Copyright © 2008 John Wiley & Sons, Ltd.

Elections are increasingly dependent on computers and telecommunication systems. Such "e-voting" schemes create socio-technical systems (combinations of technology and human organisations) that are complex and critical, as the future of nations depends on their proper operation. Thus heated debate surrounds their adoption and the possible methods for making them demonstrably dependable. We discuss the dependability requirements for such systems, and the design issues in ensuring their satisfaction, with reference to a recent proposal that uses cryptography for fault tolerance, in order to avoid some of the perceived dangers of electronic voting. Our treatment highlights the need for considering the whole socio-technical system, and for integrating security and fault tolerance viewpoints.

Dynamic coalitions are temporary alliances formed between agents in order to achieve specific business goals. Such coalitions can vary widely in architecture, scale, complexity and lifetime. Few techniques have so far emerged to assist in the analysis and design of coalitions. We apply formal model- oriented techniques to help structure the space of dynamic coalitions, with an emphasis on modelling information flow. A series of models is developed in VDM, each emphasising a different "dimension" of the space. These are used to characterise a new dynamic coalition architecture under development for the chemical engineering industry. Tool-supported analysis of this formal model has identified potential improvements in the coalition architecture.

Modern distributed systems include a class of applications in which non-functional requirements are important. In particular, these applications include multimedia facilities where real time constraints are crucial to their correct functioning. In order to specify such systems it is necessary to describe that events occur at times given by probability distributions; stochastic automata have emerged as a useful technique by which such systems can be specified and verified.However, stochastic descriptions are very general, in particular they allow the use of general probability distribution functions, and therefore their verification can be complex. In the last few years, model checking has emerged as a useful verification tool for large systems. In this article we describe two model checking algorithms for stochastic automata. These algorithms consider how properties written in a simple probabilistic real-time logic can be checked against a given stochastic automaton.

It is now well recognized that the next generation of distributed systems will be distributed multimedia systems. Central to multimedia systems is quality of service, which defines the non-functional requirements on the system. In this paper we investigate how stochastic process algebra can be used in order to determine the quality of service properties of distributed multimedia systems. We use a simple multimedia stream as our basic example. We describe it in the stochastic process algebra PEPA and then we analyse whether the stream satisfies a set of quality of service parameters: throughput, end-to-end latency, jitter and error rates.