hira299/sentinel-mesh
GitHub: hira299/sentinel-mesh
神经符号框架，结合LLM与Z3 SMT形式化验证实现云基础设施配置错误的自动闭环修复。
Stars: 0 | Forks: 0
# Sentinel-Mesh
神经符号框架，用于自动修复云基础设施配置错误。将 LLM 驱动的补丁生成与 Z3 SMT 形式化验证结合在闭环反馈中。
### 技术资源
要深入了解 Cloud Perimeter Model 和本框架中使用的 SMT 逻辑，请阅读 Medium 上的文章：
**[超越启发式：使用 Z3 SMT 求解器形式化验证 AI 生成的基础设施](https://medium.com/@hira229922/beyond-heuristics-formally-verifying-ai-generated-infrastructure-with-z3-smt-solvers-e95fd3a7bf95)**
## 工作原理
1. 检测到 Terraform 配置错误并传递给 LLM 代理
2. 代理生成修复补丁
3. Z3 验证器根据形式化安全不变量（Cloud Perimeter Model）检查补丁
4. 如果补丁验证失败，Z3 错误消息将反馈给 LLM 并重试循环
5. 一旦补丁满足所有不变量，即被接受。对于加密和网络违规问题，还通过双求解器 Z3 细化（求解器 A 用于完整性，求解器 B 用于正确性）颁发形式化证明证书 — 基准测试中 37/88 个修复案例获得了证书
验证器充当闭环接受 oracle。LLM 无法在不满足形式化约束的情况下生成通过验证的补丁。
## 基准测试结果
在 8 个云基础设施领域的 105 个手工制作的 Terraform 配置错误基准案例上进行了评估。
| 指标 | 结果 |
|---|---|
| 总体修复率 | 88/105 (83.81%) |
| 单次解决率 | 85.23% (75/88 在 k=1 时) |
| 颁发的形式化证明证书 | 37 (29 个 FPC + 8 个 PATCH REJECTED) |
| LLM 幻觉率 | 16.19% (17/105) |
| 阻止的幻觉补丁 | 17/17（0% 回退率） |
| 每个修复案例的平均尝试次数 | μ=1.27，σ=0.74 |
### 按领域分类
| 领域 | 案例数 | 修复数 | 率 |
|---|---|---|---|
| Identity | 9 | 9 | 100% |
| Management | 6 | 6 | 100% |
| Database | 17 | 16 | 94.1% |
| Networking | 15 | 14 | 93.3% |
| Security | 12 | 11 | 91.7% |
| Compute | 23 | 17 | 73.9% |
| Analytics | 13 | 9 | 69.2% |
| Storage | 10 | 6 | 60.0% |
## 设置
```
git clone https://github.com/hira299/sentinel-mesh
cd sentinel-mesh
make install
```
将 `.env.example` 复制到 `.env` 并添加您的 API 密钥：
```
CEREBRAS_API_KEY=...
GEMINI_API_KEY=...
GROQ_API_KEY=...
```
## 使用方法
```
# Run full benchmark
make benchmark
# Generate result figures
make visualize
# Single file run
make run
```
结果写入 `logs/research_data_v100.csv`。图表保存到 `logs/`。
## 项目结构
```
sentinel-mesh/
├── benchmark/
│ └── test_cases/ # 105 Terraform misconfiguration test cases
├── core/
│ ├── verifier.py # Z3 SMT verifier and Cloud Perimeter Model (2,591 lines)
│ ├── orchestrator.py # closed-loop remediation orchestrator (MAX_RETRIES=3)
│ └── llm_agent.py # LLM patch generation agent (Cerebras/Gemini/Groq rotation)
├── parsers/
│ └── hcl_to_json.py # Terraform HCL parser
├── experiment_runner.py # batch benchmark runner (uses k=5 retries)
├── visualizer.py # result figure generation
├── logs/ # generated outputs (gitignored)
├── Makefile
└── requirements.txt
```
## 依赖项
- Python 3.10+
- z3-solver
- python-hcl2
- matplotlib
- cerebras-cloud-sdk
- 完整列表请参见 `requirements.txt`
## 引用
如果您使用此工作，请引用：
```
@misc{sentinelmesh2026,
title = {Sentinel-Mesh: Neuro-Symbolic Autonomous Remediation of Cloud Misconfigurations},
author = {Hira Ahmed},
year = {2026},
url = {https://github.com/hira299/sentinel-mesh}
}
```
## 许可证
MIT
| 指标 | 结果 |
|---|---|
| 总体修复率 | 88/105 (83.81%) |
| 单次解决率 | 85.23% (75/88 在 k=1 时) |
| 颁发的形式化证明证书 | 37 (29 个 FPC + 8 个 PATCH REJECTED) |
| LLM 幻觉率 | 16.19% (17/105) |
| 阻止的幻觉补丁 | 17/17（0% 回退率） |
| 每个修复案例的平均尝试次数 | μ=1.27，σ=0.74 |
### 按领域分类
| 领域 | 案例数 | 修复数 | 率 |
|---|---|---|---|
| Identity | 9 | 9 | 100% |
| Management | 6 | 6 | 100% |
| Database | 17 | 16 | 94.1% |
| Networking | 15 | 14 | 93.3% |
| Security | 12 | 11 | 91.7% |
| Compute | 23 | 17 | 73.9% |
| Analytics | 13 | 9 | 69.2% |
| Storage | 10 | 6 | 60.0% |
## 设置
```
git clone https://github.com/hira299/sentinel-mesh
cd sentinel-mesh
make install
```
将 `.env.example` 复制到 `.env` 并添加您的 API 密钥：
```
CEREBRAS_API_KEY=...
GEMINI_API_KEY=...
GROQ_API_KEY=...
```
## 使用方法
```
# Run full benchmark
make benchmark
# Generate result figures
make visualize
# Single file run
make run
```
结果写入 `logs/research_data_v100.csv`。图表保存到 `logs/`。
## 项目结构
```
sentinel-mesh/
├── benchmark/
│ └── test_cases/ # 105 Terraform misconfiguration test cases
├── core/
│ ├── verifier.py # Z3 SMT verifier and Cloud Perimeter Model (2,591 lines)
│ ├── orchestrator.py # closed-loop remediation orchestrator (MAX_RETRIES=3)
│ └── llm_agent.py # LLM patch generation agent (Cerebras/Gemini/Groq rotation)
├── parsers/
│ └── hcl_to_json.py # Terraform HCL parser
├── experiment_runner.py # batch benchmark runner (uses k=5 retries)
├── visualizer.py # result figure generation
├── logs/ # generated outputs (gitignored)
├── Makefile
└── requirements.txt
```
## 依赖项
- Python 3.10+
- z3-solver
- python-hcl2
- matplotlib
- cerebras-cloud-sdk
- 完整列表请参见 `requirements.txt`
## 引用
如果您使用此工作，请引用：
```
@misc{sentinelmesh2026,
title = {Sentinel-Mesh: Neuro-Symbolic Autonomous Remediation of Cloud Misconfigurations},
author = {Hira Ahmed},
year = {2026},
url = {https://github.com/hira299/sentinel-mesh}
}
```
## 许可证
MIT标签：C2, CloudPerimeterModel, DLL 劫持, EC2, ECS, IaC, LLM, SMT求解器, Sysdig, Terraform, Unmanaged PE, Vagrant, Z3, 云基础设施, 双求解器验证, 反馈循环, 合规检测, 大语言模型, 安全不变量, 形式化方法, 形式化验证, 神经符号AI, 自动修复, 自动化运维, 证明证书, 逆向工具, 配置修复, 错误修复