SysML Model Transformation for Safety and Security Analysis

Rabéa Ameur-Boulifa; Florian Lugou; Ludovic Apvrille

doi:10.1007/978-3-030-16874-2_3

SysML Model Transformation for Safety and Security Analysis

Université Paris-Saclay
Prove & Run

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

14 Citations (Scopus)

Résumé

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.

langue originale	Anglais
titre	Security and Safety Interplay of Intelligent Software Systems - ESORICS 2018 International Workshops, ISSA 2018 and CSITS 2018, Revised Selected Papers
rédacteurs en chef	Asaf Shabtai, Yuval Elovici, Brahim Hamid, Barbara Gallina, Joaquin Garcia-Alfaro
Editeur	Springer Verlag
Pages	35-49
Nombre de pages	15
ISBN (imprimé)	9783030168735
Les DOIs	https://doi.org/10.1007/978-3-030-16874-2_3
état	Publié - 1 janv. 2019
Modification externe	Oui
Evénement	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 - Barcelona, Espagne Durée: 6 sept. 2018 → 7 sept. 2018

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11552 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	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
Pays/Territoire	Espagne
La ville	Barcelona
période	6/09/18 → 7/09/18

Accès au document

10.1007/978-3-030-16874-2_3

Contient cette citation

Ameur-Boulifa, R., Lugou, F., & Apvrille, L. (2019). SysML Model Transformation for Safety and Security Analysis. Dans A. Shabtai, Y. Elovici, B. Hamid, B. Gallina, & J. Garcia-Alfaro (eds.), Security and Safety Interplay of Intelligent Software Systems - ESORICS 2018 International Workshops, ISSA 2018 and CSITS 2018, Revised Selected Papers (p. 35-49). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 11552 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-16874-2_3

Ameur-Boulifa, Rabéa ; Lugou, Florian ; Apvrille, Ludovic. / SysML Model Transformation for Safety and Security Analysis. Security and Safety Interplay of Intelligent Software Systems - ESORICS 2018 International Workshops, ISSA 2018 and CSITS 2018, Revised Selected Papers. Editeur / Asaf Shabtai ; Yuval Elovici ; Brahim Hamid ; Barbara Gallina ; Joaquin Garcia-Alfaro. Springer Verlag, 2019. p. 35-49 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{50c022111bbf4ef18916b3d4b5e85ec0,

title = "SysML Model Transformation for Safety and Security Analysis",

abstract = "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.",

keywords = "Embedded systems, Model-Driven Engineering, Safety, Security, Verification",

author = "Rab{\'e}a Ameur-Boulifa and Florian Lugou and Ludovic Apvrille",

note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.; 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 ; Conference date: 06-09-2018 Through 07-09-2018",

year = "2019",

month = jan,

day = "1",

doi = "10.1007/978-3-030-16874-2\_3",

language = "English",

isbn = "9783030168735",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "35--49",

editor = "Asaf Shabtai and Yuval Elovici and Brahim Hamid and Barbara Gallina and Joaquin Garcia-Alfaro",

booktitle = "Security and Safety Interplay of Intelligent Software Systems - ESORICS 2018 International Workshops, ISSA 2018 and CSITS 2018, Revised Selected Papers",

}

Ameur-Boulifa, R, Lugou, F & Apvrille, L 2019, SysML Model Transformation for Safety and Security Analysis. Dans A Shabtai, Y Elovici, B Hamid, B Gallina & J Garcia-Alfaro (eds), Security and Safety Interplay of Intelligent Software Systems - ESORICS 2018 International Workshops, ISSA 2018 and CSITS 2018, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 11552 LNCS, Springer Verlag, p. 35-49, 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, Barcelona, Espagne, 6/09/18. https://doi.org/10.1007/978-3-030-16874-2_3

SysML Model Transformation for Safety and Security Analysis. / Ameur-Boulifa, Rabéa; Lugou, Florian; Apvrille, Ludovic.
Security and Safety Interplay of Intelligent Software Systems - ESORICS 2018 International Workshops, ISSA 2018 and CSITS 2018, Revised Selected Papers. Ed. / Asaf Shabtai; Yuval Elovici; Brahim Hamid; Barbara Gallina; Joaquin Garcia-Alfaro. Springer Verlag, 2019. p. 35-49 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 11552 LNCS).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - SysML Model Transformation for Safety and Security Analysis

AU - Ameur-Boulifa, Rabéa

AU - Lugou, Florian

AU - Apvrille, Ludovic

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

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 -

Ameur-Boulifa R, Lugou F, Apvrille L. SysML Model Transformation for Safety and Security Analysis. Dans Shabtai A, Elovici Y, Hamid B, Gallina B, Garcia-Alfaro J, rédacteurs en chef, Security and Safety Interplay of Intelligent Software Systems - ESORICS 2018 International Workshops, ISSA 2018 and CSITS 2018, Revised Selected Papers. Springer Verlag. 2019. p. 35-49. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-16874-2_3

SysML Model Transformation for Safety and Security Analysis

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation