不再误引：安全地提取F*程序及其IO
Misquoted No More: Securely Extracting F* Programs with IO
AI总结：
本文提出了一种安全提取F*程序的方法，通过关系引用和翻译验证，确保提取过程在语义上与原程序保持一致，并提供形式化的安全编译保证。
摘要：
使用monad表示效果的浅层嵌入在证明导向语言中很受欢迎，因为它们在形式验证中很方便。一旦浅层嵌入程序被验证，通常会被提取到主流语言如OCaml或C，并链接到更大的代码库中。提取过程并未完全验证，因为它通常涉及引用——将浅层嵌入程序转换为深层嵌入程序——并且验证引用仍然是一个主要的开放挑战。相反，一些先前的工作通过翻译验证来获得形式正确性保证，以认证个别提取结果。我们在此基础上，但将翻译验证的使用限制在第一步提取中，称为关系引用，并使用一个元程序来构建给定浅层嵌入程序的类型推导。这个元程序很简单，因为类型推导遵循原始程序的结构。一旦我们验证了类型推导对原始程序有效，我们将其传递给一个经过验证的语法生成函数，该函数生成的代码在语义上与原始程序相关。我们应用这一一般想法，构建SEIO*框架，用于将带有IO和精确定义类型的浅层嵌入F*程序提取到深层嵌入的单纯类型lambda演算中，同时提供形式化的安全编译保证。使用两个跨语言逻辑关系，我们设计了一个在F*中可机器检查的证明，证明SEIO*保证了Robust Relational Hyperproperty Preservation (RrHP)，这是一个非常强的安全编译标准，它不仅意味着完全抽象，还意味着对任意链接的对抗性代码的跟踪属性和超属性的保持。这超出了已验证和认证提取的现有状态，迄今为止，这些研究主要集中在正确性而不是安全性上。
英文摘要：
Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C and linked into larger codebases. The extraction process is not fully verified because it often involves quotation -- turning the shallowly embedded program into a deeply embedded one -- and verifying quotation remains a major open challenge. Instead, some prior work obtains formal correctness guarantees using translation validation to certify individual extraction results. We build on this idea, but limit the use of translation validation to a first extraction step that we call relational quotation and that uses a metaprogram to construct a typing derivation for the given shallowly embedded program. This metaprogram is simple, since the typing derivation follows the structure of the original program. Once we validate that the typing derivation is valid for the original program, we pass it to a verified syntax-generation function that produces code guaranteed to be semantically related to the original program. We apply this general idea to build SEIO*, a framework for extracting shallowly embedded F* programs with IO and refinement types to a deeply embedded simply typed lambda-calculus while providing formal secure compilation guarantees. Using two cross-language logical relations, we devise a machine-checked proof in F* that SEIO* guarantees Robust Relational Hyperproperty Preservation (RrHP), a very strong secure compilation criterion that implies full abstraction as well as preservation of trace properties and hyperproperties against arbitrary linked adversarial code. This goes beyond the state of the art in verified and certifying extraction, which so far has focused on correctness rather than security.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
