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

Razika Lounas 1 Nisrine Jafri 2 Axel Legay 2 Mohamed Mezghiche 1 Jean-Louis Lanet 2
1 LIMOSE - Laboratoire d’Informatique de Modélisation d’Optimisation et de Systèmes Electroniques [Boumerdes]
2 TAMIS - Threat Analysis and Mitigation for Information Security
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : Dynamic Software Updating (DSU) consists in updating running programs on the y 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 veri ed using model checking against correctness properties: deadlock free, activeness safety and DSU-liveness.
Keywords : Update Safety. Dynamic Software Updating Safe Update Point Model Checking
Type de document :
Communication dans un congrès
CRiSIS 2016 - The 11th International Conference on Risks and Security of Internet and Systems , Sep 2016, Roscoff, France. LNCS
Liste complète des métadonnées
https://hal.inria.fr/hal-01405467
Contributeur : Jean-Louis Lanet <>
Soumis le : mercredi 30 novembre 2016 - 08:58:23
Dernière modification le : jeudi 15 novembre 2018 - 11:58:54

Identifiants

  • HAL Id : hal-01405467, version 1

Collections

INRIA | IRISA | CENTRALESUPELEC | UR1-UFR-ISTIC | UNIV-RENNES

Citation

Razika Lounas, Nisrine Jafri, Axel Legay, Mohamed Mezghiche, Jean-Louis Lanet. A Formal Verification of Safe Update Point Detection in Dynamic Software Updating. CRiSIS 2016 - The 11th International Conference on Risks and Security of Internet and Systems , Sep 2016, Roscoff, France. LNCS. 〈hal-01405467〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

443

Contact


archive-ouverte@inria.fr