We propose a secure compilation chain for statically verified partial programs with input-output (IO). The source language is an F* subset in which a verified IO-performing program interacts with its IO-performing context via a higher-order interface that includes refinement types as well as pre- and post-conditions about past IO events. The target language is a smaller F* subset in which the compiled program is linked with an adversarial context via an interface without refinement types or pre- and post-conditions. To bridge this interface gap and make compilation and linking secure we propose a novel combination of higher-order contracts and reference monitoring for recording and controlling IO operations. During compilation we use contracts to convert the logical assumptions the program makes about the context into dynamic checks on each context-program boundary crossing. These boundary checks can depend on information about past IO events stored in the monitor's state, yet these checks cannot stop the adversarial target context before it performs dangerous IO operations. So, additionally, our linking forces the context to perform all IO via a secure IO library that uses reference monitoring to dynamically enforce an access control policy before each IO operation. We propose a novel way to model in F* that the context cannot directly access the IO operations and the monitor's internal state, based on F*'s recent support for flag-based effect polymorphism. We prove in F* that enforcing the access control policy on the context in combination with static verification of the program soundly enforces a global trace property. Moreover, we prove in F* that our secure compilation chain satisfies by construction Robust Relational Hyperproperty Preservation, a very strong secure compilation criterion. Finally, we illustrate our secure compilation chain at work on a simple web server example.
翻译:我们为静态核查的部分程序建议一个安全的编译链,并配有输入输出(IO) 。 源语言是一个 F* 子集, 其中, 一个经过验证的 IO 执行程序通过更高阶界面与IO 表现环境互动, 其中包括对过去IO 事件进行精细的种类以及前和后条件。 目标语言是一个较小的 F* 子集, 其中编成的程序通过不改进类型或前和后条件的界面与对抗性背景相联系。 为了弥合这个界面的缺口, 编译和连接安全, 我们提出将更高阶的合同和参考监测相结合, 用于记录和控制 IO 操作。 在编译过程中, 我们使用逻辑假设, 将程序对背景的假设转换成对每个背景- program 边界的动态检查。 这些边界检查可以依赖在监视器状态中存储的关于过去IO 事件的信息, 但是这些检查无法在进行危险的 IO 运行之前通过一个对抗性组合之前, 我们的链接环境来执行所有IO 。 因此, 我们通过一个安全的 IO 库库库 使用引用 快速监控 访问 访问 操作 支持最近的访问 运行 。</s>