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.
Type de document :
Communication dans un congrès
Tenth International Conference on Systems (ICONS 2015), Apr 2015, Barcelone, Spain. IARIA, pp.1-4, 2015, 〈http://thinkmind.org/index.php?view=article&articleid=icons_2015_1_10_40005〉
Liste complète des métadonnées

https://hal-supelec.archives-ouvertes.fr/hal-01149471
Contributeur : Guillaume Piolle <>
Soumis le : jeudi 7 mai 2015 - 10:40:25
Dernière modification le : vendredi 15 juin 2018 - 16:18:03

Identifiants

  • HAL Id : hal-01149471, version 1

Citation

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. IARIA, pp.1-4, 2015, 〈http://thinkmind.org/index.php?view=article&articleid=icons_2015_1_10_40005〉. 〈hal-01149471〉

Partager

Métriques

Consultations de la notice

850