一句话：借助 Reckon 分离逻辑与语义反向翻译，将类 C 程序编译到 capability 机器，保证鲁棒安全。
程序常由可信与不可信组件链接，可信组件需在任意不可信代码下保持鲁棒安全。已有封装机制多针对高级或低级语言，尚未在 C 这类不安全语言中实现。本文针对代表性类 C 语言 Rec，将其编译到类 CHERI 的 capability 机器 Cap，以加固编译器获得鲁棒安全。为形式化这一优势，作者提出 Reckon：一种验证 Rec 程序鲁棒安全的分离逻辑；它在 Rec 的不安全语义下不可靠，但在程序经编译加固并链接 Cap 上不可信代码后可靠。证明的关键是一种新的语义反向翻译技术，基于 DimSum 多语言语义框架形式化。所有结果均在 Rocq 中机器化。
It is common for programmers to assemble their programs from a combination of trusted and untrusted components. In this context, a trusted program component is said to be robustly safe if it behaves safely when linked against arbitrary untrusted code. Prior work has shown how various encapsulation mechanisms (in both high- and low-level languages) can be used to protect code so that it is robustly safe, but none of the existing work has explored how robust safety can be achieved in a patently unsafe language like C. In this paper, we show how to bring robust safety to a simple yet representative C-like language we call Rec . Although Rec (like C) is inherently “dangerous” and thus not robustly safe, we can “save” Rec programs via compilation to Cap , a CHERI-like capability machine . To formalize the benefits of such a hardening compiler , we develop Reckon, a separation logic for verifying robust safety of Rec programs. Reckon is not sound under Rec ’s unsafe, C-like semantics, but it is sound when Rec programs are hardened via compilation and linked against untrusted code running on Cap . As a crucial step in proving soundness of Reckon, we introduce a novel technique of semantic back-translation , which we formalize by building on the DimSum framework for multi-language semantics. All our results are mechanized in the Rocq prover.
@article{MuckGDGS26,
title = {Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation},
author = {Niklas Mück and Aïna Linn Georges and Derek Dreyer and Deepak Garg and Michael Sammler},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776682}
}