Advertisement

SysML Model Transformation for Safety and Security Analysis

  • Rabéa Ameur-BoulifaEmail author
  • Florian Lugou
  • Ludovic Apvrille
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11552)

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

Model-Driven Engineering Verification Safety Security Embedded systems 

References

  1. 1.
    Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. J. ACM 52, 102–146 (2005)MathSciNetCrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Allamigeon, X., Blanchet, B.: Reconstruction of attacks against cryptographic protocols. In: 18th IEEE Workshop on Computer Security Foundations, CSFW-18 2005 (2005)Google Scholar
  4. 4.
    Amadio, R.M., Lugiez, D., Vanackère, V.: On the symbolic reduction of processes with cryptographic functions. Theor. Comput. Sci. 290, 695–740 (2003)MathSciNetCrossRefGoogle Scholar
  5. 5.
    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_17CrossRefGoogle Scholar
  6. 6.
    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_27CrossRefGoogle Scholar
  7. 7.
    Blanchet, B., et al.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, vol. 1, pp. 82–96 (2001)Google Scholar
  8. 8.
    Blanchet, B., Smyth, B., Cheval, V.: Automatic cryptographic protocol verifier. User Manual and Tutorial, Technical report (2015)Google Scholar
  9. 9.
    Drouineaud, M., Bortin, M., Torrini, P., Sohr, K.: A first step towards formal verification of security policy properties for RBAC. In: QSIC 2004 (2004)Google Scholar
  10. 10.
    Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Workshop on Formal Methods and Security Protocols (1999)Google Scholar
  11. 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_40CrossRefGoogle Scholar
  12. 12.
    OM Group: System modeling language specification (SysML), version 1.5. Technical reportGoogle Scholar
  13. 13.
    Jürjens, J.: Developing secure embedded systems: pitfalls and how to avoid them. In: 29th International Conference on Software Engineering (2007)Google Scholar
  14. 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_6CrossRefGoogle Scholar
  15. 15.
    Lugou, F.: Environments for analyzing the security of smart objects. Ph.D. thesis, Télécom ParisTech, France (2018)Google Scholar
  16. 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)Google Scholar
  17. 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)Google Scholar
  18. 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)Google Scholar
  19. 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)Google Scholar
  20. 20.
    Toussaint, M.J.: A new method for analyzing the security of cryptographic protocols. IEEE J. Sel. Areas Commun. 11, 702–714 (1993)CrossRefGoogle Scholar
  21. 21.
    Trcek, D., Blazic, B.J.: Formal language for security services base modelling and analysis. Elsevier Sci. J. Comput. Commun. 18, 921–928 (1995)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Rabéa Ameur-Boulifa
    • 1
    Email author
  • Florian Lugou
    • 2
  • Ludovic Apvrille
    • 1
  1. 1.LTCI, Télécom ParisTech, Université Paris-SaclayParisFrance
  2. 2.Prove & RunParisFrance

Personalised recommendations