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.
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 DocumentationNote: xml files shall be saved, and then opened with TTool.
System design mixing safety/security mechanisms and properties
- Microwave over with secure remote control To perform the security proof, you should select, when doing the syntax checking of your design model, only the relevant block for security: RemoteControl, WirelessInterface, MicroWaveOven, RemotelyControlledMicrowave
- 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 installationTo 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
- Design diagrams seems to support only a limited set of attributes (e.g, int, boolean), why is it so?
- ProVerif returns an error when performing the proof of security properties, what can I do?
- The proof with ProVerif does not complete after waiting a few hours, what can I do?