AWS Templates for CBMC Proofs

This repository includes templates and scripts intended to make it easy to get started writing CBMC proofs for your code. The first script installs proof infrastructure in the form of a few directories containing code, templates, and Makefiles that facilitate writing CBMC proofs in general. The second script installs, for a particular proof, a directory containing skeletons of all the files needed to start writing that proof.

Proof infrastructure set up

The script scripts/setup.py will set up the infrastructure for CBMC proofs.

• Choose the path to the source root (eg, /usr/project)
• Choose the path to a directory under the source root that should hold the infrastructure (eg, /usr/project/cbmc)
• Submodule the AWS-templates-for-CBMC repository into this directory (eg, /usr/project/cbmc/aws-templates-for-cbmc)

  cd /usr/project/cbmc
  git submodule add https://github.com/awslabs/aws-templates-for-cbmc-proofs.git aws-templates-for-cbmc-proofs
  

• Use the script aws-templates-for-cbmc-proofs/scripts/setup.py to setup the standard directory structure for CBMC proof.

  cd /usr/project/cbmc
  python3 aws-templates-for-cbmc-proofs/scripts/setup.py
  

  The script will ask for the path to the source root /usr/project. The script will install the directories
  • include: contains include files for the proofs
  • sources: contains source code for the proofs
  • stubs: contains stubs for the proofs
  • proofs: contains the proofs themselves (the proof root).

Proof set up

The script scripts/setup-proof.py will set up a directory for a CBMC proof.

• Change to a directory under the proof root (/usr/project/cbmc/proofs)
• Run the script aws-templates-for-cbmc/scripts/setup-proof.py and give
  • The name of the function under test.
  • The path to the source file defining the function under test.
  • The path to the source root

The script will create a directory named for the function, and will install files needed to run the proof.

You can cut and paste into the files, and type make to run and debug the proof. For more details, see the instructions in the training materials repository.

Security

See CONTRIBUTING for more information.

License

This project is licensed under the Apache-2.0 License.