Formal Modeling and Verification of CloudProxy

Paper

This paper appeared in VSTTE 2014.
pdf

UCLID Models

To prove a property in the CloudProxy model, you will need to append the property file under the Properties section to the CloudProxy model file (under the CloudProxy Model section). We have provided a shell script: run_cloudproxy.sh that will append each of the property files to the model file and check for all the four properties. You may want to edit the output paths in the script.

CloudProxy Model

cloudproxy_model.ucl

Properties

1. Non-interference: ppty1.ucl
2. Data confidentiality: ppty2.ucl
3. Data integrity: ppty3.ucl
4. Keys protection: ppty4.ucl