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操作。在编译过程中，我们利用契约将程序对上下文的逻辑假设转换为每次上下文-程序边界跨越时的动态检查。这些边界检查可依赖于监控器状态中存储的过往IO事件信息，但无法在对抗性目标上下文执行危险IO操作之前阻止它。因此，我们进一步要求上下文必须通过一个安全的IO库执行所有IO操作，该库在每次IO操作前使用引用监控动态强制执行访问控制策略。我们提出了一种在F*中建模上下文无法直接访问IO操作及监控器内部状态的新方法，该方法基于F*近期对基于标记的效果多态性的支持。我们在F*中证明，对上下文强制实施访问控制策略，结合程序的静态验证，能够可靠地强制执行全局迹属性。此外，我们在F*中证明我们的安全编译链在构造上满足鲁棒关系超属性保持——这是一个非常强的安全编译标准。最后，我们以一个简单的Web服务器示例展示了安全编译链的实际运行。