io.github.Bajuzjefe/aikido-mcp

---

Security analysis platform for Aiken smart contracts on Cardano.

Aikido goes beyond static analysis. It combines a 75-detector suite with SMT verification, transaction simulation, compliance analysis, protocol pattern detection, and grammar-aware fuzzing to find vulnerabilities in Aiken smart contracts before they reach mainnet. Multi-lane analysis cross-correlates evidence across techniques, producing findings with source context, severity ratings, CWE/CWC classifications, and actionable remediation guidance.

Built in Rust. Fast. Zero configuration required.

---

Why Aikido

Cardano smart contracts are immutable once deployed. A vulnerability in production means lost funds with no recourse. Manual audits are expensive, slow, and bottlenecked. Aikido catches the classes of bugs that auditors find most often - double satisfaction, missing signature checks, unbounded iteration, unsafe datum handling - automatically, in seconds.

• The only security tool for Aiken - no alternatives exist in the ecosystem
• 75 detectors with CWC (Cardano Weakness Classification) and CWE mappings
• Multi-lane analysis - static detectors, compliance, SMT verification, transaction simulation, protocol detection, fuzzing
• Validated against professional audit - 85% coverage on TxPipe's Strike Finance audit findings (full comparison)
• Evidence framework - findings corroborated across multiple analysis techniques (PatternMatch -> SmtProven -> SimulationConfirmed)
• 9 output formats - terminal, JSON, SARIF, Markdown, HTML, PDF, CSV, GitLab SAST, reviewdog
• Ecosystem proven - 10+ real-world projects including SundaeSwap, Anastasia Labs, Strike Finance, and Seedelf (0 crashes)

---

Quick Start

Install

# 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

# From source
git clone https://github.com/Bajuzjefe/Aikido-Security-Analysis-Platform.git
cd aikido && cargo build --release

Run

aikido /path/to/your-aiken-project

Example Output

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
  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<TreasuryDatum>,
    >   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
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━

---

Analysis Architecture

Aikido uses a multi-lane approach where independent analysis techniques cross-validate each other:

graph TB
    subgraph Input
        A[Aiken Project] --> B[Typed AST]
    end

    subgraph Analysis Lanes
        B --> C[Detector Suite<br/>75 detectors]
        B --> D[Compliance<br/>Securify2-style]
        B --> E[SMT Verification<br/>Cardano axioms]
        B --> F[Tx Simulation<br/>exploit generation]
        B --> G[Protocol Detection<br/>DeFi classification]
        B --> H[Fuzz Lane<br/>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<br/>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

Lane Details

Lane	What it does
Detector Suite	Cross-module interprocedural analysis, taint tracking, symbolic execution, delegation-aware suppression, transitive signal merging, datum continuity tracking
Compliance	Securify2-style dual-pattern system: every security property has compliance (safe) and violation (unsafe) patterns. 10 security property variants
SMT Verification	Solver-independent interface with Cardano domain axioms (value conservation, signature semantics, minting policy). Constraint solving for reachability
Tx Simulation	ScriptContext builder generates concrete exploit scenarios. Tests 6 detector categories against simulated transactions
Protocol Detection	Automatic DeFi protocol classification (DEX, Lending, Staking, DAO, NFT, Options, Escrow). Token flow and authority analysis
Fuzz Lane	Grammar-aware Cardano transaction generation, Echidna-style stateful protocol fuzzing, deterministic PRNG

Supporting modules: CWC Registry (30 entries mapping all 75 detectors), Scorecard (Experimental -> Beta -> Stable promotion with quality gates), SSA IR (phi nodes, dominators, use-def chains).

---

Real-World Validation

Strike Finance Audit Comparison

Aikido was benchmarked against TxPipe's professional audit of Strike Finance (perpetuals + forwards contracts):

Metric	Result
TxPipe security findings analyzed	24
Full match (true positive)	12
Partial match	5
Correctly not flagged (code fixed)	4
False negatives	3
Aikido unique findings	26
Coverage (unfixed findings)	85%

Full methodology and per-finding breakdown: AUDIT_COMPARISON.md

Ecosystem Validation

Validated against 10+ real-world Aiken smart contract projects with zero crashes:

Project	Findings	Severity Distribution
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
Total	176	81% estimated true positive rate

---

Detectors

75 detectors mapped to CWE identifiers.

Critical (5)

Detector	CWE	Description
double-satisfaction	CWE-362	Spend handler iterates outputs without referencing own input
missing-minting-policy-check	CWE-862	Mint handler doesn't validate which token names are minted
missing-utxo-authentication	CWE-345	Reference inputs used without authentication
unrestricted-minting	CWE-862	Minting policy with no authorization check at all
output-address-not-validated	CWE-20	Outputs sent to unchecked addresses

High (19)

Detector	CWE	Description
missing-redeemer-validation	CWE-20	Catch-all redeemer pattern trivially returns True
missing-signature-check	CWE-862	Authority datum fields with no extra_signatories check
unsafe-datum-deconstruction	CWE-252	Option datum not safely deconstructed with expect Some
missing-datum-in-script-output	CWE-404	Script output without datum attachment (funds locked forever)
arbitrary-datum-in-output	CWE-20	Outputs produced without validating datum correctness
division-by-zero-risk	CWE-369	Division with attacker-controlled denominator
token-name-not-validated	CWE-20	Mint policy checks auth but not token names
value-not-preserved	CWE-682	Spend handler doesn't verify output value >= input value
unsafe-match-comparison	CWE-697	Value compared with match instead of structural equality
integer-underflow-risk	CWE-191	Subtraction on redeemer-controlled values
quantity-of-double-counting	CWE-682	Token quantity checked without isolating input vs output
state-transition-integrity	CWE-20	Redeemer actions without datum transition validation
withdraw-zero-trick	CWE-863	Withdraw handler exploitable with zero-value withdrawal
other-token-minting	CWE-862	Mint policy allows minting tokens beyond intended scope
unsafe-redeemer-arithmetic	CWE-682	Arithmetic on redeemer-tainted values without bounds
value-preservation-gap	CWE-682	Lovelace checked but native assets not preserved
uncoordinated-multi-validator	CWE-362	Multi-handler validator without cross-handler coordination
missing-burn-verification	CWE-862	Token burning without proper verification
oracle-manipulation-risk	CWE-20	Oracle data used without manipulation safeguards

Medium (24)

Detector	CWE	Description
missing-validity-range	CWE-613	Time-sensitive datum without validity_range check
insufficient-staking-control	CWE-863	Outputs don't constrain staking credential
unbounded-datum-size	CWE-400	Datum fields with unbounded types (List, ByteArray)
unbounded-value-size	CWE-400	Outputs don't constrain native asset count
unbounded-list-iteration	CWE-400	Direct iteration over raw transaction list fields
oracle-freshness-not-checked	CWE-613	Oracle data used without recency verification
non-exhaustive-redeemer	CWE-478	Redeemer match doesn't cover all constructors
hardcoded-addresses	CWE-798	ByteArray literals matching Cardano address lengths
utxo-contention-risk	CWE-400	Single global UTXO contention pattern
cheap-spam-vulnerability	CWE-770	Validator vulnerable to cheap UTXO spam
unsafe-partial-pattern	CWE-252	Expect pattern on non-Option type that may fail at runtime
unconstrained-recursion	CWE-674	Self-recursive handler without clear termination
empty-handler-body	CWE-561	Handler with no meaningful logic
unsafe-list-head	CWE-129	list.head() / list.at() without length guard
missing-datum-field-validation	CWE-20	Spend handler accepts datum fields but never validates them
missing-token-burn	CWE-862	Minting policy with no burn handling
missing-state-update	CWE-665	State machine without datum update
rounding-error-risk	CWE-682	Integer division on financial values
missing-input-credential-check	CWE-862	Input iteration without credential check
duplicate-asset-name-risk	CWE-694	Minting without unique asset name enforcement
fee-calculation-unchecked	CWE-682	Fee or protocol payment without validation
datum-tampering-risk	CWE-20	Datum passed through without field-level validation
missing-protocol-token	CWE-862	State transition without protocol token verification
unbounded-protocol-operations	CWE-400	Both input and output lists iterated without bounds

Low / Info (12)

Detector	Severity	Description
reference-script-injection	Low	Outputs don't constrain reference_script field
unused-validator-parameter	Low	Validator parameter never referenced
fail-only-redeemer-branch	Low	Redeemer branch that always fails
missing-min-ada-check	Info	Script output without minimum ADA check
dead-code-path	Low	Unreachable code paths
redundant-check	Low	Trivially true conditions
shadowed-variable	Info	Handler parameter shadowed by pattern binding
magic-numbers	Info	Unexplained numeric literals
excessive-validator-params	Info	Too many validator parameters
unused-import	Info	Imported module with no function calls

Each detector has detailed documentation with vulnerable examples, safe examples, and remediation guidance. Use aikido --explain <detector-name> or see docs/detectors/.

---

Output Formats

9 formats for different workflows:

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

---

Configuration

.aikido.toml

# Use a preset as a starting point
extends = "strict"      # or "lenient" for fewer warnings

[detectors]
disable = ["magic-numbers", "unused-import"]

[detectors.severity_override]
unbounded-datum-size = "low"

# Per-file overrides
[[files]]
pattern = "tests/**"
disable = ["hardcoded-addresses", "magic-numbers"]

Inline Suppression

// aikido:ignore[double-satisfaction] -- false positive: own_ref checked in helper
spend(datum, redeemer, own_ref, tx) {
  ...
}

Baseline Support

aikido /path --accept-baseline    # Save current findings as baseline
aikido /path                      # Only new findings reported

---

CI/CD Integration

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 Reference

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 <rule>       # 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 <url>                  # Clone and analyze remote repo
aikido --benchmark-manifest benchmarks/local-fixtures.toml --format json
aikido --benchmark-manifest benchmarks/local-fixtures.toml --benchmark-enforce-gates

---

Architecture

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

Building from Source

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)

Requires Rust >= 1.88.0.

---

Vulnerability Coverage

Detectors are derived from real vulnerabilities found in published Cardano smart contract audits:

Source	Findings Covered
MLabs audit reports	Double satisfaction, missing minting policy, arbitrary datum, unbounded size
Vacuumlabs audit reports	Unbounded value size, token dust attacks
Plutonomicon	Unrestricted minting, double satisfaction patterns
Anastasia Labs audit reports	Staking credential theft, datum handling
TxPipe audit reports	Oracle manipulation, state transition integrity, value preservation
CWE Database	75 detectors mapped to specific CWE identifiers

---

License

MIT