diff options
| -rw-r--r-- | README.md | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/README.md b/README.md new file mode 100644 index 0000000..9e8c3e9 --- /dev/null +++ b/README.md @@ -0,0 +1,35 @@ +# rego-proofs + +This repository contains the supporting materials for "Software Verification Techniques for Analyzing Access Control Policies". + +## An Embedding of eXtensible Access Control Markup Language + +The source code for the compiler is in the `xacml-proofs/compiler/` directory. +It is a standard OCaml Dune project and can be built with `dune build`. +`main` corresponds to the compiler for XACML policies, and `request` corresponds to the compiler for XACML requests. +The Lean project encoding the semantics of XACML is in the `xacml-proofs/lean/` directory. + +## An Embedding of the Rego Language + +The source code for the compiler is in the `rego-proofs/compiler/` directory. +It is a standard OCaml Dune project and can be built with `dune build`. +The Lean project encoding the semantics of XACML is in the `rego-proofs/Rego/` directory. + +## Case Study: Policy Equivalence + +The proofs described in this section are lines 179 to 613 in `rego-proofs/Rego/Rego.lean`. + +## Case Study: Property Checking + +The proofs described in this section are lines 1291 to 2316 in `xacml-proofs/lean/Xacml.lean`. + +## Case Study: Performance of XACML 3.0 Implementations + +The supporting code for result collection is in the `benchmarks/` directory. +We used the following command to run the benchmarks: + +``` +hyperfine --export-json=[...] "bash authzforce-harness.bash $BENCHMARK" "bash lean-harness.bash $BENCHMARK" "bash rego-harness.bash $BENCHMARK" +``` + +where `$BENCHMARK` is the path of the particular test in the `xacml-3.0-from-2.0-ct` conformance suite. |