CCS 2023 Artifact

This release accompanies our paper submitted to CCS2023, titled: Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts.
We provide a general README.md for the source code, as well as one aimed at the artifact itself: ARTIFACT.md.

The source code is included as a zip and we also provide a docker image that has all the dependencies installed and builds the project.
Getting started with the project can be done by downloading katamaran-ccs23-image.tar.gz, the docker image, and loading it into Docker:

docker load < katamaran-ccs23-image.tar.gz
docker run -it --rm katamaran/ccs23

Katamaran 0.2.0

What's Changed

• Now compatible with Coq 8.14 and 8.15.
• Support for application-specific abstract pure predicates and user-defined solvers.
• The LinkedList toy example now comes with a full instantiation of the Iris model.
• New heuristics for consuming exact and precise chunks.
• Inlining up to a bound for functions without contracts.
• Speed and memory improvements.
• New custom bit vector library.
• Computing verification condition statistics and sizes.
• Support multiple sets of contracts for the same functions.

Full Changelog: https://github.com/katamaran-project/katamaran/commits/v0.2.0

First release v0.1.0

Release version 0.1.0