nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

SysML Model Transformation for Safety and Security Analysis

verfasst von : Rabéa Ameur-Boulifa, Florian Lugou, Ludovic Apvrille

Erschienen in: Security and Safety Interplay of Intelligent Software Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Understanding Common Automotive Security Issues and Their Implications

Nächstes Kapitel The Challenge of Safety Tactics Synchronization for Cooperative Systems

http://sysml-sec.telecom-paristech.fr/.

The term call here is abusive. Indeed, the attacker has no control over the execution flow of each process. It is however able to pass a token to a particular process which is blocked waiting for it.

Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. J. ACM 52, 102–146 (2005)MathSciNetCrossRef

Ali, Y., El-Kassas, S., Mahmoud, M.: A rigorous methodology for security architecture modeling and verification. In: Proceedings of the 42nd Hawaii International Conference on System Sciences (2009)

Allamigeon, X., Blanchet, B.: Reconstruction of attacks against cryptographic protocols. In: 18th IEEE Workshop on Computer Security Foundations, CSFW-18 2005 (2005)

Amadio, R.M., Lugiez, D., Vanackère, V.: On the symbolic reduction of processes with cryptographic functions. Theor. Comput. Sci. 290, 695–740 (2003)MathSciNetCrossRef

Apvrille, L., Roudier, Y.: Designing safe and secure embedded and cyber-physical systems with SysML-Sec. In: Desfray, P., et al. (eds.) Model-Driven Engineering and Software Development, vol. 580, pp. 293–308. Springer, Switzerland (2016). https://doi.org/10.1007/978-3-319-27869-8_17CrossRef

Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_27CrossRef

Blanchet, B., et al.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, vol. 1, pp. 82–96 (2001)

Blanchet, B., Smyth, B., Cheval, V.: Automatic cryptographic protocol verifier. User Manual and Tutorial, Technical report (2015)

Drouineaud, M., Bortin, M., Torrini, P., Sohr, K.: A first step towards formal verification of security policy properties for RBAC. In: QSIC 2004 (2004)

10.

Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Workshop on Formal Methods and Security Protocols (1999)

11.

Eames, D.P., Moffett, J.D.: The integration of safety and security requirements. In: Felici, M., Kanoun, K. (eds.) SAFECOMP 1999. LNCS, vol. 1698, pp. 468–480. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48249-0_40CrossRef

12.

OM Group: System modeling language specification (SysML), version 1.5. Technical report

13.

Jürjens, J.: Developing secure embedded systems: pitfalls and how to avoid them. In: 29th International Conference on Software Engineering (2007)

14.

Kordy, B., Mauw, S., Radomirović, S., Schweitzer, P.: Foundations of attack–defense trees. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 80–95. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19751-2_6CrossRef

15.

Lugou, F.: Environments for analyzing the security of smart objects. Ph.D. thesis, Télécom ParisTech, France (2018)

16.

Lugou, F., Li, L.W., Apvrille, L., Ameur-Boulifa, R.: SysML models and model transformation for security. In: 4th International Conference on Model-Driven Engineering and Software Development (2016)

17.

Maña, A., Pujol, G.: Towards formal specification of abstract security properties. In: The Third International Conference on Availability, Reliability and Security. IEEE (2008)

18.

Pedroza, G., Knorreck, D., Apvrille, L.: AVATAR: a SysML environment for the formal verification of safety and security properties. In: The 11th IEEE Conference on Distributed Systems and New Technologies, NOTERE 2011 (2011)

19.

Shen, G., Li, X., Feng, R., Xu, G., Hu, J., Feng, Z.: An extended UML method for the verification of security protocols. In: 19th International Conference on Engineering of Complex Computer Systems (ICECCS) (2014)

20.

Toussaint, M.J.: A new method for analyzing the security of cryptographic protocols. IEEE J. Sel. Areas Commun. 11, 702–714 (1993)CrossRef

21.

Trcek, D., Blazic, B.J.: Formal language for security services base modelling and analysis. Elsevier Sci. J. Comput. Commun. 18, 921–928 (1995)CrossRef

Titel: SysML Model Transformation for Safety and Security Analysis
verfasst von: Rabéa Ameur-Boulifa
Florian Lugou
Ludovic Apvrille
Verlag: Springer International Publishing
Buch: Security and Safety Interplay of Intelligent Software Systems
Print ISBN: 978-3-030-16873-5

Electronic ISBN: 978-3-030-16874-2

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-16874-2_3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner