一句话：提出并验证 SCIO⋆ 安全编译框架，通过高阶契约与引用监控，使已验证 IO 程序与不可信上下文链接后仍满足全局轨迹性质。
论文针对已验证 IO 程序与未验证对抗代码链接时，其精化类型及历史 IO 前后条件等逻辑假设可能失效的问题，提出安全编译框架 SCIO⋆。源语言为 F* 子集，程序通过含精化类型和 IO 事件前后条件的高阶接口与 IO 上下文交互；目标语言是更小 F* 子集，编译后程序与缺少这些逻辑接口的对抗上下文链接。为弥合接口差距，SCIO⋆ 形式化验证地结合高阶契约与引用监控：编译用契约把逻辑假设转为边界动态检查，并可依赖监控状态中的历史 IO 事件；链接还强制上下文经安全 IO 库执行 IO，在每次操作前动态实施访问控制。作者在 F* 中证明 SCIO⋆ 可靠强制全局轨迹性质，并构造性地满足 Robust Relational Hyperproperty Preservation（RRHP）这一强安全编译准则；最后以 Web 服务器示例说明。
We introduce SCIO ⋆ , a formally secure compilation framework for statically verified 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.
@article{paperbot2592,
title = {Securing Verified IO Programs Against Unverified Code in F*},
author = {Cezar-Constantin Andrici and Ștefan Ciobâcă and Cătălin Hriţcu and Guido Martínez and Exequiel Rivas and Éric Tanter and Théo Winterhalter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632916}
}