LIO*: Low Level Information Flow Control in F*

Jean-Joseph Marty, Lucas Franceschino, Jean-Pierre Talpin +1

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…