Asi move-smart-contract-audit

Comprehensive Move/Aptos smart contract security audit pipeline

install

source · Clone the upstream repo

git clone https://github.com/plurigrid/asi

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/plurigrid/asi "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/move-smart-contract-audit" ~/.claude/skills/plurigrid-asi-move-smart-contract-audit && rm -rf "$T"

manifest: skills/move-smart-contract-audit/SKILL.md

source content

Move Smart Contract Audit Skill

"Formal verification meets differential fuzzing. Every Move module audited from bytecode to specification."

Overview

Full-stack security audit pipeline for Move smart contracts on Aptos. Combines Trail of Bits audit methodology with Move-native tooling: Move Prover (formal verification), Semgrep (pattern-based detection), MoveSmith (compiler fuzzing), Belobog (contract fuzzing), mutation testing, and bytecode analysis.

GF(3) Role

Aspect	Value
Trit	-1 (MINUS)
Role	VALIDATOR
Function	Validates Move contracts through multi-layered security analysis

Architecture

┌─────────────────────────────────────────────────────────────────────┐
│                MOVE SMART CONTRACT AUDIT PIPELINE                    │
├─────────────────────────────────────────────────────────────────────┤
│                                                                     │
│  Layer 1: STATIC ANALYSIS                                          │
│  ┌──────────┐  ┌──────────┐  ┌──────────┐  ┌──────────────┐       │
│  │ Aptos    │  │ Semgrep  │  │ Context  │  │ Bytecode     │       │
│  │ Linter   │  │ Move     │  │ Builder  │  │ Disassembly  │       │
│  │ (built-  │  │ Rules    │  │ (ToB)    │  │ (movetool)   │       │
│  │  in)     │  │          │  │          │  │              │       │
│  └────┬─────┘  └────┬─────┘  └────┬─────┘  └──────┬───────┘       │
│       │              │              │               │              │
│       ▼              ▼              ▼               ▼              │
│  ┌─────────────────────────────────────────────────────────┐       │
│  │              FINDINGS AGGREGATOR (Layer 2)              │       │
│  └───────────────────────┬─────────────────────────────────┘       │
│                          │                                         │
│  Layer 3: FORMAL VERIFICATION                                      │
│  ┌──────────────────┐  ┌──────────────────┐                        │
│  │ Move Prover      │  │ Mutation Testing │                        │
│  │ (Boogie + Z3)    │  │ (move-mutator)   │                        │
│  │ - requires       │  │ - spec coverage  │                        │
│  │ - ensures        │  │ - test quality   │                        │
│  │ - invariants     │  │                  │                        │
│  └────────┬─────────┘  └────────┬─────────┘                        │
│           │                      │                                  │
│           ▼                      ▼                                  │
│  ┌─────────────────────────────────────────────────────────┐       │
│  │              VERIFICATION REPORT (Layer 4)              │       │
│  └───────────────────────┬─────────────────────────────────┘       │
│                          │                                         │
│  Layer 5: DYNAMIC ANALYSIS                                         │
│  ┌──────────────────┐  ┌──────────────────┐                        │
│  │ MoveSmith        │  │ Belobog          │                        │
│  │ (compiler fuzz)  │  │ (contract fuzz)  │                        │
│  │ - V1 vs V2       │  │ - type-guided    │                        │
│  │ - opt on/off     │  │ - concolic exec  │                        │
│  └────────┬─────────┘  └────────┬─────────┘                        │
│           │                      │                                  │
│           ▼                      ▼                                  │
│  ┌─────────────────────────────────────────────────────────┐       │
│  │              FINAL AUDIT REPORT (Layer 6)               │       │
│  │  Severity: Critical / High / Medium / Low / Info        │       │
│  │  GF(3): Conservation verified / violated                │       │
│  └─────────────────────────────────────────────────────────┘       │
│                                                                     │
└─────────────────────────────────────────────────────────────────────┘

Audit Checklist

1. Pre-Audit Context Building (Trail of Bits methodology)

□ Read entire contract line-by-line
□ Map module dependencies and friend declarations
□ Identify all entry functions (attack surface)
□ Identify all public functions (composability surface)
□ Map resource lifecycles (create → read → update → delete)
□ Map capability/permission model (signer usage, access control)
□ Identify all abort conditions and error codes
□ Check Move.toml dependencies and versions

2. Static Analysis

# Built-in Aptos linter (runs during compilation)
aptos move compile --named-addresses MODULE_ADDR=default

# Semgrep Move rules
semgrep --config ~/i/tools/semgrep-move-rules/ sources/

# Checks:
□ Signer leaks (passing signer to untrusted code)
□ friend + entry combination (privilege escalation)
□ Missing object ownership verification
□ Unsafe table::borrow / table::add
□ Public ConstructorRef return (capability leak)
□ Infinite recursion
□ Non-uniform random distribution (random % N bias)
□ Dead code / unreachable statements

3. Move-Specific Vulnerability Classes

Category	Check	Severity
Access Control	Signer validation on all entry functions	Critical
Access Control	Friend module trust boundaries	High
Resource Safety	No orphaned resources (resource leak)	High
Resource Safety	Global storage access patterns (exists/borrow/move)	High
Arithmetic	Integer overflow/underflow (Move aborts, but check logic)	Medium
Arithmetic	Division by zero guards	Medium
Randomness	On-chain randomness manipulation	Critical
Token	Royalty enforcement / bypass	Medium
Token	Token burn authority	High
Object Model	ConstructorRef / ExtendRef capability leaks	Critical
Object Model	Object ownership transfer authorization	High
Events	Missing events for state changes	Low
Upgradability	Module upgrade policy (compatible/immutable)	Medium
GF(3)	Conservation law violations	Medium
GF(3)	Trit encoding consistency (0/1/2 vs -1/0/+1)	Low

4. Formal Verification (Move Prover)

# Install prover dependencies
aptos update prover-dependencies

# Run prover on module
aptos move prove --named-addresses MODULE_ADDR=default

# Key specification patterns:
spec fun_name {
    requires condition;          // Precondition
    ensures result == expected;  // Postcondition
    aborts_if bad_condition;     // Abort condition
}

spec module {
    invariant global_property;   // Module invariant
}

5. Mutation Testing

# Install mutation tools
RUSTFLAGS="--cfg tokio_unstable" cargo install \
  --git https://github.com/eigerco/move-mutation-tools.git \
  --locked move-mutation-test

# Run mutation testing
move-mutation-test --path . --output mutations/

6. Dynamic Analysis (Fuzzing)

# MoveSmith (compiler-level)
cd ~/i/tools/move-smith
./scripts/fuzz.sh v1v2 24 32 4 3

# Belobog (contract-level, type-guided)
cd ~/i/tools/belobog
# Follow belobog setup for target contract

Known Contract Inventory

Contract	Location	Status
`swarm_bootstrap`	`asi/skills/swarm-bootstrap/sources/`	Production
`kolmogorov_codex_quest`	`asi/skills/kolmogorov-codex-quest/sources/`	Production
`bci_anchoring`	`duck/bci_contract/sources/`	Production
`vibesnipe::core`	`vibesnipe/move/sources/core.move`	Production
`vibesnipe::signature_economies`	`vibesnipe/move/sources/signature_economies.move`	Production
`vibesnipe::oracle`	`vibesnipe/move/sources/oracle.move`	Production
`vibesnipe::goblin_mesh`	`vibesnipe/move/sources/goblin_mesh.move`	Production
`vibesnipe::triadic_consensus`	`vibesnipe/move/sources/vibesnipe_triadic_consensus.move`	Production
`vibesnipe::mini_clojure`	`vibesnipe/move/sources/mini_clojure.move`	Production
`vibesnipe::sci_index`	`vibesnipe/move/sources/sci_index.move`	Production
`vibesnipe::skill_challenge`	`vibesnipe/move/sources/skill_challenge.move`	Production
`vibesnipe::merkle_integration`	`vibesnipe/move/sources/vibesnipe_merkle_integration.move`	Production

Quick Audit Commands

# Full audit pipeline (compile + lint + test)
aptos move compile --named-addresses vibesnipe=default 2>&1 | tee audit-compile.log
aptos move test --named-addresses vibesnipe=default 2>&1 | tee audit-test.log

# Semgrep scan
semgrep --config ~/i/tools/semgrep-move-rules/ sources/ 2>&1 | tee audit-semgrep.log

# Formal verification
aptos move prove --named-addresses vibesnipe=default 2>&1 | tee audit-prove.log

# Generate audit report
cat audit-*.log > AUDIT-REPORT-$(date +%Y%m%d).md

Tooling Installation

# 1. Aptos CLI (already installed: v7.14.1)
aptos --version

# 2. Move Prover dependencies (Boogie + Z3)
aptos update prover-dependencies

# 3. Semgrep + Move rules
pip install semgrep  # or brew install semgrep
git clone https://github.com/aptos-labs/semgrep-move-rules.git ~/i/tools/semgrep-move-rules

# 4. MoveSmith (compiler fuzzer)
git clone https://github.com/aptos-labs/move-smith.git ~/i/tools/move-smith
cd ~/i/tools/move-smith && make build-docker

# 5. Belobog (contract fuzzer)
git clone https://github.com/abortfuzz/belobog.git ~/i/tools/belobog

# 6. Movetool (bytecode disassembler)
git clone https://github.com/Zellic/movetool.git ~/i/tools/movetool
cd ~/i/tools/movetool && cargo build --release

# 7. Move Mutation Tools
RUSTFLAGS="--cfg tokio_unstable" cargo install \
  --git https://github.com/eigerco/move-mutation-tools.git \
  --locked move-mutation-test

# 8. Move Prover Examples (learning)
git clone https://github.com/Zellic/move-prover-examples.git ~/i/tools/move-prover-examples

# 9. Move Audit Resources (checklists)
git clone https://github.com/0xriazaka/Move-Audit-Resources.git ~/i/tools/move-audit-resources

GF(3) Audit Triad

move-smart-contract-audit (-1 VALIDATOR)
  ⊗ aptos-agent (0 COORDINATOR)
  ⊗ aptos-gf3-society (+1 GENERATOR)
  = 0 ✓

move-smart-contract-audit (-1) ⊗ move-smith-fuzzer (-1) ⊗ token-integration-analyzer (-1) = 0 (mod 3) ✓

References

Skill Name: move-smart-contract-audit Type: Security Audit / Formal Verification / Fuzzing Trit: -1 (MINUS - VALIDATOR) GF(3): Validates Move contracts through 6-layer security pipeline