Unlocking the Power of Environment Assumptions for Unit Proofs

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.