一句话：SecRef* 框架让 F* 中已验证代码与未验证代码安全共享可变引用，并用契约与形式证明保证互操作可靠。
本文针对在 F* 中验证的有状态程序与链接的未验证代码动态共享 ML 风格可变引用时的安全性与可验证性问题。SecRef* 区分可与未验证代码共享的引用和不可共享引用：后者内容在调用未验证代码后保证不变，该通用性质被暴露给已验证程序。对于已验证代码期望未验证代码满足的 refinement types、前置与后置条件，框架通过高阶契约将其转换为对共享引用的动态检查。作者在 F* 中形式化证明该策略保证健全且安全的互操作。由于 SecRef* 建立在 F* 的 Monotonic State 效应之上，证明还依赖本文提出的该效应首个 monadic 表示，这一表示可独立使用。最后，作者实现了一个与未验证线程安全交互的协作式多线程调度器。
We introduce SecRef ★ , a secure compilation framework protecting stateful programs verified in F ★ against linked unverified code, with which the program dynamically shares ML-style mutable references. To ease program verification in this setting, we track which references are shareable with the unverified code, and which ones are not shareable and whose contents are thus guaranteed to be unchanged after calling into unverified code. This universal property of non-shareable references is exposed in the interface on which the verified program can rely when calling into unverified code. The remaining refinement types and pre- and post-conditions that the verified code expects from the unverified code are converted into dynamic checks about the shared references by using higher-order contracts. We prove formally in F ★ that this strategy ensures sound and secure interoperability with unverified code. Since SecRef ★ is built on top of the Monotonic State effect of F ★ , these proofs rely on the first monadic representation for this effect, which is a contribution of our work that can be of independent interest. Finally, we use SecRef ★ to build a simple cooperative multi-threading scheduler that is verified and that securely interacts with unverified threads.
@article{paperbot3056,
title = {SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*},
author = {Cezar-Constantin Andrici and Danel Ahman and Cătălin Hriţcu and Ruxandra Icleanu and Guido Martínez and Exequiel Rivas and Théo Winterhalter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747522}
}