CT-Wasm Proofs

This repository contains the CT-Wasm model and mechanized proofs of soundness and security.

The CT-WASM Isabelle model may be found in CT-WASM_model.

Lemmas/definitions mentioned in paper, in order of appearance:

• preservation
• equivp_config_indistinguishable
• config_indistinguishable_imp_config_typing
• equivp_action_indistinguishable
• config_indistinguishable_imp_reduce
• config_bisimulation
• config_bisimilar
• typed_indistinguishable_pairs
• config_bisimulation_typed_indistinguishable_pairs
• config_indistinguishable_imp_config_bisimilar
• config_indistinguishable_trace_noninterference
• config_is_trace
• config_trace_set
• trace_set_equiv
• constant_time_traces
• config_untrusted_constant_time_traces
• observation
• config_obs_set
• constant_time

Running the proofs

To run the proofs end-to-end, Isabelle2017 is required; you can download an archive from: https://isabelle.in.tum.de/website-Isabelle2017/index.html

We provide a ROOT file to run all proofs and generate a summary document.

With Isabelle downloaded, run:

git clone [email protected]:PLSysSec/ct-wasm-proofs.git
cd ct-wasm-proofs/CT-WASM_model
<.../bin/isabelle> build -D ./

Note: the isabelle binary you want to use if you downloaded Isabelle from the above link lives in the bin directory. (The binary that lives in the top-level directory is for the IDE and NOT what you want.)

Note: This build will take a very long time due to the need to bootstrap the full Isabelle environment on the first execution.

Moreover, note that existing ROOT files from previous installations of Isabelle2017 may interfere with the build. These may have to be deleted from the .isabelle folder that will have been left somewhere in the home directory.

Running the above commands will produce:

• Summary documents in the CT-WASM_model/output directory.
• Executable type checker CT-WASM_model/Wasm_Printing/Wasm_Extracted/checker.ml

For convenience, we supply a pre-built type checker, session graph, and summary document in the prebuilt folder.

Using docker

For convenience, we provide a docker image to run the proofs without setting up Isabelle in your own environment. Simply run:

./docker-build.sh

This will produce the same artifacts as the local instructions.