README.md


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
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.