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.

The separation logic framework Iris has been built on the premise that all assertions are stable , meaning they unconditionally enjoy the famous frame rule. This gives Iris—and the numerous program logics that build on it—very modular reasoning principles. But stability also comes at a cost. It excludes a core feature of the Viper verifier family, heap-dependent expression assertions , which lift program expressions to the assertion level in order to reduce redundancy between code and specifications and better facilitate SMT-based automation. In this paper, we bring heap-dependent expression assertions to Iris with Daenerys . To do so, we must first revisit the very core of Iris, extending it with a new form of unstable resources (and adapting the frame rule accordingly). On top, we then build a program logic with heap-dependent expression assertions and lay the foundations for connecting Iris to SMT solvers. We apply Daenerys to several case studies, including some that go beyond what Viper and Iris can do individually and others that benefit from the connection to SMT.

International audience