What is SysML-Sec?

SysML-Sec is an environment to design safe and SECURE embedded systems with an extended version of the SysML language. SysML-Sec targets both the software and hardware components of these systems.

SysML-Sec is fully supported by the free and open-source toolkit: TTool.

SysML-Sec has been developed in the scope of the EVITA European Project. Many projects and case studies have already been modeled with SysML-Sec ranging from automotive systems, drone systems, information systems (e.g., the analysis of malware targetting banking systems) and industrial systems (Analysis of SCADA malware), and more generally, security protocols.

Methology

SysML-Sec supports the following methodology stages:

Requirement captures, with specific stereotypes for security-related requirements (e.g., confidentiality, authenticity, integrity, etc.)

Attack graphs, that are an enriched version of attack trees. Moreover, attack graphs are formally defined, and can therefore be studied against some properties, e.g., reachability of a given attack.

Security-aware system architecture definition and exploration, that is, defining the functions, the hardware architectures (CPUs, buses, etc.), and the mapping of functions - and their communications - over the hardware nodes. During that phase, the impact of security mechanisms over the safety and performance of the overall system can be studied, e.g., the additional latencies induced by security mechanisms. Safety and performance properties can be verified with the TTool's built-in model-checker. That model checker takes into acocunt eh characteristics of hardware nodes. For example, in the case of a CPU, it takes into account its pipeline size, its cache meory, etc.

Design of software components including the ones related to safety and security. From the design diagrams - built upon SysML block and state machine diagrams -, safety and security proofs can be performed. Those proofs rely on external toolkits: UPPAAL for safety proofs and ProVerif for security proofs.

Prototyping of sofware components: executable code can be generated from design diagrams. TTool offers a specific support to facilitate the execution of that code in a virtual prototyping environment (SocLib) so to experiment the software components in a more realistic environment that the PC running TTool.

Models and Documentation

Note: xml files shall be saved, and then opened with TTool.

Tutorial

You should start with the SysML-Sec tutorial. This tutorial uses this toy example.

Attack graphs

Zeus/Zitmo

Chuli

System design mixing safety/security mechanisms and properties

Microwave over with secure remote control

Cryptographic protocols

Basic Alice and Bob secure data exchange

Symetric and asymetric key exchange. The two protocols have been defined in the scope of the FP7 EVITA project.

https / TLS model, with authenticated and non authenticated client.

X3DH protocol, used in severla messaging apps.

Key exchange in Intel SGX system.

Impact of security over performance

System architecture with and without security. The model provides two systems. A first one is used to asses the average load of a main CAN bus in an automotive system when no security is provided. Then, the system is enhanced with a key distribution protocol: its impact on the performance, and e.g., the load of the CAN bus, can be studied.

Papers and presentations

Secure HW/SW Partitioning: Letitia W. Li, Florian Lugou and Ludovic Apvrille, "Security-Aware Modeling and Analysis for HW/SW Partitioning", Proceedings of the 5th International Conference on Model-Driven Engineering and Software Development (Modelsward), Porto, Portugal, 19-21 Feb. 2017. paper bibtex slides

Proof of security properties: Florian Lugou, Letitia Li, Ludovic Apvrille, Rabéa Ameur-Boulifa, "SysML Models and Model Transformation for Security", Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2016), Rome, Italy, 19-21 Feb. 2016. paper bibtex.

Safety and security: Ludovic Apvrille, Yves Roudier, "Designing Safe and Secure Embedded and Cyber-Physical Systems with SysML-Sec", Chapter in Model-Driven Engineering and Software Development, p293--308, Springer International Publishing, 2015. online bib

Attack trees/graphs: Ludovic Apvrille, Yves Roudier, "SysML-Sec Attack Graphs: Compact Representations for Complex Attacks", The Second International Workshop on Graphical Models for Security (GramSec'2015), col-located with Co-located with CSF 2015, Verona, Italy - July 13, 2015. paper bibtex slides

Safety and security: Ludovic Apvrille, Yves Roudier, "SysML-Sec: A Model Driven Approach for Designing Safe and Secure Systems", Special session on Security and Privacy in Model Based Engineering, 3rd International Conference on Model-Driven Engineering and Software Development (Modelsward), Angers, France, Feb. 2015. paper bibtex slides

Security Requirements: Yves Roudier, Muhammad Sabir Idrees and Ludovic Apvrille, "Improved Security Requirements Engineering using Knowledge Representation", Proceedings of the 9th conference on the security of network architecture and information systems, May 2014, Lyon, France. paper

Security and safety: Ludovic Apvrille, Yves Roudier, "Towards the Model-Driven Engineering of Secure yet Safe Embedded Systems", The First International Workshop on Graphical Models for Security (GramSec'2014), April, 2014, Grenoble, France. paper bibtex

Security, safety and performance: Ludovic Apvrille, "Ludovic Apvrille, "Model-Driven Engineering for Safety, Security and Performance: SysML-Sec", Invited talk at InSP3CT workshop, Dec. 2017. slides

Methodology: Ludovic Apvrille, Yves Roudier, "SysML-Sec: A Model-Driven Environment for Developing Secure Embedded Systems", Proceedings of the 8th conference on the security of network architecture and information systems (SARSSI'2013), Mont de Marsan, France, 16-18 sept. 2013. paper

Overview of SysML-Sec: Ludovic Apvrille, Yves Roudier, "SysML-Sec: A SysML Environment for the Design and Development of Secure Embedded Systems", Proceedings of the INCOSE/APCOSEC 2013 Conference on system engineering, Yokohama, Japan, September 8-11, 2013. paper

Security requirements: Yves Roudier, Muhammad Sabir Idrees, Ludovic Apvrille, "Towards the Model-Driven Engineering of Security Requirements for Embedded Systems", Proceedings of the Model-Driven Requirements Engineering Workshop (MoDRE'13), Rio de Janeiro, Brazil, July 2013. paper

Application of SysML-Sec to automotive systems: Gabriel Pedroza, Muhammad Sabir Idrees, Ludovic Apvrille, Yves Roudier, "A Formal Methodology Applied to Secure Over-the-Air Automotive Applications", Proceedings of the 74th IEEE Vehicular Technology Conference: VTC2011-Fall, San Francisco, United States, 5-8 September 2011. paper

Application of SysML-Sec to automotive systems: Hendrik Schweppe, Yves Roudier, Benjamin Weyl, Ludovic Apvrille, Dirk Scheuermann, "C2X Communication: Securing the Last Meter", Proceedings of the 4th IEEE International Symposium on Wireless Vehicular Communications: WIVEC2011, San Francisco, United States, 5-6 September 2011. paper bibtex

Download and installation

To use SysML-Sec, you must first install TTool.
Then, if you wish to:

Make proofs of safety properties from AVATAR models, you need to install and configure UPPAAL

Make proofs of security properties from AVATAR models, you need to install and configure ProVerif

Generate, compile and execute prototyping code from AVATAR models, you need to install and configure a C compiler

Generate, compile and execute prototyping code on the SoCLib/MutekH platform from AVATAR models, you need to install and configure SoCLib and MutekH

FAQ

Design diagrams seems to support only a limited set of attributes (e.g, int, boolean), why is it so?

Actually, the formal verification of the design diagrams has more chance to be performed if basic types are used. Yet, data structures can be elaborated from int/boolean types. Also, more complex types can be given in C, but they won't be taken into account by the simulation/verifiers, but are taken inato account only during the code generation process.

ProVerif returns an error when performing the proof of security properties, what can I do?

ProVerif supports only a subset of constructions of the SysML-Sec constructs, and may thus return errors. We are working on that point. Meanwhile, when doing the syntax checking of the diagram, select only the blocks that are really involved in the security features of your system. Also, avoid loops in the state machine diagrams involved in the security verification.

The proof with ProVerif does not complete after waiting a few hours, what can I do?

It is very likely that there is a combinatory explosion, just like it can occur in safety-related model checkers. Try to resolve as much as possible the non usefull non-deterministic elements of your model. Also, you may try to apply hints given in previous questions

Support

Simply send an email to: ludovic.apvrille AT telecom-paris.fr