nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

A Formal Verification of Safe Update Point Detection in Dynamic Software Updating

verfasst von : Razika Lounas, Nisrine Jafri, Axel Legay, Mohamed Mezghiche, Jean-Louis Lanet

Erschienen in: Risks and Security of Internet and Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Ransomware and the Legacy Crypto API

Nächstes Kapitel Analyzing the Risk of Authenticity Violation Based on the Structural and Functional Sizes of UML Sequence Diagrams

Agence Nationale de la Sécurité des Systèmes d’Information.

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)MATH

10.

Common Criteria. https://www.commoncriteriaportal.org/. Accessed 05 June 2016

11.

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)

12.

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)

13.

Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, New York (2003)

14.

Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRef

15.

SPIN model checker. http://spinroot.com/. Accessed 05 June 2016

16.

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)CrossRef

17.

The modex tool user guide. http://spinroot.com/modex/MANUAL.html. Accessed 05 June 2016

18.

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)

19.

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)CrossRef

20.

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)

21.

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)

22.

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)

23.

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

24.

Murarka, Y.: Online update of concurrent object oriented programs. Ph.D. thesis, Indian Institute of Technology, India (2010)

25.

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

26.

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 CrossRef

27.

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)CrossRef

28.

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

29.

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

Titel: A Formal Verification of Safe Update Point Detection in Dynamic Software Updating
verfasst von: Razika Lounas
Nisrine Jafri
Axel Legay
Mohamed Mezghiche
Jean-Louis Lanet
Verlag: Springer International Publishing
Buch: Risks and Security of Internet and Systems
Print ISBN: 978-3-319-54875-3

Electronic ISBN: 978-3-319-54876-0

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-54876-0_3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"