End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation

TL;DR

This work introduces open safety, a modular, boundary-focused safety predicate defined on open labeled transition systems to enable end-to-end compositional verification of program safety across heterogeneous modules. It blends partial safety (from verifying compilation) with total safety (from verified compilation) through open backward simulations and safety interfaces, avoiding intrusive changes to existing compilers. The authors implement an ownership-oriented language Owlang and its front-end to Clight, plus an ownership-checking pass, and demonstrate end-to-end safety on a hash-map example implemented in Owlang and C. The framework supports modular reasoning about safety, environmental interactions, and compiler assumptions, and it is formalized in Rocq atop CompCertO. The approach promises practical, scalable safety verification for modern systems software that mixes safe and unsafe code while coexisting with verifying compilation tools.

Abstract

Program safety (i.e., absence of undefined behaviors) is critical for correct operation of computer systems. It is usually verified at the source level (e.g., by separation logics) and preserved to the target by verified compilers (e.g., CompCert), thereby achieving end-to-end verification of safety. However, modern safe programming languages like Rust pose new problems in achieving end-to-end safety. Because not all functionalities can be implemented in the safe language, mixing safe and unsafe modules is needed. Therefore, verified compilation must preserve a modular notion of safety which can be composed at the target level. Furthermore, certain classes of errors (e.g., memory errors) are automatically excluded by verifying compilation (e.g., borrow checking) for modules written in safe languages. As a result, verified compilation needs to cooperate with verifying compilation to ensure end-to-end safety. To address the above problems, we propose a modular and generic definition of safety called open safety based on program semantics described as open labeled transition systems (LTS). Open safety is composable at the boundary of modules and can be modularly preserved by verified compositional compilation. Those properties enable separate verification of safety for heterogeneous modules and composition of the safety results at the target level. Open safety can be generalized to partial safety (i.e., only a certain class of errors can occur). By this we formalized the correctness of verifying compilation as derivation of total safety from partial safety. We demonstrate how our framework can combine verified and verifying compilation by developing a verified compiler for an ownership language (called Owlang) inspired by Rust. We evaluate our approach on the compositional safety verification using a hash map implemented by Owlang and C.

Figures (15)

• Figure 1: Verifying Safety for a Program Mixing Rust and C Code
• Figure 2: An Example of Hash Map Implemented in Owlang and C
• Figure 3: Preservation of Partial Correctness via Backward Simulation
• Figure 4: The Framework ( Green: total safety, Red: partial safety)
• Figure 5: Simulation Diagrams for Open Backward Simulation

Theorems & Definitions (21)

• definition 1: Reachability Safety
• definition 2: Progress Property
• definition 3: Open Backward Simulation
• definition 4: Forward Progress Property
• definition 5: Open Safety
• definition 6: Correctness of Verifying Compilation
• theorem 1: Compositionality of Open Safety
• theorem 2: Preservation of Open Total Safety
• definition 7: $\triangleleft$ operator
• definition 8: Partial Forward Progress Property