Static Analysis for Memory Safety and Security
Frame 是一款由**分离逻辑**驱动的静态分析工具，能够以极高的精度发现安全漏洞和内存安全 bug。它支持 **5 种语言**并达到了 **80%+ 的 OWASP 得分**——显著优于 Semgrep 和 Bandit 等工具。
## 核心亮点
**OWASP 得分**（True Positive Rate - False Positive Rate）：
| Benchmark | Frame | Semgrep | 差异 |
|-----------|:---:|:---:|:---:|
| **Python** (OWASP) | 80.9% | 4.5% | +76.4 pts |
| **Java** (OWASP) | 81.5% | 15.7% | +65.8 pts |
| **JavaScript** (SecBench.js) | 43.0% | 10.0% | +33 pts |
| **C/C++** (NIST Juliet) | 54.4% | -14.9% | +69.3 pts |
| **C#** (IssueBlot.NET) | 80.3% | 14.2% | +66.1 pts |
分数越高越好。有关详细的方法和结果，请参阅 [benchmarks/](benchmarks/)。
## 安装说明
```
git clone https://github.com/lambdasec/frame.git
cd frame
pip install -e ".[scan]"
```
## 快速开始
```
# 扫描漏洞
frame scan app.py
# 扫描目录
frame scan src/ --pattern "**/*.py"
# CI/CD 集成（SARIF 输出）
frame scan src/ --format sarif -o results.sarif --fail-on high
```
更多示例
```
# 检查 separation logic 蕴含
frame solve "x |-> 5 * y |-> 3 |- x |-> 5"
# 批量检查公式
frame check formulas.txt
# 交互模式
frame repl
```
## 支持的语言
| 语言 | 框架与库 |
|----------|----------------------|
| **Python** | Flask, Django, FastAPI, SQLAlchemy, subprocess |
| **Java** | Spring, JDBC, Hibernate, JNDI |
| **JavaScript/TypeScript** | Express, Node.js, DOM API |
| **C/C++** | POSIX, Windows API, 内存操作 |
| **C#** | ASP.NET, Entity Framework, ADO.NET |
## Frame 的检测范围
|
**注入与 XSS**
- SQL 注入 (CWE-89)
- 跨站脚本攻击 (CWE-79)
- 命令注入 (CWE-78)
- LDAP/XPath 注入
- 模板注入
|
**内存安全**
- 缓冲区溢出 (CWE-121/122)
- 释放后使用 (CWE-416)
- 重复释放 (CWE-415)
- 空指针解引用
- 整数溢出
|
|
**数据暴露**
- 路径遍历 (CWE-22)
- SSRF (CWE-918)
- 开放重定向 (CWE-601)
- 硬编码密钥
- 日志注入
|
**密码学**
- 弱算法 (CWE-327)
- 不安全的随机数 (CWE-330)
- 弱哈希 (CWE-328)
- 不安全的反序列化
|
## 工作原理
Frame 采用了一种将**污点分析**与**分离逻辑验证**相结合的独特方法：
```
Source Code
|
v
[Language Frontend] ---> SIL (Separation Intermediate Language)
| |
v v
[Taint Tracking] [Symbolic Execution]
| |
v v
[Pattern Detection] <---> [Z3 Verification]
|
v
Vulnerability Report
```
**为什么这很重要：**
- **污点分析**追踪从来源（用户输入）到汇聚点（SQL 查询）的不可信数据流
- **分离逻辑**正式验证内存安全属性
- **Z3 验证**通过证明漏洞的可达性来消除误报
## CI/CD 集成
```
# GitHub Actions
- name: Install Frame
run: pip install -e ".[scan]"
- name: Security Scan
run: frame scan src/ --format sarif -o results.sarif --fail-on high
- name: Upload Results
uses: github/codeql-action/upload-sarif@v2
with:
sarif_file: results.sarif
```
## Python API
```
from frame import EntailmentChecker
from frame.sil import FrameScanner
# 安全扫描
scanner = FrameScanner()
result = scanner.scan_file("app.py")
for vuln in result.vulnerabilities:
print(f"{vuln.cwe_id}: {vuln.description}")
# separation logic 验证
checker = EntailmentChecker()
result = checker.check_entailment("x |-> 5 * y |-> 3 |- x |-> 5")
print(result.valid) # True
```
## 分离逻辑求解器
Frame 包含一个用于验证堆属性的分离逻辑求解器：
| 语法 | 含义 |
|--------|---------|
| `x \|-> v` | x 指向值 v |
| `emp` | 空堆 |
| `P * Q` | P 和 Q 位于独立内存中 |
| `P -* Q` | 魔法棒 |
| `P \|- Q` | P 蕴含 Q |
**内置谓词：** `ls(x,y)`（链表段）、`list(x)`、`tree(x)`、`dll(x,p,y,n)`
```
frame solve "ls(x, y) * ls(y, z) |- ls(x, z)" # List transitivity
```
## 基准测试
Frame 已通过业界标准的基准测试套件验证：
| Benchmark | 领域 | 测试数 | 精确率 | 召回率 |
|-----------|--------|-------|-----------|--------|
| OWASP Python | Web 安全 | 500 | 95.3% | 83.5% |
| OWASP Java | Web 安全 | 500 | 97.2% | 84.8% |
| SecBench.js | Node.js 安全 | 300 | 82.0% | 81.0% |
| NIST Juliet | C/C++ 内存 | 1,000 | 89.9% | 60.5% |
| IssueBlot.NET | C# 安全 | 171 | 84.7% | 80.3% |
| SL-COMP | 分离逻辑 | 692 | 79.9% | - |
| SMT-LIB QF_S | 字符串理论 | 3,300 | 99.3% | - |
```
python -m benchmarks run --curated # Run all benchmarks
```
有关详细结果、方法和工具对比，请参阅 [benchmarks/README.md](benchmarks/README.md)。
## 项目结构
```
frame/
core/ # AST and parser
encoding/ # Z3 SMT encoding
checking/ # Entailment checker
sil/ # Security scanner
scanner.py # Main interface
frontends/ # Language parsers (Python, Java, JS, C, C#)
analyzers/ # Taint & memory analysis
cli.py # Command-line interface
```
## 参考文献
- Reynolds & O'Hearn (2002). [分离逻辑：用于共享可变数据结构的逻辑](https://doi.org/10.1109/LICS.2002.1029817)
- O'Hearn (2020). [非正确性逻辑](https://doi.org/10.1145/3371078)
**相关项目：** [Infer](https://fbinfer.com/), [Semgrep](https://semgrep.dev/), [CodeQL](https://codeql.github.com/)
使用 Z3 和 tree-sitter 构建