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.