Handling cybersecurity during system design is mandatory for (critical and) connected embedded systems. Numerous contributions, including standards like ISO 26262, emphasize the need to address cybersecurity as early as possible in the design process. Design space exploration, typically performed early in system design - before software or hardware development - offers an opportunity for early cybersecurity integration. SysML-Sec has demonstrated how cybersecurity concepts can be incorporated into design space exploration. However, its security mechanisms have significant limitations to address some of the modern threats.

The paper introduces a new security modeling and verification approach. Our method enables multi-pattern security channels, allowing multiple security patterns to coexist within a single communication channel. It also supports fine-grained verification of individual write and read operations, ensuring that confidentiality and authenticity are independently validated for each data exchange. Additionally, our approach generates traceable counterexamples for unverified properties, helping engineers identify and address security vulnerabilities.

We implemented this technique in TTool/DIPLODOCUS, a UML/SysML-based framework for hardware/software co-design, demonstrating how its enhanced version can now support more advanced security mechanisms, and evaluated it on an automotive case-study.