Top

Published in:

2021 | OriginalPaper | Chapter

Formal Modeling: A Step Forward to Cyber Secure Connected Car Systems

Authors : Branka Stojanović, Katharina Hofer-Schmitz, Kai Nahrgang, Heribert Vallant, Christian Derler

Published in: Towards Connected and Autonomous Vehicle Highways

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The paradigm communicate with anyone anywhere at anytime nowadays spans to cyber-physical systems in general including automotive industry. The established path and goal for the automotive industry include connected cars and various services, like autonomous driving. Communication technologies used with connected cars fall into one umbrella, called vehicle-to-everything (V2X). Different sensors and processing units inside connected cars communicate and synchronize using different types of intra-vehicle protocols. In addition to in-vehicle communication, connected cars communicate and interact with their environment, using so-called inter-vehicle protocols. Because of significant advancements in V2X technology, security issues related to them are on the rise. The security-by-design frameworks, including threat modeling and formal methods, have the potential and means to answer these challenges. This chapter contains a comprehensive, security focused, overview of the connected cars’ communication architecture and the most important protocols. Then it discusses security-by-design frameworks application within this domain – threat modeling state of the art methodologies and the ability to adapt those for the automotive industry, and formal verification tools and their applications in V2X protocols space. Furthermore, challenges and future research directions are discussed.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Smart City and Smart Transportation: Intelligent IoT-Based Transportation Objects “Me-Online Mobile Application: A Mutual Practice of Internet of Mobile Things”

next chapter Towards Autonomous Vehicles in Smart Cities: Risks and Risk Governance

https://www.iso.org/standard/63648.html

https://www.iso.org/standard/67244.html

https://www.iso.org/standard/36055.html

https://www.ti.com/lit/an/slla038b/slla038b.pdf

https://www.iso.org/standard/71044.html

https://www.iso.org/standard/59804.html

https://www.iso.org/standard/59806.html

https://www.iso.org/standard/59807.html

https://www.iso.org/standard/59808.html

https://www.iso.org/standard/59809.html

https://standards.ieee.org/standard/802_3bw-2015.html

https://standards.ieee.org/standard/802_3bp-2016.html

https://standards.ieee.org/standard/802_3bv-2017.html

https://standards.ieee.org/standard/802_3cg-2019.html

https://standards.ieee.org/project/802_3ch.html

https://standards.ieee.org/standard/802_11p-2010.html

https://standards.ieee.org/standard/802_11-2016.html

https://standards.ieee.org/standard/1609_12-2019.html

https://www.etsi.org/technologies/automotive-intelligent-transport

https://www.etsi.org/deliver/etsi_en/302600_302699/302663/01.03.01_60/en_302663v010301p .pdf

https://standards.ieee.org/project/802_11bd.html

https://www.3gpp.org/release-14

https://www.etsi.org/deliver/etsi_en/303600_303699/303613/01.01.01_30/en_303613v010101v .pdf

https://www.3gpp.org/release-15

https://www.3gpp.org/release-16

https://www.3gpp.org/release-17

https://www.microsoft.com/en-us/download/details.aspx?id=49168

http://www.avispa-project.org/

https://prosecco.gforge.inria.fr/personal/bblanche/proverif/

https://people.cispa.io/cas.cremers/scyther/

https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf

http://www.uppaal.org/

https://www.prismmodelchecker.org

A. Bazzi, G. Cecchini, M. Menarini, B.M. Masini, A. Zanella, Survey and perspectives of vehicular wi-fi versus sidelink cellular-V2X in the 5G era. Future Internet 11(6), 122 (2019)

B. Stojanović, K. Hofer-Schmitz, Formal methods for connected vehicle protocols, in 2019 27th Telecommunications Forum (TELFOR) (IEEE, 2019), pp. 1–4

E. Hamida, H. Noura, W. Znaidi, Security of cooperative intelligent transport systems: standards, threats analysis and cryptographic countermeasures. Electronics 4(3), 380–423 (2015)CrossRef

A. Alnasser, H. Sun, J. Jiang, Cyber security challenges and solutions for V2X communications: a survey. Comput. Netw. 151, 380–423 (2019)CrossRef

P. Sewalkar, J. Seitz, Vehicle-to-pedestrian communication for vulnerable road users: survey, design considerations, and challenges. Sensors 19(2), 358 (2019)

S. Tuohy, M. Glavin, C. Hughes, E. Jones, M. Trivedi, L. Kilmartin, Intra-vehicle networks: a review. IEEE Trans. Intell. Transp. Syst. 16(2), 534–545 (2014)CrossRef

C. Specification, Version 2.0, Robert Bosch GmbH

R.I. Davis, A. Burns, R.J. Bril, J.J. Lukkien, Controller Area Network (CAN) schedulability analysis: refuted, revisited and revised. Real-Time Syst. 35(3), 239–272 (2007)CrossRef

A.X.A. Sim, B. Sitohang, OBD-II standard car engine diagnostic software development, in 2014 International Conference on Data and Software Engineering (ICODSE) (IEEE, 2014), pp. 1–5

10.

I.A. Grzemba, MOST: The Automotive Multimedia Network (Franzis Verlag, Munchen, 2012)

11.

S.B. Huq, J. Goldie, An overview of LVDS technology. Natl. Semicond. Appl. Note 971, 1–6 (1998)

12.

M. Ruff, Evolution of local interconnect network (LIN) solutions, in 2003 IEEE 58th Vehicular Technology Conference. VTC 2003-Fall (IEEE Cat. No. 03CH37484), Vol. 5 (IEEE, 2003), pp. 3382–3389

13.

P.-S. Murvay, B. Groza, Practical security exploits of the FlexRay in-vehicle communication protocol, in International Conference on Risks and Security of Internet and Systems (Springer, 2018), pp. 172–187

14.

C. Corbett, E. Schoch, F. Kargl, F. Preussner, Automotive ethernet: security opportunity or challenge? Sicherheit 2016-Sicherheit, Schutz und Zuverlässigkeit

15.

A. Masmoudi, K. Mnif, F. Zarai, A survey on radio resource allocation for V2X communication. Wirel. Commun. Mob. Comput. 2019, 1–12 (2019)CrossRef

16.

F. Arena, G. Pau, An overview of vehicular communications. Future Internet 11(2), 27 (2019)

17.

ThreatModeler, Application Threat Modeling vs Operational Threat Modeling (2016). https://threatmodeler.com/operational-application-threat-modeling/

18.

A. Shostack, Threat Modeling (Wiley, Indianapolis, 2014)

19.

B. Strom, ATT&CK 101 (2018). https://www.mitre.org/capabilities/cybersecurity/overview/cybersecurity-blog/attck-1011

20.

B.E. Strom, A. Applebaum, D.P. Miller, K.C. Nickels, A.G. Pennington, C.B. Thomas, MITRE ATT&CK: Design and Philosophy (MITRE, 2018)

21.

MITRE, Cloud Matrix (2019). https://attack.mitre.org/matrices/enterprise/cloud/

22.

B. Schneier, Attack trees. Dr. Dobb’s J. 24(12), 21–29 (1999)

23.

M. Howard, D. LeBlanc, Writing Secure Code (Microsoft Press, Redmond, 2014)

24.

S. Marksteiner, H. Vallant, K. Nahrgang, Cyber security requirements engineering for low-voltage distribution smart grid architectures using threat modeling. J. Inf. Secur. Appl. 49, 102389 (2019)

25.

R. Ankele, S. Marksteiner, K. Nahrgang, H. Vallant, Requirements and recommendations for IoT/IIoT models to automate security assurance through threat modelling, security analysis and penetration testing, in Proceedings of the 14th International Conference on Availability, Reliability and Security (2019), pp. 1–8

26.

C. Corradini, The Automotive Threat Modeling Template (2016). https://www.nccgroup.trust/uk/about-us/newsroom-and-events/blogs/2016/july/the-automotive-threat-modeling-template/

27.

NCCGroup, The Automotive Threat Modeling Template (2017). https://github.com/nccgroup/The_Automotive_Threat_Modeling_Template

28.

Intel, Prioritizing Information Risk Security with Threat Agent Risk Assessment, Technical report, Intel (2009)

29.

A. Karahasanovic, K. Pierre, M. Almgren, Adapting threat modeling methods for the automotive industry, in 15th ESCAR Conference

30.

D. Basin, C. Cremers, C. Meadows, Model checking security protocols, in Handbook of Model Checking (Springer, Cham, 2018), pp. 727–762MATH

31.

K. Keerthi, I. Roy, A. Hazra, C. Rebeiro, Formal verification for security in IoT devices, in Security and Fault Tolerance in Internet of Things (Springer, 2019), pp. 179–200

32.

K. Hofer-Schmitz, B. Stojanović, Towards formal verification of IoT protocols: a review. Comput. Netw. 174, 107233 (2020). doi:https: //doi.org/10.1016/j.comnet.2020.107233. http://www.sciencedirect.com/science/article/pii/S1389128619317116

33.

L. Viganò, Automated security protocol analysis with the AVISPA tool. Electron. Notes Theor. Comput. Sci. 155, 61–86 (2006), in Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI). doi:https: //doi.org/10.1016/j.entcs.2005.11.052. http://www.sciencedirect.com/science/article/pii/S1571066106001897

34.

S. Gürgens, N. Lahr, D. Zelle, On formal security analysis of automotive systems, in 15th Embedded Security in Cars (escar) (2017). http://sit.sit.fraunhofer.de/smv/publications/download/guergensESCAReu2017.pdf

35.

C. Pan, J. Guo, L. Zhu, J. Shi, H. Zhu, X. Zhou, Modeling and verification of CAN bus with application layer using UPPAAL. Electr. Notes Theor. Comput. Sci. 309, 31–49 (2014)CrossRef

36.

D. Thiele, J. Schlatow, P. Axer, R. Ernst, Formal timing analysis of CAN-to-Ethernet gateway strategies in automotive networks. Real-Time Syst 52(1), 88–112 (2016)CrossRef

37.

B. Zhang, On the formal verification of the FlexRay communication protocol, in S. Merz, T. Nipkow (eds.), Automatic Verification of Critical Systems, Automatic Verification of Critical Systems (AVoCS 2006) (Nancy, 2006), pp. 184–189. https://hal.inria.fr/inria-00091667

38.

S. Gordon, S. Choosang, Verification of the FlexRay transport protocol for AUTOSAR in-vehicle communications. Int. J. Veh. Technol. 2010, 1–23 (2010)CrossRef

39.

A. Bruni, M. Sojka, F. Nielson, H.R. Nielson, Formal security analysis of the MaCAN protocol, in International Conference on Integrated Formal Methods (Springer, 2014), pp. 241–255

40.

D. Dolev, A. Yao, On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983). doi:10.1109/TIT.1983.1056650

41.

G. Rodriguez-Navas, J. Proenza, H. Hansson, An UPPAAL model for formal verification of master/slave clock synchronization over the controller area network, in Proceedings of the 6th IEEE International Workshop on Factory Communication Systems, Torino (IEEE Computer Society Press, Los Alamitos, 2006)

42.

C. Tofts, Compositional performance analysis, in E. Brinksma (ed.), Tools and Algorithms for the Construction and Analysis of Systems (Springer, Berlin/Heidelberg, 1997), pp. 290–305CrossRef

43.

A. Koutsos, The 5G-AKA authentication protocol privacy, in 2019 IEEE European Symposium on Security and Privacy (EuroS P) (2019), pp. 464–479. doi: 10.1109/EuroSP.2019.00041

44.

A. Braeken, M. Liyanage, P. Kumar, J. Murphy, Novel 5G authentication protocol to improve the resistance against active attacks and malicious serving networks. IEEE Access 7, 64040–64052 (2019). doi:10.1109/ACCESS.2019.2914941

45.

A. Sharma, I. Sharma, A. Jain, A construction of security enhanced and efficient handover AKA protocol in 5G communication network, in 2019 10th International Conference on Computing, Communication and Networking Technologies (ICCCNT) (2019), pp. 1–6. doi: 10.1109/ICCCNT45670.2019.8944569

46.

K. Han, M. Ma, X. Li, Z. Feng, J. Hao, An efficient handover authentication mechanism for 5G wireless network, in 2019 IEEE Wireless Communications and Networking Conference (WCNC) (2019), pp. 1–8. doi:10.1109/WCNC.2019.8885915.

47.

J. Cao, M. Ma, H. Li, Y. Fu, X. Liu, EGHR: eflcient group-based handover authentication protocols for mMTC in 5G wireless networks. J. Netw. Comput. Appl. 102, 1–16 (2018). doi:https: //doi.org/10.1016/j.jnca.2017.11.009. http://www.sciencedirect.com/science/article/pii/S1084804517303776

48.

C. Zhou, Y. Wang, M. Cao, J. Shi, Y. Liu, Formal analysis of MAC in IEEE 802.11 p with probabilistic model checking, in 2015 International Symposium on Theoretical Aspects of Software Engineering (IEEE, 2015), pp. 55–62

49.

D. Basin, J. Dreier, L. Hirschi, S. Radomirovic, R. Sasse, V. Stettler, A formal analysis of 5G authentication, in Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (ACM, 2018), pp. 1383–1396

50.

C. Cremers, M. Dehnel-Wild, Component-based formal analysis of 5G-AKA: channel assumptions and session confusion, in Network and Distributed Systems Security (NDSS) Symposium 2019 (Internet Society, San Diego, 2019)

51.

J. Zhang, Q. Wang, L. Yang, T. Feng, Formal verification of 5G-EAP-TLS authentication protocol, in 2019 IEEE Fourth International Conference on Data Science in Cyberspace (DSC) (2019), pp. 503–509. doi:10.1109/DSC.2019.00082

52.

J. Zhang, L. Yang, W. Cao, Q. Wang, Formal analysis of 5G EAP-TLS authentication protocol using proverif. IEEE Access 8, 23674–23688 (2020). doi:10.1109/ACCESS.2020.2969474

53.

K. Hofer-Schmitz, B. Stojanović, Towards formal methods of IoT application layer protocols, in 2019 12th CMI Conference on Cybersecurity and Privacy (CMI) (IEEE, 2019), pp. 1–6

Title: Formal Modeling: A Step Forward to Cyber Secure Connected Car Systems
Authors: Branka Stojanović
Katharina Hofer-Schmitz
Kai Nahrgang
Heribert Vallant
Christian Derler
Publisher: Springer International Publishing
Book: Towards Connected and Autonomous Vehicle Highways
Print ISBN: 978-3-030-66041-3

Electronic ISBN: 978-3-030-66042-0

Copyright Year: 2021
DOI: https://doi.org/10.1007/978-3-030-66042-0_6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner