Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01535862
Contributor : Guillaume Piolle <>
Submitted on : Friday, June 9, 2017 - 3:48:49 PM
Last modification on : Wednesday, April 8, 2020 - 3:45:00 PM
Document(s) archivé(s) le : Sunday, September 10, 2017 - 1:20:11 PM

File

flows_lsm_IEEE.pdf
Files produced by the author(s)

Licence


Copyright

Identifiers

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. pp.10-16, ⟨10.1109/FormaliSE.2017.1⟩. ⟨hal-01535862⟩

Share

Metrics

Record views

1466

Files downloads

624