We introduce SCIO*, a formally secure compilation framework for statically verified partial programs performing input-output (IO). The source language is an F* subset in which a verified 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 that has an interface without refinement types, pre-conditions, or concrete post-conditions. To bridge this interface gap and make compilation and linking secure we propose a formally verified combination of higher-order contracts and reference monitoring for recording and controlling IO operations. Compilation uses 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 state of the monitor. But these checks cannot stop the adversarial target context before it performs dangerous IO operations. Therefore linking in SCIO* additionally forces the context to perform all IO actions via a secure IO library, which uses reference monitoring to dynamically enforce an access control policy before each IO operation. We prove in F* that SCIO* soundly enforces a global trace property for the compiled verified program linked with the untrusted context. Moreover, we prove in F* that SCIO* satisfies by construction Robust Relational Hyperproperty Preservation, a very strong secure compilation criterion. Finally, we illustrate SCIO* at work on a simple web server example.

翻译：我们提出SCIO*，一个面向执行输入输出（IO）的静态验证部分程序的形式化安全编译框架。源语言是F*子集，其中验证程序通过高阶接口与执行IO的上下文交互，该接口包含精化类型以及关于历史IO事件的前置条件和后置条件。目标语言是更小的F*子集，其中已编译程序与一个具有不包含精化类型、前置条件或具体后置条件的接口的对抗性上下文链接。为弥合这一接口鸿沟并确保编译与链接的安全性，我们提出一种形式化验证的组合方案，结合高阶契约与引用监控来记录和控制IO操作。编译过程使用契约将程序对上下文所做的逻辑假设转换为每次上下文-程序边界跨越时的动态检查。这些边界检查可能依赖于监控状态中存储的历史IO事件信息，但无法在对抗性目标上下文执行危险IO操作之前阻止其行为。因此SCIO*中的链接机制进一步强制上下文通过安全的IO库执行所有IO动作，该库在每次IO操作前使用引用监控动态实施访问控制策略。我们在F*中证明：SCIO*能针对已编译验证程序与不可信上下文链接后的系统，可靠地强制实施全局轨迹属性。此外，我们在F*中证明：SCIO*天然满足鲁棒关系超属性保持这一极强的安全编译准则。最后，我们通过一个简单的Web服务器示例展示SCIO*的实际应用。