We propose a holistic methodology for designing automotive systems that consider security a central concern at every design stage. During the concept design, we model the system architecture and define the security attributes of its components. We perform threat analysis on the system model to identify structural security issues. From that analysis, we derive attack trees that define recipes describing steps to successfully attack 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 using learning for testing approaches for the black-box components. It consists of inferring a finite state model of the black-box component from its execution traces. This model can then be used to generate new relevant tests, model check it against requirements, and compare two different implementations of the same protocol. We illustrate the methodology with an automotive infotainment system example. Using the advocated approach, we could also document unexpected and potentially critical behavior in our example systems.
|Title of host publication||Formal Methods. FM 2023|
|Publication status||Published - 6 Mar 2023|
|Event||25th International Symposium on Formal Methods: FM 2023 - Lübeck, Germany|
Duration: 7 Mar 2023 → 9 Mar 2023
|Name||Lecture Notes in Computer Science LNCS|
|Conference||25th International Symposium on Formal Methods|
|Period||7/03/23 → 9/03/23|