论文标题
lio*：f*中的低级别信息流控制
LIO*: Low Level Information Flow Control in F*
论文作者
论文摘要
我们在F*（LIO*）中提出了标记的输入输出，该框架是一种经过验证的框架，该框架在F*中制定了信息流控制（IFC）策略，并自动提取至C.受LIO的启发，我们将IFC策略封装在效果中，但是使用F*，我们得出了有效的，低级，低级，并且可以证明正确的代码。具体来说，将运行时检查提起为静态证明义务，开发的代码自动提取到C，并使用元编程证明了无间断的代码。我们对三个客户端进行了基准测试，并在静态证明IFC运行时检查时观察到高达54％的速度。我们的框架旨在帮助开发嵌入式设备，在这些设备上，安全策略的执行和低级有效代码都至关重要。
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.
