LIO*: Low Level Information Flow Control in F* - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Autre Publication Année : 2020

LIO*: Low Level Information Flow Control in F*

Jean-Joseph Marty
  • Fonction : Auteur
  • PersonId : 1051354
Lucas Franceschino
  • Fonction : Auteur
  • PersonId : 1090610
Jean-Pierre Talpin

Résumé

We present Labeled Input Output in F* (LIO*), a verified framework that enforces information flow control (IFC) policies developed in F* and automatically extracted to C. Inspired by LIO, we encapsulated IFC policies into effects, but using F* we derived efficient, low level, and provably correct code. Concretely, runtime checks are lifted to static proof obligations, the developed code is automatically extracted to C and proved non-interferent using metaprogramming. We benchmarked our framework on three clients and observed up to 54% speedup when IFC runtime checks are proved statically. Our framework is designed to aid development of embedded devices where both enforcement of security policies and low level efficient code is critical.
Fichier principal
Vignette du fichier
2004.12885.pdf (727.32 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03137132 , version 1 (10-02-2021)

Identifiants

Citer

Jean-Joseph Marty, Lucas Franceschino, Jean-Pierre Talpin, Niki Vazou. LIO*: Low Level Information Flow Control in F*. 2020. ⟨hal-03137132⟩
38 Consultations
78 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More