Bajuzjefe/Aikido-Security-Analysis-Platform
GitHub: Bajuzjefe/Aikido-Security-Analysis-Platform
针对 Cardano 链上 Aiken 智能合约的多轨道安全分析平台，结合 75 个检测器、SMT 验证与交易模拟，在合约部署前自动发现漏洞。
Stars: 1 | Forks: 0
**针对 Cardano 上 [Aiken](https://aiken-lang.org/) 智能合约的安全分析平台。**
Aikido 不仅仅局限于静态分析。它结合了包含 75 个检测器的套件与 SMT 验证、交易模拟、合规性分析、协议模式检测以及语法感知的模糊测试，旨在 Aiken 智能合约上线主网之前发现漏洞。多轨道分析交叉关联各项技术产生的证据，生成包含源码上下文、严重等级、CWE/CWC 分类以及可操作修复建议的发现报告。
使用 Rust 构建。速度快。零配置。
## 为什么选择 Aikido
Cardano 智能合约一旦部署即不可变。生产环境中的漏洞意味着资金损失且无法追回。人工审计成本高昂、速度慢，且存在瓶颈。Aikido 可以在几秒钟内自动捕捉审计师最常发现的几类漏洞 —— 双重满足、缺失签名检查、无界迭代、不安全的 datum 处理 等。
- **唯一针对 Aiken 的安全工具** - 生态系统中尚无替代方案
- **75 个检测器** - 包含 CWC (Cardano Weakness Classification) 和 CWE 映射
- **多轨道分析** - 静态检测器、合规性、SMT 验证、交易模拟、协议检测、模糊测试
- **经专业审计验证** - 对 TxPipe 的 Strike Finance 审计发现覆盖率达 85% ([完整对比](AUDIT_COMPARISON.md))
- **证据框架** - 发现结果经多种分析技术确证 (PatternMatch -> SmtProven -> SimulationConfirmed)
- **9 种输出格式** - terminal, JSON, SARIF, Markdown, HTML, PDF, CSV, GitLab SAST, reviewdog
- **生态验证** - 10+ 个真实项目，包括 SundaeSwap, Anastasia Labs, Strike Finance, 以及 Seedelf (0 崩溃)
## 快速开始
### 安装
```
# Homebrew (macOS/Linux)
brew install Bajuzjefe/tap/aikido
# Cargo (Rust >= 1.88.0)
cargo install --git https://github.com/Bajuzjefe/Aikido-Security-Analysis-Platform aikido-cli
# npm (wrapper)
npx aikido-aiken /path/to/project
# Docker
docker run --rm -v $(pwd):/project ghcr.io/bajuzjefe/aikido:0.3.1 /project
# 从源代码构建
git clone https://github.com/Bajuzjefe/Aikido-Security-Analysis-Platform.git
cd aikido && cargo build --release
```
### 运行
```
aikido /path/to/your-aiken-project
```
### 示例输出
```
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
AIKIDO v0.3.1 Static Analysis Report
Project: test/simple-treasury v0.1.0
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
[CRITICAL] (definite) double-satisfaction - Handler treasury.spend iterates
outputs without own OutputReference - validators/treasury.ak:23
Spend handler accesses tx.outputs but never uses __own_ref to identify
its own input. An attacker can satisfy multiple script inputs with a
single output, draining funds.
22 | validator treasury {
> 23 | spend(
> 24 | datum: Option
,
> 25 | redeemer: TreasuryRedeemer,
Suggestion: Use the OutputReference parameter to correlate outputs
to this specific input.
...
1 critical, 5 high, 7 medium, 0 low, 0 info
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
```
## 分析架构
Aikido 采用多轨道方法，其中独立的分析技术相互交叉验证：
```
graph TB
subgraph Input
A[Aiken Project] --> B[Typed AST]
end
subgraph Analysis Lanes
B --> C[Detector Suite
75 detectors]
B --> D[Compliance
Securify2-style]
B --> E[SMT Verification
Cardano axioms]
B --> F[Tx Simulation
exploit generation]
B --> G[Protocol Detection
DeFi classification]
B --> H[Fuzz Lane
grammar-aware]
end
subgraph Evidence Correlation
C --> I[Evidence Framework]
D --> I
E --> I
F --> I
G --> I
H --> I
end
I --> J[PatternMatch]
J --> K[PathVerified]
K --> L[SmtProven]
L --> M[SimulationConfirmed]
M --> N[Corroborated]
N --> O[Report
9 output formats]
style C fill:#2EFFB5,color:#0a0a0a
style D fill:#2EFFB5,color:#0a0a0a
style E fill:#2EFFB5,color:#0a0a0a
style F fill:#2EFFB5,color:#0a0a0a
style G fill:#2EFFB5,color:#0a0a0a
style H fill:#2EFFB5,color:#0a0a0a
style I fill:#111111,color:#e0e0e0
style O fill:#111111,color:#e0e0e0
```
### 轨道详情
| 轨道 | 功能 |
|------|-------------|
| **检测器套件** | 跨模块过程间分析、污点追踪、符号执行、感知委托的抑制、传递信号合并、datum 连续性追踪 |
| **合规性** | Securify2 风格的双模式系统：每个安全属性都有合规（安全）和违规（不安全）模式。10 种安全属性变体 |
| **SMT 验证** | 独立于求解器的接口，包含 Cardano 领域公理（价值守恒、签名语义、铸造策略）。可达性的约束求解 |
| **Tx 模拟** | ScriptContext 构建器生成具体的利用场景。针对模拟交易测试 6 类检测器 |
| **协议检测** | 自动 DeFi 协议分类（DEX, Lending, Staking, DAO, NFT, Options, Escrow）。Token 流向和权限分析 |
| **Fuzz 轨道** | 语法感知的 Cardano 交易生成，Echidna 风格的有状态协议模糊测试，确定性 PRNG |
支持模块：**CWC 注册表**（30 个条目映射所有 75 个检测器），**记分卡**（Experimental -> Beta -> Stable 晋升及质量门控），**SSA IR**（phi 节点、支配树、使用-定义链）。
## 真实世界验证
### Strike Finance 审计对比
Aikido 以 TxPipe 对 Strike Finance（永续合约 + 远期合约）的专业审计为基准进行了测试：
| 指标 | 结果 |
|--------|--------|
| TxPipe 安全发现分析数 | 24 |
| 完全匹配（真阳性） | 12 |
| 部分匹配 | 5 |
| 正确未标记（代码已修复） | 4 |
| 假阴性 | 3 |
| Aikido 独特发现 | 26 |
| **覆盖率（未修复发现）** | **85%** |
完整方法论及各项发现细分：**[AUDIT_COMPARISON.md](AUDIT_COMPARISON.md)**
### 生态验证
针对 **10+ 个真实世界 Aiken 智能合约项目**进行了验证，**零崩溃**：
| 项目 | 发现数 | 严重程度分布 |
|---------|----------|-----------------------|
| SundaeSwap DEX | 47 | 1 critical, 13 high, 24 medium, 3 low, 6 info |
| Anastasia Design Patterns | 24 | 3 critical, 10 high, 8 medium, 2 low, 1 info |
| Anastasia Multisig | 6 | 2 critical, 4 medium |
| Seedelf Wallet | 4 | 1 high, 2 medium, 1 low |
| Strike Finance (4 repos) | 75 | 5 critical, 18 high, 40 medium, 8 low, 4 info |
| Acca | 20 | 20 medium |
| **总计** | **176** | **81% estimated true positive rate** |
## 检测器
75 个映射到 CWE 标识符的检测器。
Critical (5)
| 检测器 | CWE | 描述 |
|----------|-----|-------------|
| `double-satisfaction` | CWE-362 | Spend handler 迭代输出但未引用自身输入 |
| `missing-minting-policy-check` | CWE-862 | Mint handler 未验证铸造了哪些 token 名称 |
| `missing-utxo-authentication` | CWE-345 | 引用输入未经身份验证即被使用 |
| `unrestricted-minting` | CWE-862 | 铸造策略完全没有授权检查 |
| `output-address-not-validated` | CWE-20 | 输出发送到未检查的地址 |
High (19)
| 检测器 | CWE | 描述 |
|----------|-----|-------------|
| `missing-redeemer-validation` | CWE-20 | Catch-all redeemer 模式直接返回 True |
| `missing-signature-check` | CWE-862 | Authority datum 字段没有 `extra_signatories` 检查 |
| `unsafe-datum-deconstruction` | CWE-252 | Option datum 未使用 `expect Some` 安全解构 |
| `missing-datum-in-script-output` | CWE-404 | Script 输出没有附加 datum（资金被永久锁定）|
| `arbitrary-datum-in-output` | CWE-20 | 生成输出时未验证 datum 正确性 |
| `division-by-zero-risk` | CWE-369 | 除法运算的分母受攻击者控制 |
| `token-name-not-validated` | CWE-20 | 铸造策略检查了授权但未检查 token 名称 |
| `value-not-preserved` | CWE-682 | Spend handler 未验证 output value >= input value |
| `unsafe-match-comparison` | CWE-697 | 使用 match 而非结构相等性进行值比较 |
| `integer-underflow-risk` | CWE-191 | 对 redeemer 控制的值进行减法运算 |
| `quantity-of-double-counting` | CWE-682 | Token 数量检查未隔离输入与输出 |
| `state-transition-integrity` | CWE-20 | Redeemer 操作没有 datum 转换验证 |
| `withdraw-zero-trick` | CWE-863 | Withdraw handler 可被零值提取利用 |
| `other-token-minting` | CWE-862 | 铸造策略允许铸造预期范围之外的 token |
| `unsafe-redeemer-arithmetic` | CWE-682 | 对 redeemer 污染的值进行无边界算术运算 |
| `value-preservation-gap` | CWE-682 | Lovelace 已检查但原生资产未保留 |
| `uncoordinated-multi-validator` | CWE-362 | 多 handler validator 缺乏跨 handler 协调 |
| `missing-burn-verification` | CWE-862 | Token 销毁未进行适当验证 |
| `oracle-manipulation-risk` | CWE-20 | Oracle 数据使用时缺乏防篡改保障 |
Medium (24)
| 检测器 | CWE | 描述 |
|----------|-----|-------------|
| `missing-validity-range` | CWE-613 | 时间敏感的 datum 没有 validity_range 检查 |
| `insufficient-staking-control` | CWE-863 | 输出未约束 staking credential |
| `unbounded-datum-size` | CWE-400 | Datum 字段具有无界类型 (List, ByteArray) |
| `unbounded-value-size` | CWE-400 | 输出未约束原生资产数量 |
| `unbounded-list-iteration` | CWE-400 | 直接迭代原始交易列表字段 |
| `oracle-freshness-not-checked` | CWE-613 | Oracle 数据使用时未验证新鲜度 |
| `non-exhaustive-redeemer` | CWE-478 | Redeemer match 未覆盖所有构造器 |
| `hardcoded-addresses` | CWE-798 | 匹配 Cardano 地址长度的 ByteArray 字面量 |
| `utxo-contention-risk` | CWE-400 | 单一全局 UTXO 争用模式 |
| `cheap-spam-vulnerability` | CWE-770 | Validator 易受低成本 UTXO 垃圾攻击 |
| `unsafe-partial-pattern` | CWE-252 | 在可能运行时失败的非 Option 类型上使用 Expect 模式 |
| `unconstrained-recursion` | CWE-674 | 自递归 handler 无明确终止条件 |
| `empty-handler-body` | CWE-561 | Handler 无有意义逻辑 |
| `unsafe-list-head` | CWE-129 | `list.head()` / `list.at()` 无长度保护 |
| `missing-datum-field-validation` | CWE-20 | Spend handler 接受 datum 字段但从未验证 |
| `missing-token-burn` | CWE-862 | 铸造策略无销毁处理 |
| `missing-state-update` | CWE-665 | 状态机无 datum 更新 |
| `rounding-error-risk` | CWE-682 | 对金融值进行整数除法 |
| `missing-input-credential-check` | CWE-862 | 输入迭代无凭证检查 |
| `duplicate-asset-name-risk` | CWE-694 | 铸造时未强制执行唯一资产名 |
| `fee-calculation-unchecked` | CWE-682 | 费用或协议支付未经验证 |
| `datum-tampering-risk` | CWE-20 | Datum 传递时未进行字段级验证 |
| `missing-protocol-token` | CWE-862 | 状态转换无 protocol token 验证 |
| `unbounded-protocol-operations` | CWE-400 | 输入和输出列表均无边界迭代 |
Low / Info (12)
| 检测器 | 严重程度 | 描述 |
|----------|----------|-------------|
| `reference-script-injection` | Low | 输出未约束 reference_script 字段 |
| `unused-validator-parameter` | Low | Validator 参数从未被引用 |
| `fail-only-redeemer-branch` | Low | Redeemer 分支总是失败 |
| `missing-min-ada-check` | Info | Script 输出无最低 ADA 检查 |
| `dead-code-path` | Low | 不可达代码路径 |
| `redundant-check` | Low | 琐碎的真值条件 |
| `shadowed-variable` | Info | Handler 参数被模式绑定遮蔽 |
| `magic-numbers` | Info | 未解释的数字字面量 |
| `excessive-validator-params` | Info | Validator 参数过多 |
| `unused-import` | Info | 导入的模块无函数调用 |
每个检测器都有详细的文档，包含漏洞示例、安全示例和修复指南。使用 `aikido --explain ` 或查看 `docs/detectors/`。
## 输出格式
支持 9 种格式以适应不同工作流：
```
aikido /path/to/project # Colored terminal output (default)
aikido /path/to/project --format json # JSON (machine-readable)
aikido /path/to/project --format sarif # SARIF v2.1.0 (GitHub Code Scanning)
aikido /path/to/project --format markdown # Markdown report
aikido /path/to/project --format html # Standalone HTML report
aikido /path/to/project --format pdf # PDF audit report
aikido /path/to/project --format csv # CSV export
aikido /path/to/project --format gitlab-sast # GitLab SAST
aikido /path/to/project --format rdjson # reviewdog
```
## 配置
### `.aikido.toml`
```
# 使用 preset 作为起点
extends = "strict" # or "lenient" for fewer warnings
[detectors]
disable = ["magic-numbers", "unused-import"]
[detectors.severity_override]
unbounded-datum-size = "low"
# 按文件覆盖
[[files]]
pattern = "tests/**"
disable = ["hardcoded-addresses", "magic-numbers"]
```
### 内联抑制
```
// aikido:ignore[double-satisfaction] -- false positive: own_ref checked in helper
spend(datum, redeemer, own_ref, tx) {
...
}
```
### 基线支持
```
aikido /path --accept-baseline # Save current findings as baseline
aikido /path # Only new findings reported
```
## CI/CD 集成
### GitHub Actions
```
name: Security
on: [push, pull_request]
jobs:
aikido:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Install Aikido
run: cargo install --git https://github.com/Bajuzjefe/Aikido-Security-Analysis-Platform aikido-cli
- name: Run analysis
run: aikido . --format sarif --fail-on high > results.sarif
- name: Upload SARIF
if: always()
uses: github/codeql-action/upload-sarif@v3
with:
sarif_file: results.sarif
```
### Docker
```
docker run --rm -v $(pwd):/project ghcr.io/bajuzjefe/aikido:0.3.1 /project --format json
```
## CLI 参考
```
aikido /path # Analyze project
aikido /path --fail-on high # Exit non-zero for high+ findings
aikido /path --min-severity medium # Filter to medium+ only
aikido /path --verbose # Include UPLC metrics and budget
aikido /path --list-rules # Show all detectors
aikido /path --explain # Detailed explanation with examples
aikido /path --diff main # Only report findings in changed files
aikido /path --watch # Re-run on file changes
aikido /path -q # Quiet mode
aikido /path --config my.toml # Use specific config file
aikido /path --accept-baseline # Save current findings as baseline
aikido /path --lsp # LSP JSON-RPC diagnostics
aikido /path --interactive # Terminal navigator for findings
aikido /path --fix # Insert suppression comments
aikido /path --generate-config # Generate .aikido.toml from findings
aikido /path --strict-stdlib # Reject stdlib v1.x (default: warn)
aikido --git # Clone and analyze remote repo
aikido --benchmark-manifest benchmarks/local-fixtures.toml --format json
aikido --benchmark-manifest benchmarks/local-fixtures.toml --benchmark-enforce-gates
```
## 架构
```
aikido/
├── crates/
│ ├── aikido-core/ # Library: analysis engine
│ │ ├── src/
│ │ │ ├── project.rs # Aiken project loading & compilation
│ │ │ ├── ast_walker.rs # Typed AST traversal -> ModuleInfo
│ │ │ ├── body_analysis.rs # Handler body signal extraction + taint tracking
│ │ │ ├── call_graph.rs # Function dependency graph
│ │ │ ├── cross_module.rs # Cross-module interprocedural analysis
│ │ │ ├── symbolic.rs # Symbolic execution & constraints
│ │ │ ├── delegation.rs # Delegation-aware suppression
│ │ │ ├── evidence.rs # 5-level evidence framework
│ │ │ ├── cwc.rs # Cardano Weakness Classification registry
│ │ │ ├── scorecard.rs # Detector quality tracking & promotion
│ │ │ ├── ssa.rs # SSA IR with phi nodes & use-def chains
│ │ │ ├── compliance.rs # Securify2-style compliance analysis
│ │ │ ├── smt.rs # SMT verification with Cardano axioms
│ │ │ ├── path_analysis.rs # Path-sensitive analysis & CFG
│ │ │ ├── invariant_spec.rs # .aikido-invariants.toml DSL
│ │ │ ├── protocol_patterns.rs # DeFi protocol detection & classification
│ │ │ ├── tx_simulation.rs # ScriptContext builder & exploit generation
│ │ │ ├── fuzz_lane.rs # Grammar-aware tx fuzzing
│ │ │ ├── config.rs # .aikido.toml configuration
│ │ │ ├── suppression.rs # Inline suppression comments
│ │ │ ├── baseline.rs # Baseline file support
│ │ │ ├── uplc_analysis.rs # UPLC bytecode analysis & budgets
│ │ │ └── detector/ # 75 detector implementations
│ │ └── tests/ # 1186+ tests
│ └── aikido-cli/ # Binary: clap-based CLI
├── fixtures/ # Test contracts (7 fixtures)
├── audits/ # Audit comparison artifacts
├── docs/detectors/ # Per-detector documentation
├── .github/workflows/ # CI, cross-platform, release, fuzz
├── homebrew/ # Homebrew formula
├── npm/ # npm wrapper package
├── vscode-extension/ # VS Code extension
├── fuzz/ # cargo-fuzz targets
└── Dockerfile # Multi-stage build
```
### 从源码构建
```
git clone https://github.com/Bajuzjefe/Aikido-Security-Analysis-Platform.git
cd aikido
cargo build --release # Binary at target/release/aikido
cargo test # Run test suite (1186+ tests)
cargo clippy --all-targets # Lint (zero warnings)
```
需要 Rust >= 1.88.0。
## 漏洞覆盖
检测器源自已发表的 Cardano 智能合约审计中发现的真实漏洞：
| 来源 | 覆盖的发现 |
|--------|-----------------|
| MLabs 审计报告 | Double satisfaction, missing minting policy, arbitrary datum, unbounded size |
| Vacuumlabs 审计报告 | Unbounded value size, token dust attacks |
| [Plutonomicon](https://github.com/Plutonomicon/plutonomicon) | Unrestricted minting, double satisfaction patterns |
| Anastasia Labs 审计报告 | Staking credential theft, datum handling |
| Tx 审计报告 | Oracle manipulation, state transition integrity, value preservation |
| CWE 数据库 | 75 个检测器映射到特定 CWE 标识符 |
## 许可证
MIT
标签：Ada, Aiken, Cardano, CWC, GraphQL安全矩阵, Homebrew安装, Rust, SMT验证, TLS, UTXO模型, Web3安全, XSS注入, 云安全监控, 交易模拟, 区块链安全, 协议检测, 双重支付, 可视化界面, 合规分析, 多模态安全, 安全扫描器, 形式化验证, 文档结构分析, 智能合约安全, 暗色界面, 签名检查, 网络流量审计, 自动审计, 请求拦截, 通知系统, 通知系统, 通知系统, 防御加固, 防御工具, 静态分析