Search

We propose a holistic methodology for designing automotivesystems that consider security a central concern at every design stage.During the concept design, we model the system architecture and definethe security attributes of its components. We perform threat analysis onthe system model to identify structural security issues. From that analysis,we derive attack trees that define recipes describing steps to successfullyattack the system's assets and propose threat prevention measures.The attack tree allows us to derive a verification and validation (V&V)plan, which prioritizes the testing effort. In particular, we advocate usinglearning for testing approaches for the black-box components. It consistsof inferring a finite state model of the black-box component from its executiontraces. This model can then be used to generate new relevanttests, model check it against requirements, and compare two differentimplementations of the same protocol. We illustrate the methodologywith an automotive infotainment system example. Using the advocated approach, we could also document unexpected and potentially criticalbehavior in our example systems., Comment: Presented at Formal Methods 2023 25th International Symposium (FM'23). 12 pages, 5 figures

As a result of the ever-increasing application of cyber-physical components in the automotive industry, cybersecurity has become an urgent topic. Adapting technologies and communication protocols like Ethernet and WiFi in connected vehicles yields many attack scenarios. Consequently, ISO/SAE 21434 and UN R155 (2021) define a standard and regulatory framework for automotive cybersecurity. Both documents follow a risk management-based approach and require a threat modeling methodology for risk analysis and identification. Such a threat modeling methodology must conform to the Threat Analysis and Risk Assessment (TARA) framework of ISO/SAE 21434. Conversely, existing threat modeling methods enumerate isolated threats disregarding the vehicle's design and connections. Consequently, they neglect the role of attack paths from a vehicle's interfaces to its assets. In other words, they are missing the TARA work products, e.g., attack paths compromising assets or feasibility and impact ratings. We propose a threat modeling methodology to construct attack paths by identifying, sequencing, and connecting vulnerabilities from a valid attack surface to an asset. Initially, we transform cybersecurity guidelines to attack trees, and then we use their formal interpretations to assess the vehicle's design. This workflow yields compositional construction of attack paths along with the required TARA work products (e.g., attack paths, feasibility, and impact). More importantly, we can apply the workflow iteratively in the context of connected vehicles to ensure design conformity, privacy, and cybersecurity. Finally, to show the complexity and the importance of preemptive threat identification and risk analysis in the automotive industry, we evaluate the presented model-based approach in a connected vehicle testing platform, SPIDER., Comment: SAE 2022 Intelligent and Connected Vehicles Symposium

We propose a model-based procedure for automatically preventing security threats using formal models. We encode system models and potential threats as satisfiability modulo theory (SMT) formulas. This model allows us to ask security questions as satisfiability queries. We formulate threat prevention as an optimization problem over the same formulas. The outcome of our threat prevention procedure is a suggestion of model attribute repair that eliminates threats. Whenever threat prevention fails, we automatically explain why the threat happens. We implement our approach using the state-of-the-art Z3 SMT solver and interface it with the threat analysis tool THREATGET. We demonstrate the value of our procedure in two case studies from automotive and smart home domains, including an industrial-strength example.

Supply chain traceability systems have become central in many industries, however, traceability data is often commercially sensitive, and firms seek to keep it confidential to protect their competitive advantage. This is at odds with calls for greater transparency in supply chains for sustainability and efficiency. In this research paper, we develop a solution to this conflict. We demonstrate that sanitised data can be used to confirm the authenticity of products and anonymously verify the rights of an actor to access detailed traceability data. Following a design science methodology, we develop a prototype protocol and verify its performance with traceability data based on the global standard EPCIS., Comment: 10 pages + appendix, 2 tables, 4 figures, to be presented at https://www.euroma2022.org/

In the last years the interconnection and ongoing development of physical systems combined with cyber resources has led to increasing automation. Through this progress in technology, autonomous vehicles, especially autonomous trains are getting more attention from industry and are already under test. The use of autonomous trains is known for increasing operation efficiency and reduction of personnel and infrastructure costs, which is mostly considered for main tracks. However, for less-used secondary lines, autonomous trains and their underlying sensor infrastructure are not yet considered. Thus, a system needs to be developed, which is less expensive for installation and operation of these trains and underlying infrastructure for secondary lines. Therefore, this position paper describes the process of how to derive an approach to help develop a digital interlocking system at design time for the use with secondary railway lines. In this work, we motivate the necessary research by investigating gaps in existing work as well as presenting a possible solution for this problem, a meta-model. The model considers safety, security as well as interoperability like 5G and socio-technical aspects to provide a holistic modeling approach for the development of the interlocking system for industrial secondary line use cases., Comment: The 5th IEEE International workshop on Communication, Computing, and Networking in Cyber Physical Systems (CCNCPS 2019) in association with 20th IEEE International Symposium on a World of Wireless, Mobile and Multimedia Networks (IEEE WoWMoM 2019) - Washington D.C., USA

A homomorphic public key crypto-scheme based on the Boolean Satisfiability Problem is proposed. The public key is a SAT formula satisfied by the private key. Probabilistic encryption generates functions implied to be false by the public key XOR the message bits. A zero-knowledge proof is used to provide signatures., Comment: 7 pages + appendix, 1 figure + 6 in appendix