Skip to Main content Skip to Navigation
Conference papers

Towards a Formal Semantics for System Calls in terms of Information Flow

Laurent Georget 1 Guillaume Piolle 1 Frédéric Tronel 1 Valérie Viet Triem Tong 1 Mathieu Jaume 2
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 : We propose a new semantics for system calls, which focuses on the information flows they generate in a UNIX OS. We built a prototypal model of an OS and system calls using the concurrent transaction logic along with its interpreter. We have yet a few results and applications that show the usefulness of our semantics to model an OS from a kernel point of view. Once completed, we expect our semantics to enable us to extensively test security software implemented inside the kernel, among other use cases.
Complete list of metadatas
Contributor : Guillaume Piolle <>
Submitted on : Thursday, May 7, 2015 - 10:40:25 AM
Last modification on : Friday, July 10, 2020 - 4:23:28 PM


  • HAL Id : hal-01149471, version 1


Laurent Georget, Guillaume Piolle, Frédéric Tronel, Valérie Viet Triem Tong, Mathieu Jaume. Towards a Formal Semantics for System Calls in terms of Information Flow. Tenth International Conference on Systems (ICONS 2015), Apr 2015, Barcelone, Spain. pp.1-4. ⟨hal-01149471⟩



Record views