Verifying the Reliability of Operating System-Level Information Flow Control Systems in Linux

Laurent Georget 1 Mathieu Jaume 2 Guillaume Piolle 1 Frédéric Tronel 1 Valérie Viet Triem Tong 1
1 CIDRE - Confidentialité, Intégrité, Disponibilité et Répartition
CentraleSupélec, Inria Rennes – Bretagne Atlantique , IRISA_D1 - SYSTÈMES LARGE ÉCHELLE
2 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : Information Flow Control at Operating System (OS) level features interesting properties and have been an active topic of research for years. However, no implementation can work reliably if there does not exist a way to correctly and precisely track all information flows occurring in the system. The existing implementations for Linux are based on the Linux Security Modules (LSM) framework which implements hooks at speciic points in code where any security mechanism may interpose a security decision in the execution. However, previous works on the verification of LSM only addressed access control and no work has raised the question of the reliability of information flow control systems built on LSM. In this work, we present a compiler-assisted and reproducible static analysis on the Linux kernel to verify that the LSM hooks are correctly placed with respect to operations generating information flows so that LSM-based information flow monitors can properly track all information flows. Our results highlight flaws in LSM that we propose to solve, thus improving the suitability of this framework for the implementation of information flow monitors.
Type de document :
Communication dans un congrès
5th International FME Workshop on Formal Methods in Software Engineering, May 2017, Buenos Aires, Argentina. IEEE Press, pp.10-16, 2017, 〈http://www.formalise.org/〉. 〈10.1109/FormaliSE.2017.1〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01535862
Contributeur : Guillaume Piolle <>
Soumis le : vendredi 9 juin 2017 - 15:48:49
Dernière modification le : jeudi 12 avril 2018 - 01:54:54
Document(s) archivé(s) le : dimanche 10 septembre 2017 - 13:20:11

Fichier

flows_lsm_IEEE.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Copyright (Tous droits réservés)

Identifiants

Citation

Laurent Georget, Mathieu Jaume, Guillaume Piolle, Frédéric Tronel, Valérie Viet Triem Tong. Verifying the Reliability of Operating System-Level Information Flow Control Systems in Linux. 5th International FME Workshop on Formal Methods in Software Engineering, May 2017, Buenos Aires, Argentina. IEEE Press, pp.10-16, 2017, 〈http://www.formalise.org/〉. 〈10.1109/FormaliSE.2017.1〉. 〈hal-01535862〉

Partager

Métriques

Consultations de la notice

549

Téléchargements de fichiers

167