From Mock Environments to Ownership-Aware Compilation: Practical Advances in Low-Level Program Reasoning

Abstract

Automated reasoning can improve both the correctness and the performance of systems software. In practice, however, such reasoning matters only when it fits how developers build software and when it scales to realistic codebases. In verification, one workflow challenge is that the cost of modeling the surrounding environment can exceed the cost of verifying the system itself. Another practical difficulty is scaling precise low-level reasoning and optimization to larger bodies of code. To address these problems, this work develops verification and optimization tools built over a low-level intermediate representation, LLVM-IR, integrating directly with existing compiler toolchains.

The thesis first addresses developer workflow friction in verification. vMocks introduces testing-style mocks to code-level formal verification, bringing a familiar testing idiom for specifying environments to a setting where environment modeling is a significant barrier. Instead of building full environment models, developers specify unit-local behavior through SeaMock, a compile-time C++ library compatible with symbolic execution. On the Android Trusty TEE communication layer and the mbedTLS cryptographic library, this approach substantially reduces unit-proof development effort relative to full environment models.

The verify-rust case study extends this workflow-oriented perspective to mixed safe–unsafe Rust programs, where the type system alone cannot enforce whole-program properties such as panic freedom and memory safety. This case study builds on SEABMC, a bit-precise bounded model checker for LLVM-IR introduced in prior work. Because SEABMC operates on LLVM-IR, it verifies these properties directly on the bitcode that the Rust compiler already produces. This lets the approach fit into existing Rust toolchains used in production without requiring a custom frontend.

The thesis then addresses scale by preserving and exploiting ownership semantics in low-level reasoning and optimization. Cache-at-Pointer and SeaUrchin show that ownership information from high-level languages can remain useful after lowering to low-level representations. Cache-at-Pointer develops ownership semantics for an LLVM-like IR. It then uses a pointer cache to simplify low-level memory reasoning by modeling some memory accesses directly at the pointer rather than through a shared address space. SeaUrchin maps Rust’s ownership discipline to LLVM-IR, preserving semantic structure that is normally discarded during compilation and making it available to optimization. As a case study, ownership-aware loop-invariant code motion shows that the preserved ownership information improves LICM efficacy on realistic Rust benchmarks.

Together, these two phases form a single arc: low-level automated reasoning becomes more useful when it better fits developer workflows and when it preserves enough semantic structure to scale. The thesis therefore advances formal verification and compilation not as isolated techniques, but as parts of software engineering practice.