Verifying data secure flow in AUTOSAR models
Tóm tắt
This paper presents an approach for enhancing the design phase of AUTOSAR models when security annotations are required. The approach is based on information flow analysis and abstract interpretation. The analysis evaluates the correctness of the model by assessing if the flow of data is secure with respect to causal data dependencies within the model. To find these dependencies an exhaustive search through the model would be required. Abstract interpretation is used as a trade-off between the precision and complexity of the analysis. The approach also provides annotated models without oversizing the set of annotations.
Tài liệu tham khảo
Adelsbach, A., Huber, U., Sadeghi, A.: Secure software delivery and installation in embedded systems. In: Lemke, K., Paar, C., Wolf, M. (eds.) Embedded Security in Cars, pp. 27–49. Springer, Berlin (2006)
AUTOSAR: https://www.autosar.org/
AUTOSAR: General Requirements on Basic Software Modules. https://www.autosar.org/fileadmin/user_upload/standards/classic/3-2/AUTOSAR_SRS_General.pdf
AUTOSAR: Safety Use Case Example. https://www.autosar.org/fileadmin/user_upload/standards/classic/4-3/AUTOSAR_EXP_SafetyUseCase.pdf
AUTOSAR: Specification of Crypto Abstraction Library. https://www.autosar.org/fileadmin/user_upload/standards/classic/4-1/AUTOSAR_SWS_CryptoAbstractionLibrary.pdf
AUTOSAR: Specification of Crypto Service Manager. https://www.autosar.org/fileadmin/user_upload/standards/classic/4-1/AUTOSAR_SWS_CryptoServiceManager.pdf
AUTOSAR: Specification of Module Secure Onboard Communication. https://www.autosar.org/fileadmin/user_upload/standards/classic/4-3/AUTOSAR_SWS_SecureOnboardCommunication.pdf
Avvenuti, M., Bernardeschi, C., De Francesco, N., Masci, P.: Jcsi: a tool for checking secure information flow in java card applications. J. Syst. Softw. 85(11), 24792493 (2012)
Banerjee, A., Naumann, D.A.: Secure information flow and pointer confinement in a java-like language. In: Proceedings of the 15th IEEE Workshop on Computer Security Foundations, CSFW’02, p. 253, Washington, DC, USA (2002)
Barbuti, R., Bernardeschi, C., De Francesco, N.: Abstract interpretation of operational semantics for secure information flow. Inf. Process. Lett. 83(2), 101–108 (2002)
Bell, D.E., LaPadula, L.J.: Secure Computer Systems: Mathematical Foundation. In: MITRE Technical Report 2547, Volume I (1996)
Bernardeschi, C., De Francesco, N., Lettieri, G., Martini, L.: Checking secure information flow in java bytecode by code transformation and standard bytecode verification. Softw. Pract. Exp. 34(13), 1225–1255 (2004)
Bernardeschi, C., Del Vigna, G., Di Natale, M., Dini, G., Varano, D.: Using autosar high-level specifications for the synthesis of security components in automotive systems. In: Hodicky, J. (ed.) International Working on Modelling and Simulation for Autonomous Systems, pp. 101–117. Springer, Berlin (2016)
Bernardeschi, C., Di Natale, M., Dini, G., Varano, D.: Modeling and generation of secure component communications in autosar. In: The 32nd ACM SIGAPP Symposium On Applied Computing. ACM (2017)
Checkoway, S., McCoy, D., Kantor, B., Anderson, D., Shacham, H., Savage, S., Koscher, K., Czeskis, A., Roesner, F., Kohno, T., et al.: Comprehensive experimental analyses of automotive attack surfaces. In: USENIX Security Symposium. San Francisco (2011)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic Comput. 4(2), 511–547 (1992)
Denning, P.J., Denning, D.E.: Certification of programs for secure information flow. Commun. ACM 7(20), 504–513 (1977)
IBM: Rational Rhapsody. https://www.ibm.com/us-en/marketplace/rational-rhapsody/details
Jürjens, J.: UMLsec: extending UML for secure systems development. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002–The Unified Modeling Language, pp. 412–425. Springer, Berlin (2002)
Kehr, S., Pani, M., Quiones, E., Bddeker, B., Sandoval, J.B., Abella, J., Cazorla, F.J., Schfer, G.: Supertask: maximizing runnable-level parallelism in autosar applications. In: 2016 Design, Automation Test in Europe Conference Exhibition (DATE), pp. 25–30 (2016)
Kienberger, J., Minnerup, P., Kuntz, S., Bauer, B.: Analysis and validation of autosar models. In: Proceedings of the 2Nd International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2014, pp. 274–281, Portugal (2014)
Koscher, K., Czeskis, A., Roesner, F., Patel, S., Kohno, T., Checkoway, S., McCoy, D., Kantor, B., Anderson, D., Shacham, H., et al.: Experimental security analysis of a modern automobile. In: 2010 IEEE Symposium on Security and Privacy (SP), pp. 447–462. IEEE (2010)
Leino, K.R.M., Joshi, R.: A semantic approach to secure information flow. In: Proceedings of the 4th International Conference, Mathematics of Program Construction, LNCS 1422, pp. 254–271. Springer, Berlin (1998)
Lemke, K., Paar, C., Wolf, M.: Embedded Security in Cars. Springer, Berlin (2006)
Lin, C., Sangiovanni-Vincentelli, A.: Cyber-security for the controller area network (can) communication protocol. In: 2012 International Conference on Cyber Security, pp. 1–7. IEEE (2012)
Lodderstedt, T., Basin, D., Doser, J.: SecureUML: A UML-based modeling language for model-driven security. In: UML 2002—The Unified Modeling Language 2002, pp. 426–441. Springer, Berlin (2002)
Macher, G., Stolz, M., Armengaud, E., Kreiner, C.: Filling the gap between automotive systems, safety, and software engineering. e & i Elektrotechnik und Informationstechnik 132(3), 142–148 (2015)
MISRA: Guidelines for the Use of the C Language in Vehicle Based Software. Motor Industry Research Association, Nuneaton (1998)
Mizuno, D., Schmidt, M.: A security flow control algorithm and its denotational semantics correctness proof. Form. Asp. Comput. 4(1), 727–754 (1992)
Pani, M., Kehr, S., Quiones, E., Boddecker, B., Abella, J., Cazorla, F.J.: Runpar: An allocation algorithm for automotive applications exploiting runnable parallelism in multicores. In: 2014 International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), pp. 1–10 (2014)
Saad, C., Bauer, B.: Model-Driven Engineering Languages and Systems. MODELS 2013. Lecture Notes in Computer Science. In: Moreira, A., Schätz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.) Data-Flow Based Model Analysis and Its Applications, vol. 8107, pp. 707–723. Springer, Berlin (2013)
Saadatmand, M., Leveque, T.: Modeling security aspects in distributed real-time component-based embedded systems. In: 2012 Ninth International Conference on Information Technology: New Generations (ITNG), pp. 437–444. IEEE (2012)
Sabelfeld, A., Mayers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)
Sabelfeld, A., Sands, D.: Programming Languages and Systems. ESOP 1999. Lecture Notes in Computer Science. In: Swierstra, S.D. (ed.) A Per Model of Secure Information Flow in Sequential Programs, vol. 1576, pp. 40–58. Springer, Berlin (1999)
Stephan, W., Richter, S., Muller, M.: Aspects of secure vehicle software flashing. In: Lemke, K., Paar, C., Wolf, M. (eds.) Embedded Security in Cars, pp. 17–26. Springer, Berlin (2006)
Volpano, D., Smith, G., Irvine, C.: A Sound Type System for Secure Flow Analysis. J. Comput. Secur. 4(3), 167–187 (1992)
Wyglinski, A.M., Huang, X., Padir, T., Lai, L., Eisenbarth, T.R., Venkatasubramanian, K.: Security of autonomous systems employing embedded computing and sensors. Micro IEEE 33(1), 80–86 (2013)
Zdancewic, S., Myers, A.C.: Secure information flow and cps. In: Proceedings of the 10th European Symposium on Programming Languages and Systems, ESOP’01, pp. 46–61, London, UK (2001)