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
IRISA-D1 - SYSTÈMES LARGE ÉCHELLE, Inria Rennes – Bretagne Atlantique , CentraleSupélec
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 : Tuesday, November 12, 2019 - 4:11:46 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