j-arndt/fedcloud
GitHub: j-arndt/fedcloud
FedCloud 将云基础设施状态转换为 Lean 4 数学证明和 OSCAL 合规工件，以形式化验证方式自动化 FedRAMP 持续授权流程。
Stars: 0 | Forks: 0
# FedCloud — 联邦云授权的形式化验证网关
[](https://github.com/j-arndt/fedcloud/actions/workflows/ci.yml)
[](https://j-arndt.github.io/fedcloud/)
[](https://lean-lang.org/)
[](https://pages.nist.gov/OSCAL/)
[](https://python.org/)
[](https://github.com/j-arndt/fedcloud/actions/workflows/ci.yml)
**用数学证明取代合规性叙述。**
FedCloud 使用混合双引擎架构自动执行持续合规性验证：一个用于结构化控制确定性数学证明的 [Lean 4](https://lean-lang.org/) 内核，以及用于重策略控制定性语义分析的 [Amazon Bedrock](https://aws.amazon.com/bedrock/) 代理。这两个引擎生成的输出将被组装成 [OSCAL](https://pages.nist.gov/OSCAL/) 工件，以实现持续授权。
## 架构
```
flowchart TB
subgraph INGEST["① Telemetry Ingestion"]
CT["AWS CloudTrail"]
CFG["AWS Config"]
EB["EventBridge"]
S3["S3 Uploads
PDFs · SBOMs · Certs"] APP["App Metadata
Tyler · LMS · HR"] end ROUTER{"② Lambda Router
AC · IA controls"] L2["🔑 Cryptographic
SC controls"] L3["🏗️ Architecture
CM · SC · SI controls"] L4["📊 Monitoring
AU · SI controls"] end subgraph BEDROCK["④ Amazon Bedrock Agents — Qualitative Analysis"] direction LR B1["👤 Personnel
PS controls"] B2["🎓 Training
AT controls"] B3["🚨 Incident Response
IR controls"] B4["🔄 Recovery
CP controls"] B5["📦 Supply Chain
SA · SR controls"] end subgraph GUARD["⑤ Guardrails"] direction LR RAG["RAG Grounding"] JSON["JSON Schema"] CITE["Citation Check"] HALL["Hallucination Detection"] end ROUTER -- "State JSON
deterministic" --> LEAN ROUTER -- "Documents & Logs
qualitative" --> BEDROCK BEDROCK --> GUARD subgraph OSCAL["⑥ OSCAL Assembler"] RECEIPT["Signed Receipt
HMAC-SHA256"] SSP["System Security Plan
FedRAMP Moderate"] AR["Assessment Results
OSCAL 1.1.2"] NAR["Audit Narratives
Markdown + Citations"] end LEAN --> RECEIPT GUARD --> RECEIPT RECEIPT --> SSP RECEIPT --> AR RECEIPT --> NAR CONMON["⑦ Continuous Authorization
Federal Gateway"] SSP & AR & NAR --> CONMON style INGEST fill:#1e293b,stroke:#334155,color:#e2e8f0 style LEAN fill:#1e3a5f,stroke:#3b82f6,color:#e2e8f0 style BEDROCK fill:#3b1f4a,stroke:#a855f7,color:#e2e8f0 style GUARD fill:#1a2e1a,stroke:#22c55e,color:#e2e8f0 style OSCAL fill:#2d1f0e,stroke:#f59e0b,color:#e2e8f0 style ROUTER fill:#0f172a,stroke:#60a5fa,color:#e2e8f0 style CONMON fill:#0f172a,stroke:#10b981,color:#e2e8f0 ``` ## 混合架构 系统根据控制类型将每个控制集群路由到相应的验证引擎： - **确定性控制**（结构化、可二元验证）流向 **Lean 4 内核**，该内核生成数学证明。相同的输入始终产生相同的结果，并且每个证明都是可独立检查的。 - **定性控制**（重策略、依赖上下文）流向 **Amazon Bedrock 代理**，这些代理通过对策略文档知识库进行 RAG 检索来执行基于语义的分析。在接受结果之前，Guardrails 会验证输出并抑制幻觉。 路由器 (`agents/router.py`) 对传入的遥测数据进行分类，并将每个集群分派给正确的引擎。两个引擎都会发出结构化的发现结果，OSCAL 汇编程序会将这些结果合并到统一的 SSP 和评估结果文档中。 ## 安全集群 该网关跨越两个引擎涵盖九个安全集群。 ### 确定性集群（Lean 4 内核） | 集群 | 不变量 | 控制 | |---------|-----------|----------| | **身份与访问** | 特权会话需要防钓鱼 MFA；token ≤ 60 分钟 | AC-2, AC-3, AC-6, IA-2, IA-5 | | **加密保护** | 联邦数据使用 FIPS-140-3 模块静态加密 | SC-8, SC-12, SC-13, SC-28 | | **架构不可变性** | 仅限已签名的镜像；无 shell 访问权限；无开放的 ingress | CM-2, CM-6, CM-7, SC-7, SI-7 | | **持续监控** | 主动记录到防篡改目标；保留期 ≥ 365 天 | AU-2, AU-6, AU-9, AU-11, SI-4 | 每个不变量都表示为正式的 Lean 4 定理，并带有相应的决策过程，从而产生具体的验证结果。 ### 定性集群（Amazon Bedrock 代理） | 集群 | 分析范围 | 控制 | |---------|----------------|----------| | **人员安全** | 背景调查、NDA 验证、IAM 配置时间 | PS-1 到 PS-8 | | **网络安全教育** | 培训完成情况、重新认证窗口期 | AT-1 到 AT-4 | | **事件响应** | 时间线重建、分诊指标、联邦报告 | IR-1 到 IR-8 | | **恢复计划** | DR 演练验证、RTO/RPO 验证 | CP-1, CP-2, CP-4, CP-6, CP-7, CP-9, CP-10 | | **供应链** | SBOM 分析、CVE 上下文化、风险叙述 | SA-4, SA-5, SA-9, SA-11, SR-1, SR-2, SR-3 | 每个 Bedrock 代理从知识库中检索相关的策略文档，应用语义推理，并返回带有引用的结构化发现结果。 ## 快速开始 ### 前置条件 - Python 3.9+ - [Lean 4](https://lean-lang.org/lean4/doc/setup.html)（用于证明编译） - 带有 Bedrock 访问权限的 AWS 凭据（用于定性代理集群） ### 运行流水线（模拟模式） ``` # 克隆 repository git clone https://github.com/j-arndt/fedcloud.git cd fedcloud # 运行所有测试（Lean 4 和 Bedrock agent 套件中总计 64 个） python -m pytest translator/tests/ oscal/tests/ agents/tests/ -v # 针对 mock fixtures 执行完整 pipeline python -m scripts.run_pipeline --mode mock --state fixtures/mock_aws_topology.json # 查看 output artifacts ls output/ # → SystemState.lean verification_receipt.json fedcloud_ssp.json assessment_results.json ``` ### 构建 Lean 4 验证引擎 ``` cd lean # 通过 elan 安装 Lean curl https://elan.lean-lang.org/install/linux -sSf | sh # 构建 verification library lake build # 针对 sample states 运行 proof checker lean FedCloud/Verify.lean ``` ### Docker ``` docker build -t fedcloud-gateway . docker run -v $(pwd)/fixtures:/data fedcloud-gateway /data/mock_aws_topology.json ``` ## 项目结构 ``` fedcloud/ ├── lean/ # Lean 4 formal verification engine │ ├── lakefile.lean # Lake build configuration │ ├── lean-toolchain # Lean version pin (v4.28.0) │ └── FedCloud/ │ ├── BaseModel.lean # Core type definitions │ ├── Verify.lean # Orchestrator + sample states │ └── Invariants/ │ ├── Identity.lean # IAM cluster invariant │ ├── Crypto.lean # Cryptographic protection invariant │ ├── Architecture.lean # Immutability invariant │ └── Monitoring.lean # Continuous monitoring invariant ├── agents/ # Bedrock qualitative verification engine │ ├── base_agent.py # Shared agent with RAG + citations │ ├── config.py # Bedrock model and routing config │ ├── router.py # Deterministic vs qualitative router │ ├── lambda_handler.py # AWS Lambda entry point │ ├── guardrails.py # Output validation and hallucination checks │ ├── knowledge_base.py # RAG policy document retrieval │ ├── clusters/ │ │ ├── personnel.py # KSI-PS agent │ │ ├── training.py # KSI-CED agent │ │ ├── incident_response.py # KSI-INR agent │ │ ├── recovery.py # KSI-RPL agent │ │ └── supply_chain.py # KSI-TPR agent │ └── tests/ │ └── test_agents.py # Agent unit tests ├── translator/ # JSON → Lean translation layer │ ├── json_to_lean.py # Multi-format state translator │ ├── state_ingestion.py # State collection service │ └── tests/ │ └── test_translator.py # Translator unit tests ├── oscal/ # OSCAL synthesis pipeline │ ├── receipt_generator.py # Signed verification receipts │ ├── ssp_updater.py # SSP component injection │ ├── assessment_results.py # OSCAL Assessment Results │ ├── templates/ │ │ └── fedramp_moderate_ssp.json # Baseline SSP template │ └── tests/ │ └── test_pipeline.py # Pipeline integration tests ├── fixtures/ # Mock telemetry data │ ├── mock_aws_topology.json # Sample AWS infrastructure state │ ├── mock_terraform_plan.json # Sample Terraform plan │ └── mock_tyler_app_schema.json # Sample application metadata ├── scripts/ │ └── run_pipeline.py # Pipeline orchestrator ├── docs/ # HTML documentation ├── .github/workflows/ci.yml # GitHub Actions CI ├── Dockerfile # Container build └── README.md ``` ## 工作原理 ### 1. 状态摄取 基础架构状态是从 AWS Config、CloudTrail、EventBridge 和应用程序 API 收集的。在 PoC 模式下，由模拟夹具模拟这些来源。 ### 2. 转换 `json_to_lean.py` 转换器将 JSON 负载转换为带类型的 Lean 4 定义。它处理多种输入格式（原始状态、Terraform plan、应用程序 schema），并将它们标准化为 `SystemState` 结构。 ### 3. 形式化验证 Lean 4 内核将转换后的状态与不变量定理库一起编译。如果所有证明都成立，则系统在数学上得到验证。如果任何不变量失败，则会识别出具体的违规情况。 ### 4. 凭证生成 加密签名 (HMAC-SHA256) 的 JSON 凭证会捕获验证结果、输入状态哈希、时间戳以及每个集群的状态。 ### 5. OSCAL 综合 该凭证被注入到 OSCAL SSP 中，并使用验证元数据更新组件定义。系统将生成一份单独的 OSCAL 评估结果文档，其中包含映射到各控制系列的发现结果。 ## 验证保证 与基于扫描的合规工具不同，该系统提供： - **确定性**：相同的输入始终产生相同的验证结果 - **完整性**：范围内的每个资源都会针对每个适用的不变量进行检查 - **防篡改证据**：凭证使用输入状态哈希进行加密签名 - **可审计性**：Lean 4 证明逻辑可供第三方检查和验证 ## 许可证 MIT
PDFs · SBOMs · Certs"] APP["App Metadata
Tyler · LMS · HR"] end ROUTER{"② Lambda Router
agents/router.py"}
CT & CFG & EB --> ROUTER
S3 & APP --> ROUTER
subgraph LEAN["③ Lean 4 Kernel — Deterministic Proofs"]
direction LR
L1["🔐 Identity & AccessAC · IA controls"] L2["🔑 Cryptographic
SC controls"] L3["🏗️ Architecture
CM · SC · SI controls"] L4["📊 Monitoring
AU · SI controls"] end subgraph BEDROCK["④ Amazon Bedrock Agents — Qualitative Analysis"] direction LR B1["👤 Personnel
PS controls"] B2["🎓 Training
AT controls"] B3["🚨 Incident Response
IR controls"] B4["🔄 Recovery
CP controls"] B5["📦 Supply Chain
SA · SR controls"] end subgraph GUARD["⑤ Guardrails"] direction LR RAG["RAG Grounding"] JSON["JSON Schema"] CITE["Citation Check"] HALL["Hallucination Detection"] end ROUTER -- "State JSON
deterministic" --> LEAN ROUTER -- "Documents & Logs
qualitative" --> BEDROCK BEDROCK --> GUARD subgraph OSCAL["⑥ OSCAL Assembler"] RECEIPT["Signed Receipt
HMAC-SHA256"] SSP["System Security Plan
FedRAMP Moderate"] AR["Assessment Results
OSCAL 1.1.2"] NAR["Audit Narratives
Markdown + Citations"] end LEAN --> RECEIPT GUARD --> RECEIPT RECEIPT --> SSP RECEIPT --> AR RECEIPT --> NAR CONMON["⑦ Continuous Authorization
Federal Gateway"] SSP & AR & NAR --> CONMON style INGEST fill:#1e293b,stroke:#334155,color:#e2e8f0 style LEAN fill:#1e3a5f,stroke:#3b82f6,color:#e2e8f0 style BEDROCK fill:#3b1f4a,stroke:#a855f7,color:#e2e8f0 style GUARD fill:#1a2e1a,stroke:#22c55e,color:#e2e8f0 style OSCAL fill:#2d1f0e,stroke:#f59e0b,color:#e2e8f0 style ROUTER fill:#0f172a,stroke:#60a5fa,color:#e2e8f0 style CONMON fill:#0f172a,stroke:#10b981,color:#e2e8f0 ``` ## 混合架构 系统根据控制类型将每个控制集群路由到相应的验证引擎： - **确定性控制**（结构化、可二元验证）流向 **Lean 4 内核**，该内核生成数学证明。相同的输入始终产生相同的结果，并且每个证明都是可独立检查的。 - **定性控制**（重策略、依赖上下文）流向 **Amazon Bedrock 代理**，这些代理通过对策略文档知识库进行 RAG 检索来执行基于语义的分析。在接受结果之前，Guardrails 会验证输出并抑制幻觉。 路由器 (`agents/router.py`) 对传入的遥测数据进行分类，并将每个集群分派给正确的引擎。两个引擎都会发出结构化的发现结果，OSCAL 汇编程序会将这些结果合并到统一的 SSP 和评估结果文档中。 ## 安全集群 该网关跨越两个引擎涵盖九个安全集群。 ### 确定性集群（Lean 4 内核） | 集群 | 不变量 | 控制 | |---------|-----------|----------| | **身份与访问** | 特权会话需要防钓鱼 MFA；token ≤ 60 分钟 | AC-2, AC-3, AC-6, IA-2, IA-5 | | **加密保护** | 联邦数据使用 FIPS-140-3 模块静态加密 | SC-8, SC-12, SC-13, SC-28 | | **架构不可变性** | 仅限已签名的镜像；无 shell 访问权限；无开放的 ingress | CM-2, CM-6, CM-7, SC-7, SI-7 | | **持续监控** | 主动记录到防篡改目标；保留期 ≥ 365 天 | AU-2, AU-6, AU-9, AU-11, SI-4 | 每个不变量都表示为正式的 Lean 4 定理，并带有相应的决策过程，从而产生具体的验证结果。 ### 定性集群（Amazon Bedrock 代理） | 集群 | 分析范围 | 控制 | |---------|----------------|----------| | **人员安全** | 背景调查、NDA 验证、IAM 配置时间 | PS-1 到 PS-8 | | **网络安全教育** | 培训完成情况、重新认证窗口期 | AT-1 到 AT-4 | | **事件响应** | 时间线重建、分诊指标、联邦报告 | IR-1 到 IR-8 | | **恢复计划** | DR 演练验证、RTO/RPO 验证 | CP-1, CP-2, CP-4, CP-6, CP-7, CP-9, CP-10 | | **供应链** | SBOM 分析、CVE 上下文化、风险叙述 | SA-4, SA-5, SA-9, SA-11, SR-1, SR-2, SR-3 | 每个 Bedrock 代理从知识库中检索相关的策略文档，应用语义推理，并返回带有引用的结构化发现结果。 ## 快速开始 ### 前置条件 - Python 3.9+ - [Lean 4](https://lean-lang.org/lean4/doc/setup.html)（用于证明编译） - 带有 Bedrock 访问权限的 AWS 凭据（用于定性代理集群） ### 运行流水线（模拟模式） ``` # 克隆 repository git clone https://github.com/j-arndt/fedcloud.git cd fedcloud # 运行所有测试（Lean 4 和 Bedrock agent 套件中总计 64 个） python -m pytest translator/tests/ oscal/tests/ agents/tests/ -v # 针对 mock fixtures 执行完整 pipeline python -m scripts.run_pipeline --mode mock --state fixtures/mock_aws_topology.json # 查看 output artifacts ls output/ # → SystemState.lean verification_receipt.json fedcloud_ssp.json assessment_results.json ``` ### 构建 Lean 4 验证引擎 ``` cd lean # 通过 elan 安装 Lean curl https://elan.lean-lang.org/install/linux -sSf | sh # 构建 verification library lake build # 针对 sample states 运行 proof checker lean FedCloud/Verify.lean ``` ### Docker ``` docker build -t fedcloud-gateway . docker run -v $(pwd)/fixtures:/data fedcloud-gateway /data/mock_aws_topology.json ``` ## 项目结构 ``` fedcloud/ ├── lean/ # Lean 4 formal verification engine │ ├── lakefile.lean # Lake build configuration │ ├── lean-toolchain # Lean version pin (v4.28.0) │ └── FedCloud/ │ ├── BaseModel.lean # Core type definitions │ ├── Verify.lean # Orchestrator + sample states │ └── Invariants/ │ ├── Identity.lean # IAM cluster invariant │ ├── Crypto.lean # Cryptographic protection invariant │ ├── Architecture.lean # Immutability invariant │ └── Monitoring.lean # Continuous monitoring invariant ├── agents/ # Bedrock qualitative verification engine │ ├── base_agent.py # Shared agent with RAG + citations │ ├── config.py # Bedrock model and routing config │ ├── router.py # Deterministic vs qualitative router │ ├── lambda_handler.py # AWS Lambda entry point │ ├── guardrails.py # Output validation and hallucination checks │ ├── knowledge_base.py # RAG policy document retrieval │ ├── clusters/ │ │ ├── personnel.py # KSI-PS agent │ │ ├── training.py # KSI-CED agent │ │ ├── incident_response.py # KSI-INR agent │ │ ├── recovery.py # KSI-RPL agent │ │ └── supply_chain.py # KSI-TPR agent │ └── tests/ │ └── test_agents.py # Agent unit tests ├── translator/ # JSON → Lean translation layer │ ├── json_to_lean.py # Multi-format state translator │ ├── state_ingestion.py # State collection service │ └── tests/ │ └── test_translator.py # Translator unit tests ├── oscal/ # OSCAL synthesis pipeline │ ├── receipt_generator.py # Signed verification receipts │ ├── ssp_updater.py # SSP component injection │ ├── assessment_results.py # OSCAL Assessment Results │ ├── templates/ │ │ └── fedramp_moderate_ssp.json # Baseline SSP template │ └── tests/ │ └── test_pipeline.py # Pipeline integration tests ├── fixtures/ # Mock telemetry data │ ├── mock_aws_topology.json # Sample AWS infrastructure state │ ├── mock_terraform_plan.json # Sample Terraform plan │ └── mock_tyler_app_schema.json # Sample application metadata ├── scripts/ │ └── run_pipeline.py # Pipeline orchestrator ├── docs/ # HTML documentation ├── .github/workflows/ci.yml # GitHub Actions CI ├── Dockerfile # Container build └── README.md ``` ## 工作原理 ### 1. 状态摄取 基础架构状态是从 AWS Config、CloudTrail、EventBridge 和应用程序 API 收集的。在 PoC 模式下，由模拟夹具模拟这些来源。 ### 2. 转换 `json_to_lean.py` 转换器将 JSON 负载转换为带类型的 Lean 4 定义。它处理多种输入格式（原始状态、Terraform plan、应用程序 schema），并将它们标准化为 `SystemState` 结构。 ### 3. 形式化验证 Lean 4 内核将转换后的状态与不变量定理库一起编译。如果所有证明都成立，则系统在数学上得到验证。如果任何不变量失败，则会识别出具体的违规情况。 ### 4. 凭证生成 加密签名 (HMAC-SHA256) 的 JSON 凭证会捕获验证结果、输入状态哈希、时间戳以及每个集群的状态。 ### 5. OSCAL 综合 该凭证被注入到 OSCAL SSP 中，并使用验证元数据更新组件定义。系统将生成一份单独的 OSCAL 评估结果文档，其中包含映射到各控制系列的发现结果。 ## 验证保证 与基于扫描的合规工具不同，该系统提供： - **确定性**：相同的输入始终产生相同的验证结果 - **完整性**：范围内的每个资源都会针对每个适用的不变量进行检查 - **防篡改证据**：凭证使用输入状态哈希进行加密签名 - **可审计性**：Lean 4 证明逻辑可供第三方检查和验证 ## 许可证 MIT
标签：AWS, DPI, Lean 4, OSCAL, 云计算, 合规自动化, 形式化验证, 规则引擎, 请求拦截, 逆向工具