Abstract
Dynamic Software Updating (DSU) consists in updating running programs on the fly without any downtime. This feature is interesting in critical applications that must run continuously. Because updates may lead to safety errors and security breaches, the question of their correctness is raised. Formal methods are a rigorous means to ensure the high level of safety requested by such applications. The detection of points to perform safe updates is a critical issue in DSU. Indeed, an hazardous update point leads the updated system to erroneous and unexpected behavior. We present in this paper a mechanism to detect safe update points in DSU for Java Card applications. The mechanism is then formally verified using model checking against correctness properties: deadlock free, activeness safety and DSU-liveness.
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
Notes
- 1.
Agence Nationale de la Sécurité des Systèmes d’Information.
References
Baumann, A., Kerr, J., Da Silva, D., Krieger, O., Wisniewski, R.W.: Module hot-swapping for dynamic update and reconfiguration in k42. In: 6th Linux.Conf.Au (2005)
Arnold, J., Kaashoek, M.F.: Ksplice: automatic rebootless kernel updates. In: Proceedings of the 4th ACM European Conference on Computer Systems, EuroSys 2009, pp. 187–198. ACM, New York (2009)
Wahler, M., Oriol, M.: Disruption-free software updates in automation systems. In: Emerging Technology and Factory Automation (ETFA), pp. 1–8. IEEE, September 2014
Holmbacka, S., Lund, W., Lafond, S., Lilius, J.: Lightweight framework for runtime updating of c-based software in embedded systems. In: Presented as Part of the 5th Workshop on Hot Topics in Software Upgrades. USENIX, Berkeley (2013)
Noubissi, A.C., Iguchi-Cartigny, J., Lanet, J.-L.: Hot updates for Java based smart cards, pp. 168–173, April 2011
Liu, J., Tong, W.: A framework for dynamic updating of service pack in the Internet of Things. In: 2011 International Conference on Internet of Things (iThings/CPSCom) and 4th International Conference on Cyber, Physical and Social Computing, pp. 33–42 (2011)
Lounas, R., Mezghiche, M., Lanet, J.-L.: An approach for formal verification of updated Java bytecode programs. In: Hedia, B.B., Vladicescu, F.P. (eds.) Proceedings of the 9th Workshop on Verification and Evaluation of Computer and Communication Systems, VECoS, Bucharest, Romania, 10–11 September, vol. 1431. CEUR Workshop Proceedings, pp. 51–64. CEUR-WS.org (2015)
Charlton, N., Horsfall, B., Reus, B.: Formal reasoning about runtime code update. In: ICDE Workshops, pp. 134–138. IEEE (2011)
Baier, C., Katoen, J.-P.: Principles of Model Checking. Representation and Mind Series. The MIT Press, Cambridge (2008)
Common Criteria. https://www.commoncriteriaportal.org/. Accessed 05 June 2016
Secrétariat général de la défense et de la sécurité nationale. Security requirements for post-delivery code loading. Agence Nationale de la Sécurité des Systèmes d’Information, Paris (2015)
Noubissi, A.C.: Mise á jour dynamique et scurisée de composants systéme dans une carte á puce. Ph.D. thesis, University of Limoges, France (2011)
Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, New York (2003)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
SPIN model checker. http://spinroot.com/. Accessed 05 June 2016
Holzmann, G.J., Smith, M.H.: An automated verification method for distributed systems software based on model extraction. IEEE Trans. Softw. Eng. 28(4), 364–377 (2002)
The modex tool user guide. http://spinroot.com/modex/MANUAL.html. Accessed 05 June 2016
Zhang, M., Ogata, K., Futatsugi, K.: An algebraic approach to formal analysis of dynamic software updating mechanisms. In: Leung, K.R.P.H., Muenchaisri, P. (eds.) 19th Asia-Pacific Software Engineering Conference, APSEC, Hong Kong, China, 4–7 December, pp. 664–673. IEEE (2012)
Zhang, M., Ogata, K., Futatsugi, K.: Formalization and verification of behavioral correctness of dynamic software updates. Electr. Notes Theor. Comput. Sci. 294, 12–23 (2013)
Neamtiu, I., Hicks, M., Foster, J.S., Pratikakis, P.: Contextual effects for version-consistent dynamic software updating and safe concurrent programming. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 37–49. ACM, New York (2008)
Anderson, A., Rathke, J.: Migrating protocols in multi-threaded message-passing systems. In: Proceedings of the 2nd International Workshop on Hot Topics in Software Upgrades, HotSWUp 2009, pp. 8:1–8:5. ACM, New York (2011)
Bierman, G., Hicks, M., Sewell, P., Stoyle, G.: Formalizing dynamic software updating. In: On-line Proceedings of the Second International Workshop on Unanticipated Software Evolution (USE), Warsaw, Poland (2003)
Stoyle, G., Hicks, M., Bierman, G., Sewell, P., Neamtiu, I.: Mutatis mutandis: safe and predictable dynamic software updating. ACM Trans. Program. Lang. Syst. 29(4), August 2007
Murarka, Y.: Online update of concurrent object oriented programs. Ph.D. thesis, Indian Institute of Technology, India (2010)
Murarka, Y., Bellur, U.: Correctness of request executions in online updates of concurrent object oriented programs. In: 15th Asia-Pacific Software Engineering Conference, APSEC 2008, pp. 93–100, December 2008
Hayden, C.M., Magill, S., Hicks, M., Foster, N., Foster, J.S.: Specifying and verifying the correctness of dynamic software updates. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 278–293. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27705-4_22
Makris, K., Ryu, K.D.: Dynamic and adaptive updates of non-quiescent subsystems in commodity operating system kernels. SIGOPS Oper. Syst. Rev. 41(3), 327–340 (2007)
Lv, W., Zuo, X., Wang, L.: Dynamic software updating for onboard software. In: Second International Conference on Intelligent System Design and Engineering Application (ISDEA 2012), pp. 251–253, January 2012
Zhang, M., Ogata, K., Futatsugi, K.: Towards a formal approach to modeling and verifying the design of dynamic software updates. In: Asia-Pacific Software Engineering Conference (APSEC 2015), pp. 159–166, December 2015
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Lounas, R., Jafri, N., Legay, A., Mezghiche, M., Lanet, JL. (2017). A Formal Verification of Safe Update Point Detection in Dynamic Software Updating. In: Cuppens, F., Cuppens, N., Lanet, JL., Legay, A. (eds) Risks and Security of Internet and Systems. CRiSIS 2016. Lecture Notes in Computer Science(), vol 10158. Springer, Cham. https://doi.org/10.1007/978-3-319-54876-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-54876-0_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-54875-3
Online ISBN: 978-3-319-54876-0
eBook Packages: Computer ScienceComputer Science (R0)