Verifying the Reliability of Operating System-Level Information Flow Control Systems in Linux - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2017

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

Résumé

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.
Fichier principal
Vignette du fichier
flows_lsm_IEEE.pdf (377.98 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01535862 , version 1 (09-06-2017)

Licence

Copyright (Tous droits réservés)

Identifiants

Citer

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. pp.10-16, ⟨10.1109/FormaliSE.2017.1⟩. ⟨hal-01535862⟩
693 Consultations
662 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More