This repository contains the formalization of Cedar and infrastructure for performing differential randomized testing (DRT) between the formalization and Rust production implementation available in cedar.
You can learn more about our formalization efforts in the following blog posts:
- How we built Cedar with automated reasoning and differential testing
- Lean Into Verified Software Development
cedar-leancontains the Lean formalization of, and proofs about, Cedar.cedar-drtcontains code for fuzzing, property-based testing, and differential testing of Cedar.cedar-policy-generatorscontains code for generating schemas, entities, policies, and requests using the arbitrary crate.
See the README in each directory for more information.
- Install Lean, following the instructions here.
cd cedar-leansource ../cedar-drt/set_env_vars.shlake build Cedar
The simplest way to build our DRT framework is to use the included Dockerfile:
docker build . -t cedar_drt # ~10 minutes
docker run --rm -it cedar_drtIf you'd rather not use Docker, here are the full instructions for a local build:
- Install Lean, following the instructions above.
- Clone the
cedarrepository in the current (cedar-spec) repository. source cedar-drt/set_env_vars.shcd cedar-lean && lake build Cedar:static DiffTest:static Std:staticcd ../cedar-drt && cargo build
The build has only been tested on Amazon Linux 2.
To run DRT:
- Follow the build instructions above.
- If running locally,
source ./set_env_vars.sh. cargo fuzz run -s none <target>.
List the available fuzz targets with cargo fuzz list.
Available targets are described in the README in the cedar-drt directory.
That README also explains how to debug build failures, and how to save DRT-generated tests.
Additional commands available with cargo fuzz help.
See CONTRIBUTING for more information.
This project is licensed under the Apache-2.0 License.