The BRiCk C++ Program Logic
BRiCk is a program logic for low-level, concurrent C++ built on the Iris separation logic. BRiCk’s goal is to develop a clear and compositional semantics of C++ programs, that can be used across many levels of abstraction.
Note
This repository does not provide usable verification tooling to apply these principles to real C++ programs. If you are interested in verifying real, concurrent C++ programs using this logic, please open an issue an issue on this repository. BlueRock Security has developed verification tools on top of this semantics that can be used to verify real C++ programs.
The BRiCk release contains two pieces:
The cpp2v tool transforms C++ programs into a format that is digestible by the Coq proof assistant;
The BRiCk program logic describes the meaning of C++ constructs in terms of reasoning principles that enable users to modularly derive the meaning of programs from their constituent pieces.
BRiCk focuses on a tailored (but relatively large) portion of modern C++. Some high-level features (and non-features) include the following:
BRiCk does not currently support some C++ features: e.g. member pointers, exceptions, goto, and virtual inheritance.
BRiCk is currently limited to reasoning about templated code after it has been instantiated.
Some features have restricted use: e.g. BRiCk’s support for switch statements does not support Duff’s device.
BRiCk adopts (limited) extensions to the C++ standard, based on existing research, e.g. for multi-address spaces, assembly interoperability, integer-to-pointer casts, and pointer provenance.
Our full feature set (as well as known issues) can be found on the features page.
BRiCk is a work in progress. We welcome feedback, collaborations, and contributions.