LIO *：F* 中的低级信息流控制
LIO*: Low Level Information Flow Control in F*
摘要：
我们在F*（LIO*）中提出了标记输入输出，这是一个经过验证的框架，可以执行在F* 中开发并自动提取到C的信息流控制（IFC）策略。受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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
