aiken-dex-security-audit

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Chinese

Auditing Plutus V3 Aiken contracts for a DEX (validators + minting policies)
You need a rigorous report: threat model, invariants, findings, and reproducible exploit tx shapes

No hallucinations. If something isn't in the repo or inputs, say unknown and list exactly what's missing.
Assume a hostile attacker can craft arbitrary transactions: multi-input, multi-action, weird datums, weird token bundles.
Never ask for or handle seed phrases / private keys.
Prefer evidence over vibes: minimal tx shape + failing test + fix + passing test.

Script list + purpose (spend/mint/reward/cert) and which are critical path for swaps/liquidity
Datum/redeemer schemas (Aiken types + encoding expectations)
Parameters/config: policy IDs, script hashes, upgrade/admin controls, oracle deps (if any)
Off-chain tx builder(s) in scope (where swaps/liquidity txs are constructed)
Network assumptions (mainnet/preprod) + constraints (tx size, exunits, reference scripts, inline datums)

Build a system model
- Map state UTxOs, assets, script addresses, and transitions (inputs/outputs/mint/burn/signees/time).
Extract explicit invariants (testable)
- Value conservation, LP supply rules, fee bounds/rounding, auth rules, "exactly-one state UTxO", bounded datum/value growth.
Threat model & attack surface
- Attacker capabilities in eUTxO; trusted roles; upgrade/emergency keys; oracles; economic/griefing vectors.
Manual on-chain review
- For each validator/policy branch: what must be true about inputs/outputs/minted/signers/time?
- Hunt: double satisfaction, fake-state UTxOs, asset-class mismatches, optional datum gotchas, unbounded growth, time-range bugs, division/rounding/negative amounts, "exactly one" enforcement bugs.
- For each issue: minimal exploitable tx shape + why it works (use tx-shapes template).
Off-chain review (if in scope)
- Ensure builder cannot construct valid-but-unsafe txs or mis-hash datums or mis-handle mint fields.
Evidence suite (Aiken-first)
- Add unit tests + property tests for each invariant + each exploit regression test.
Budget & DoS analysis
- Identify evaluation hotspots and griefing paths; recommend safe refactors.
Report
- Use
```
templates/audit-report.md
```
  and include: scope, assumptions, invariants, findings table, patches, tests, deployment checklist.

构建系统模型
- 映射状态UTxO、资产、脚本地址以及状态转换（输入/输出/铸币/销毁/签名者/时间）。
提取可测试的显式不变量
- 价值守恒、LP供应量规则、手续费上限/舍入、权限规则、“仅存在一个状态UTxO”、数据/价值增长受限。
威胁模型与攻击面
- eUTxO模型下的攻击者能力；可信角色；升级/紧急密钥；预言机；经济/恶意干扰攻击向量。
手动链上审查
- 针对每个验证器/策略分支：输入/输出/铸币/签名者/时间必须满足哪些条件？
- 排查：双重满足攻击、伪造状态UTxO、资产类别不匹配、可选数据陷阱、无限制增长、时间范围漏洞、除法/舍入/负金额问题、“仅一个”规则执行漏洞。
- 针对每个问题：提供最小可利用交易格式+漏洞原理（使用tx-shapes模板）。
链下审查（若在范围内）
- 确保交易构建器无法构造合法但不安全的交易，不会错误哈希数据或错误处理铸币字段。
证据套件（优先使用Aiken）
- 为每个不变量添加单元测试+属性测试，为每个漏洞添加回归测试。
预算与DoS分析
- 识别执行热点和恶意干扰路径；推荐安全重构方案。
生成报告
- 使用
```
templates/audit-report.md
```
  模板，内容包括：审计范围、假设条件、不变量、审计发现表格、补丁、测试、部署检查清单。