cedar-policy/cedar-spec
GitHub: cedar-policy/cedar-spec
Cedar规范仓库提供Cedar策略语言的形式化定义和差异测试基础设施，用于验证其Rust实现与规范的一致性。
Stars: 183 | Forks: 39
# Cedar 规范
本仓库包含 Cedar 的形式化定义以及用于在形式化定义与 [`cedar`](https://github.com/cedar-policy/cedar) 中提供的 Rust 生产实现之间进行差异化随机测试 (DRT) 的基础设施。
您可以通过以下博文了解更多关于我们的形式化工作：
* [我们如何通过自动推理和差异化测试构建 Cedar](https://www.amazon.science/blog/how-we-built-cedar-with-automated-reasoning-and-differential-testing)
* [深入验证软件开发](https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/)
## 仓库结构
* [`cedar-lean`](./cedar-lean) 包含 Cedar 的 Lean 形式化定义及相关证明。
* [`cedar-drt`](./cedar-drt) 包含 Cedar 的模糊测试、基于属性的测试和差异化测试代码。
* [`cedar-policy-generators`](./cedar-policy-generators) 包含使用 [arbitrary](https://docs.rs/arbitrary/latest/arbitrary/index.html#) crate 生成模式、实体、策略和请求的代码。
更多信息请参阅各目录中的 README。
## 构建
### Lean 形式化定义与证明
* 按照 [此处](https://leanprover.github.io/lean4/doc/setup.html) 的说明安装 Lean。
* `cd cedar-lean`
* `source ../cedar-drt/set_env_vars.sh`（仅在 AL2 上运行时需要）
* `lake update`
* `lake build Cedar`
### DRT 框架
构建我们的 DRT 框架最简单的方法是使用提供的 Dockerfile：
```
docker build . -t cedar_drt # ~10 minutes
docker run --rm -it cedar_drt
```
如果您不想使用 Docker，以下是本地构建的完整说明：
* 按照上述说明安装 Lean。
* 在当前 (`cedar-spec`) 仓库中克隆 `cedar` 仓库。
* `source cedar-drt/set_env_vars.sh`
* `cd cedar-lean && ../cedar-drt/build_lean_lib.sh`
* `cd ../cedar-drt && cargo build`
此构建仅在 **Amazon Linux 2** 上测试过。
## 运行
要运行 DRT：
* 按照上述构建说明操作。
* 如果本地运行，请执行 `source ./set_env_vars.sh`。
* `cargo fuzz run -s none `。
使用 `cargo fuzz list` 列出可用的模糊测试目标。
可用目标的描述见于 `cedar-drt` 目录中的 README。
该 README 还说明了如何调试构建失败以及如何保存 DRT 生成的测试。
其他可用命令可通过 `cargo fuzz help` 查看。
## VSCode
要在 VSCode 中使用 `cedar-drt`，首先需要配置两项设置，以便 rust analyzer 插件在尝试查找 Lean 安装时不会报错，并确保它在 `fuzz` crate 中正常工作。
将以下条目添加到您的 `.vscode/settings.json`。首先运行 `source set_env_vars.sh && echo $LEAN_LIB_DIR` 以获取 `LEAN_LIB_DIR` 的正确值。
```
{
"rust-analyzer.linkedProjects": [
"./cedar-drt/fuzz/Cargo.toml",
"./cedar/Cargo.toml",
"./cedar-lean-cli/Cargo.toml",
],
"rust-analyzer.cargo.extraEnv": {
"LEAN_LIB_DIR": <$LEAN_LIB_DIR as populated by set_env_vars.sh>
}
}
```
使用 Lean 形式化定义时的一些额外注意事项，请参阅 [cedar-lean README](./cedar-lean/README.md)。
## 安全
更多信息请参阅 [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications)。
## 许可证
本项目使用 Apache-2.0 许可证。
标签：AWS, Cedar语言, DNS解析, DPI, Lean语言, Rust语言, Streamlit, TLS抓取, 可视化界面, 属性测试, 差异随机测试, 开源项目, 形式化方法, 形式化验证, 授权策略, 测试框架, 策略语言, 自动生成, 访问控制, 请求拦截, 软件安全