GitHub - Bajuzjefe/Aikido-Security-Analysis-Platform: Security analysis platform for Aiken smart contracts on Cardano: 75 detectors, SMT verification, transaction simulation

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

Name		Name	Last commit message	Last commit date
Latest commit History 5 Commits
.github/workflows		.github/workflows
audits/strike-finance		audits/strike-finance
benchmarks		benchmarks
crates		crates
docs-src		docs-src
docs/detectors		docs/detectors
fixtures		fixtures
fuzz		fuzz
homebrew		homebrew
mcp-server		mcp-server
npm		npm
scripts		scripts
vscode-extension		vscode-extension
.gitignore		.gitignore
.pre-commit-hooks.yaml		.pre-commit-hooks.yaml
AUDIT_COMPARISON.md		AUDIT_COMPARISON.md
CHANGELOG.md		CHANGELOG.md
Cargo.lock		Cargo.lock
Cargo.toml		Cargo.toml
Dockerfile		Dockerfile
LICENSE		LICENSE
README.md		README.md
action.yml		action.yml
aikido-og.png		aikido-og.png
mutants.toml		mutants.toml

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Repository files navigation

Why Aikido

Quick Start

Install

Run

Example Output

Analysis Architecture

Lane Details

Real-World Validation

Strike Finance Audit Comparison

Ecosystem Validation

Detectors

Output Formats

Configuration

`.aikido.toml`

Inline Suppression

Baseline Support

CI/CD Integration

GitHub Actions

Docker

CLI Reference

Architecture

Building from Source

Vulnerability Coverage

License

About

Uh oh!

Contributors

Uh oh!

Languages

Folders and files

Latest commit

History

Repository files navigation

Why Aikido

Quick Start

Install

Run

Example Output

Analysis Architecture

Lane Details

Real-World Validation

Strike Finance Audit Comparison

Ecosystem Validation

Detectors

Output Formats

Configuration

.aikido.toml

Inline Suppression

Baseline Support

CI/CD Integration

GitHub Actions

Docker

CLI Reference

Architecture

Building from Source

Vulnerability Coverage

License

About

Topics

Resources

License

Uh oh!

Stars

Watchers

Forks

Contributors

Uh oh!

Languages

`.aikido.toml`