LIO*: Low Level Information Flow Control in F*
This work addresses the need for secure and efficient code in embedded devices, though it is incremental as it builds on existing IFC and verification methods.
The authors tackled the problem of enforcing information flow control (IFC) policies efficiently in low-level code by developing LIO*, a verified framework in F* that lifts runtime checks to static proofs and extracts to C, achieving up to 54% speedup in benchmarks.
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.