TY - GEN
T1 - SysML Model Transformation for Safety and Security Analysis
AU - Ameur-Boulifa, Rabéa
AU - Lugou, Florian
AU - Apvrille, Ludovic
N1 - Publisher Copyright:
© 2019, Springer Nature Switzerland AG.
PY - 2019/1/1
Y1 - 2019/1/1
N2 - While the awareness toward the security and safety of embedded systems has recently improved due to various significant attacks, the issue of building a practical but accurate methodology for designing such safe and secure systems still remains unsolved. Where test coverage is dissatisfying, formal analysis grants much higher potential to discover security vulnerabilities during the design phase of a system. Yet, formal verification methods often require a strong technical background that limits their usage. In this paper, we formally describe a verification process that enables us to prove security-oriented properties such as confidentiality on block and state machine diagrams of SysML. The mathematical description of the translation of these formally defined diagrams into a ProVerif specification enables us to prove the correctness of the verification method.
AB - While the awareness toward the security and safety of embedded systems has recently improved due to various significant attacks, the issue of building a practical but accurate methodology for designing such safe and secure systems still remains unsolved. Where test coverage is dissatisfying, formal analysis grants much higher potential to discover security vulnerabilities during the design phase of a system. Yet, formal verification methods often require a strong technical background that limits their usage. In this paper, we formally describe a verification process that enables us to prove security-oriented properties such as confidentiality on block and state machine diagrams of SysML. The mathematical description of the translation of these formally defined diagrams into a ProVerif specification enables us to prove the correctness of the verification method.
KW - Embedded systems
KW - Model-Driven Engineering
KW - Safety
KW - Security
KW - Verification
UR - https://www.scopus.com/pages/publications/85064880001
U2 - 10.1007/978-3-030-16874-2_3
DO - 10.1007/978-3-030-16874-2_3
M3 - Conference contribution
AN - SCOPUS:85064880001
SN - 9783030168735
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 35
EP - 49
BT - Security and Safety Interplay of Intelligent Software Systems - ESORICS 2018 International Workshops, ISSA 2018 and CSITS 2018, Revised Selected Papers
A2 - Shabtai, Asaf
A2 - Elovici, Yuval
A2 - Hamid, Brahim
A2 - Gallina, Barbara
A2 - Garcia-Alfaro, Joaquin
PB - Springer Verlag
T2 - International Workshop on Interplay of Security, Safety and System/Software Architecture, CSITS 2018, and International Workshop on Cyber Security for Intelligent Transportation Systems, ISSA 2018 held in conjunction with 23rd European Symposium on Research in Computer Security, ESORICS 2018
Y2 - 6 September 2018 through 7 September 2018
ER -