Heterogeneous Program Verification

Project

Program verifiers are typically developed in isolation and optimized for specific goals. For instance, some verifiers may focus on being highly expressive regarding the specification of data structures and their memory layouts or supporting strong automation capabilities. Examples of such verifiers include VeriFast, which aims to be as expressive as possible, enabling very complex proofs regarding both memory safety and functional correctness. In contrast, CBMC is less expressive but is designed with a strong focus on automation, providing efficient bounded verification. It is important to note that these are just examples, and the project is not limited to these tools.

Different verifiers use varying logical foundations and memory models, making straightforward combinations challenging. For instance, VeriFast employs an abstract memory model based on separation logic, allowing for modular reasoning about data. In contrast, CBMC operates on a more concrete, bit-precise memory model, which provides detailed analysis but is constrained to bounded verification.

Moreover, these verifiers apply distinct proof techniques and achieve different results, complicating the integration of their outcomes. For example, bounded model checking, as implemented in CBMC, provides only bounded guarantees. Using a bounded result from CBMC within a VeriFast proof and treating it as if it holds unboundedly can introduce unsoundness. Therefore, it is essential to track potential unsoundness when combining results from different verification tools and to make this information transparent to the user.

Goal

The goal of this project is to develop a tool that allows combining different verification techniques and verifiers to prove the correctness of various parts of a program. Users will be able to verify specific functions using a deductive verifier like VeriFast while using a bounded model checker like CBMC for other parts. This approach bridges the gap between bounded verification (which provides guarantees within a limited scope) and unbounded verification (which proves correctness across all possible executions).

The tool you will develop should:

  1. Combine Verifiers:
    • Allow users to specify which functions of the program should be verified with which tool. You can also provide a more fine-grained approach, such as using bounded model checking for specific loops and deductive verification for complex functions.
      • You will choose which verifiers to work with, with the only condition being that they must select one bounded verifier and one unbounded verifier.
      • Track Soundness:
        • Ensure that potential unsoundness is tracked when combining verification results from different tools. For example, if a bounded proof is used in a context where an unbounded guarantee is needed, the tool should flag this as a potential issue.
          • Provide clear indicators or warnings to the user about where bounded results are being used as unbounded guarantees, ensuring that they are aware of potential verification gaps. These warnings must be propagated; for instance, if a result marked with a warning is used, it should trigger a warning for the current context as well.
          • User-Friendly Interface:
            • Make the combination of different tools and the tracking of soundness intuitive and transparent for the user, providing clear feedback and a seamless verification process.

            This project addresses the growing need for combining different formal verification approaches to ensure higher coverage and flexibility in verifying complex software systems. We expect this project to be challenging but a lot of fun.

            Starting Points