Abstract
Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.
This work is supported by grant EP/R026092 (FAIR-SPACE Hub) through UKRI under the Industry Strategic Challenge Fund (ISCF) for Robotics and AI Hubs in Extreme and Hazardous Environments.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
We used version 6.4.6 of SPIN.
- 2.
We used version 2.2.0 of Dafny.
- 3.
Artefacts available at: https://github.com/mariefarrell/CAMVerification.git.
- 4.
This only occurs at initialisation when the speed of the other vehicle is 0.
- 5.
We chose 100 as a value but we could easily have chosen some other value.
References
Intelligent Transport Systems (ITS): Vehicular Communications, Basic Set of Applications. Part 2: Specification of Cooperative Awareness Basic Service. Standard Draft ETSI EN 302 637–2, European Telecommunications Standards Institute, November 2018. V1.4.0 (2018–08)
Back, R.-J.: A calculus of refinements for program derivations. Acta Informatica 25(6), 593–624 (1988)
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_17
Ben-Ari, M.: Principles of the Spin model checker. Springer, Cham (2008). https://doi.org/10.1007/978-1-84628-770-1
Bittl, S., Gonzalez, A.A., Myrtus, M., Beckmann, H., Sailer, S., Eissfeller, B.: Emerging attacks on VANET security based on GPS time spoofing. In: IEEE Conference on Communications and Network Security, pp. 344–352. IEEE (2015)
Choi, J., Jin, S.: Security threats in connected car environment and proposal of in-vehicle infotainment-based access control mechanism. In: Park, J.J., Loia, V., Choo, K.-K.R., Yi, G. (eds.) MUE/FutureTech -2018. LNEE, vol. 518, pp. 383–388. Springer, Singapore (2019). https://doi.org/10.1007/978-981-13-1328-8_49
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Farrell, M., Luckcuck, M., Fisher, M.: Robotics and integrated formal methods: necessity meets opportunity. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 161–171. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98938-9_10
Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic. Wiley, Hoboken (2011)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
Huang, L., Kang, E.-Y.: Formal verification of safety and security related timing constraints for a cooperative automotive system. In: Fundamental Approaches to Software Engineering. LNCS, vol. 11424, pp. 210–227. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_12
Jagielski, M., Jones, N., Lin, C.-W., Nita-Rotaru, C., Shiraishi, S.: Threat detection for collaborative adaptive cruise control in connected cars. In: ACM Conference on Security & Privacy in Wireless and Mobile Networks, pp. 184–189. ACM (2018)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)
Kamali, M., Linker, S., Fisher, M.: Modular verification of vehicle platooning with respect to decisions, space and time. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2018. CCIS, vol. 1008, pp. 18–36. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-12988-0_2
Kohnfelder, L., Garg, P.: The threats to our products (April 1999). https://adam.shostack.org/microsoft/The-Threats-To-Our-Products.docx. Accessed 10 Dec 2018
Langenstein, B., Vogt, R., Ullmann, M.: The use of formal methods for trusted digital signature devices. In: Florida Artificial Intelligence Research Society, pp. 336–340. AAAI Press (2000)
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20
Liu, J., Yan, C., Xu, W.: Can you trust autonomous vehicles: contactless attacks against sensors of self-driving vehicles. In: DEFCON24 (2016). http://bit.ly/2EQNOLs
Luckcuck, M., Farrell, M., Dennis, L., Dixon, C., Fisher, M.: Formal Specification and Verification of Autonomous Robotic Systems: A Survey. ACM Computing Surveys, US (2019). accepted
Michele Rondinone, A.C.: Deliverable (d) no: 5.1 definition of v2x message sets. report, Universidad Miguel Hernandez, V1.0 27/08/2018 (August 2018)
Morgan, C., Robinson, K., Gardiner, P.: On the Refinement Calculus. Springer, Cham (1988). https://doi.org/10.1007/978-1-4471-3273-8
Petit, J., Stottelaar, B., Feiri, M., Kargl, F.: Remote attacks on automated vehicles sensors: experiments on camera and lidar. Black Hat Eur. 11, 2015 (2015)
Pnueli, A.: The temporal logic of programs. In: 18th Symposium on the Foundations of Computer Science, pp. 46–57. IEEE (1977)
Ross, R.S.: Guide for conducting risk assessments. Technical report, National Institute of Standards and Technology. SP 800–30 Rev. 1 (September 2012)
Ruddle, A., et al.: Security requirements for automotive on-board networks based on dark-side scenarios. EVITA Deliverable D 2, 3 (2009)
Santa, J., Pereñíguez, F., Moragón, A., Skarmeta, A.F.: Vehicle-to-infrastructure messaging proposal based on CAM/DENM specifications. In: Wireless Days (WD), IFIP, pp. 1–7. IEEE (2013)
Schneider, S.: Formal analysis of a non-repudiation protocol. In: Computer Security Foundations Workshop, pp. 54–65. IEEE (1998)
Schneider, S.: Verifying authentication protocols in CSP. IEEE Trans. Softw. Eng. 24(9), 741–758 (1998)
Schneider, S., Delicata, R.: Verifying security protocols: an application of CSP. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol. 3525, pp. 243–263. Springer, Heidelberg (2005). https://doi.org/10.1007/11423348_14
Snook, C., Hoang, T.S., Butler, M.: Analysing security protocols using refinement in iUML-B. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 84–98. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_6
Stallings, W., Brown, L., Bauer, M.D., Bhattacharjee, A.K.: Computer Security: Principles and Practice. Pearson, Upper Saddle River (2012)
Vanspauwen, G., Jacobs, B.: Verifying protocol implementations by augmenting existing cryptographic libraries with specifications. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 53–68. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_4
Whitefield, J., et al.: Formal analysis of V2X revocation protocols. In: Livraga, G., Mitchell, C. (eds.) STM 2017. LNCS, vol. 10547, pp. 147–163. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68063-7_10
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Farrell, M. et al. (2019). Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages. In: Ölveczky, P., Salaün, G. (eds) Software Engineering and Formal Methods. SEFM 2019. Lecture Notes in Computer Science(), vol 11724. Springer, Cham. https://doi.org/10.1007/978-3-030-30446-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-030-30446-1_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30445-4
Online ISBN: 978-3-030-30446-1
eBook Packages: Computer ScienceComputer Science (R0)