Unlocking the Power of Environment Assumptions for Unit Proofs

TL;DR

The paper addresses the high cost of specifying environment assumptions for code-level formal verification and introduces vMocks, a verification-oriented analogue to testing mocks, implemented via SeaMock. SeaMock provides a compile-time DSL in C++ that models plausible environments with non-determinism, mitigating runtime overhead and easing adoption for verification tasks. Through evaluation on Android Trusty IPC-style scenarios and 31 mbedTLS SSL message functions, the approach demonstrates practical unit proofs with modest harness and environment footprints, suggesting faster and more scalable verification workflows. The work positions vMocks as a pragmatic bridge to broader formal verification adoption in industry, with future directions including static analysis integration and application to broader testing contexts.

Abstract

Clearly articulating the assumptions of the execution environment is crucial for the successful application of code-level formal verification. The process of specifying a model for the environment can be both laborious and error-prone, often requiring domain experts. In contrast, when engineers write unit tests, they frequently employ mocks (tMocks) to define the expected behavior of the environment in which the function under test operates. These tMocks describe how the environment behaves, e.g., the return types of an external API call (stateless behaviour) or the correct sequence of function calls (stateful behaviour). Mocking frameworks have proven to be highly effective tools for crafting unit tests. In our work, we draw inspiration from tMocks and introduce their counterpart in the realm of formal verification, which we term vMocks. vMocks offer an intuitive framework for specifying a plausible environment when conducting code-level formal verification. We implement a vMock library for the verification of C programs called SEAMOCK. We investigate the practicality of vMocks by, first, comparing specifications styles in the communication layer of the Android Trusty Trusted Execution Environment (TEE) open source project, and second, in the verification of mbedTLS, a widely used open source C library that provides secure communication protocols and cryptography primitives for embedded systems. Based on our experience, we conclude that vMocks complement other forms of environment models. We believe that vMocks ease adoption of code-level formal verification among developers already familiar with tMocks.

Figures (11)

• Figure 1: An SUT and its unit proof from Android Trusty TEE.
• Figure 2: Different environment specification styles for .
• Figure 3: vMock example using SeaMock.
• Figure 4: Expectation map (M) definition and mechanism for wiring a return function.
• Figure 5: High-level mechanism for captureArgAndInvoke.