Lab Specification — Module S11: Smart Contract Audit Harnesses

# Install Foundry
curl -L https://foundry.paradigm.xyz | bash && foundryup
# Install Slither
pip install slither-analyzer solc-select
solc-select install 0.8.20 && solc-select use 0.8.20
# Clone Damn Vulnerable DeFi
git clone https://github.com/tinchoabbate/damn-vulnerable-defi.git
cd damn-vulnerable-defi
forge install

# Run Slither, capture JSON output
slither ./contracts/unstoppable/ --json slither-unstoppable.json
# Count raw findings
python3 -c "import json; d=json.load(open('slither-unstoppable.json')); print(f'{len(d)} raw findings')"

import json

findings = json.load(open("slither-unstoppable.json"))
# Manual ground-truth tagging against DVD's documented vulnerability
real = [f for f in findings if relates_to_known_vuln(f)]
fps = [f for f in findings if not relates_to_known_vuln(f)]
precision = len(real) / len(findings) if findings else 0
print(f"Raw Slither: {len(findings)} findings, {len(real)} real, precision={precision:.2%}")

async def triage_slither_finding(finding, challenge_context, llm_client):
    prompt = f"""
    You are a smart contract security triage analyst. Slither flagged this:

    Detector: {finding['check']}
    Location: {finding['elements'][0]['source_mapping']['filename']}:
              line {finding['elements'][0]['source_mapping']['lines']}
    Description: {finding['description']}

    Relevant code:
    {finding['code_snippet']}

    Challenge context: {challenge_context}

    Questions:
    1. Is this a real vulnerability (not a false positive on a benign pattern)?
    2. Is it exploitable in this specific protocol context?
    3. Does it relate to the challenge's intended vulnerability class?

    Respond as JSON: {{"real": bool, "exploitable": bool, "reasoning": str}}
    """
    result = await llm_client.complete(prompt)
    return json.loads(result)

async def extract_invariants(contract_source, llm_client):
    prompt = f"""
    You are a smart contract auditor. Read this DeFi protocol and identify
    the invariants that MUST hold for the protocol to be safe.

    An invariant is a property that must be true across all reachable states.

    Contract source:
    {contract_source}

    For each invariant, state:
    - The invariant in plain language
    - Which functions/state variables it involves
    - How it could be checked (runtime assertion, fuzz target, or formal spec)

    Respond as JSON: {{"invariants": [{{"statement": str, "involves": [str], "check_method": str}}]}}
    """
    result = await llm_client.complete(prompt)
    return json.loads(result)["invariants"]

// Foundry invariant test for "deposits sum == contract balance"
contract SideEntranceInvariantTest is Test {
    SideEntrancePool pool;

    function setUp() public {
        pool = new SideEntrancePool();
    }

    // Invariant: the pool's ETH balance equals the sum of all deposits
    function invariant_balance_equals_deposits() public {
        assertEq(address(pool).balance, pool.totalDeposits());
    }
}

forge test --match-test invariant_ -vvv

# In foundry.toml
[rpc_endpoints]
mainnet = "${MAINNET_RPC_URL}"

// test/Exploit.t.sol
import {Test} from "forge-std/Test.sol";

contract ExploitTest is Test {
    VulnerableVault vault;
    address attacker = makeAddr("attacker");

    function setUp() public {
        // Fork mainnet at a block where the target is deployed
        vm.createFork("mainnet", BLOCK_NUMBER);
        vault = VulnerableVault(VAULT_ADDRESS);
        vm.deal(attacker, 100 ether);
    }

    function test_reentrancy_exploit() public {
        uint256 vaultBalanceBefore = address(vault).balance;
        uint256 attackerBalanceBefore = attacker.balance;

        vm.startPrank(attacker);
        AttackContract attack = new AttackContract(vault);
        attack.attack{value: 10 ether}();
        vm.stopPrank();

        uint256 vaultBalanceAfter = address(vault).balance;
        uint256 attackerBalanceAfter = attacker.balance;

        // Verification: vault drained, attacker profit
        assertLt(vaultBalanceAfter, vaultBalanceBefore, "vault not drained");
        assertGt(attackerBalanceAfter, attackerBalanceBefore, "no attacker profit");

        // Economic impact
        uint256 profit = attackerBalanceAfter - attackerBalanceBefore;
        emit log_named_uint("Attacker profit (wei)", profit);
    }
}

import subprocess, json

def run_poc_and_capture(poc_path, fork_block):
    result = subprocess.run(
        ["forge", "test", "--match-test", "test_reentrancy_exploit", "-vvv", "--json"],
        capture_output=True, text=True, cwd=poc_path
    )
    test_output = json.loads(result.stdout)
    # Extract: transaction hash, call trace, state delta, gas used
    evidence = {
        "fork_block": fork_block,
        "test_passed": test_output["test_results"][0]["status"] == "success",
        "call_trace": test_output["test_results"][0]["decoded_logs"],
        "gas_used": test_output["test_results"][0]["gas_used"],
        # Economic impact from the emitted log
    }
    return evidence

async def generate_patch(vulnerability, exploit_poc, contract_source, llm_client):
    prompt = f"""
    You are a smart contract security engineer. Generate a minimal patch
    that fixes this vulnerability WITHOUT changing the contract's intended behavior.

    Vulnerability: {vulnerability['description']}
    Location: {vulnerability['location']}
    Exploit PoC: {exploit_poc}
    Contract source: {contract_source}

    Requirements:
    - The patch must remove the vulnerability.
    - The patch must preserve all intended behavior (do not remove functionality).
    - Output a unified diff.

    Respond with the diff only.
    """
    return await llm_client.complete(prompt)

class PatchVerifier:
    def __init__(self, contract_dir, poc_test):
        self.contract_dir = contract_dir
        self.poc_test = poc_test  # the Foundry test from Phase 3

    def gate1_static_recheck(self, patched_dir) -> tuple[bool, str]:
        """Original finding gone? No new Slither findings?"""
        result = subprocess.run(
            ["slither", patched_dir, "--json", "-"],
            capture_output=True, text=True
        )
        findings = json.loads(result.stdout)
        original_pattern = self.original_finding_pattern
        original_gone = not any(f["check"] == original_pattern for f in findings)
        new_findings = [f for f in findings if f not in self.baseline_findings]
        return original_gone and len(new_findings) == 0, f"original_gone={original_gone}, new={len(new_findings)}"

    def gate2_test_suite(self, patched_dir) -> tuple[bool, str]:
        """All existing tests + property tests pass?"""
        result = subprocess.run(
            ["forge", "test", "--json"],
            capture_output=True, text=True, cwd=patched_dir
        )
        results = json.loads(result.stdout)["test_results"]
        all_pass = all(r["status"] == "success" for r in results)
        return all_pass, f"{sum(r['status']=='success' for r in results)}/{len(results)} passed"

    def gate3_exploit_rerun(self, patched_dir) -> tuple[bool, str]:
        """The exploit PoC now FAILS (attack path closed)?"""
        result = subprocess.run(
            ["forge", "test", "--match-test", self.poc_test, "--json"],
            capture_output=True, text=True, cwd=patched_dir
        )
        results = json.loads(result.stdout)["test_results"]
        # The exploit test should now FAIL (meaning the exploit no longer works)
        exploit_fails = results[0]["status"] != "success"
        return exploit_fails, f"exploit test status: {results[0]['status']}"

    def gate4_formal_verification(self, patched_dir) -> tuple[bool, str]:
        """Formal property holds? (where feasible)"""
        # If Halmos or Certora is available, run it on the patched invariant
        # Otherwise, mark as N/A
        return True, "N/A (no formal prover configured)"

    def verify(self, patched_dir) -> dict:
        results = {}
        for name, gate in [("gate1", self.gate1_static_recheck),
                           ("gate2", self.gate2_test_suite),
                           ("gate3", self.gate3_exploit_rerun),
                           ("gate4", self.gate4_formal_verification)]:
            passed, detail = gate(patched_dir)
            results[name] = {"passed": passed, "detail": detail}
            if not passed:
                break  # fail fast
        all_passed = all(r["passed"] for r in results.values())
        results["all_gates_passed"] = all_passed
        results["ready_for_approval"] = all_passed
        return results

# Lab Specification — Module S11: Smart Contract Audit Harnesses

**Course**: 2A — Building AI Harnesses for Cybersecurity
**Module**: S11 — Smart Contract Audit Harnesses
**Duration**: 150–180 minutes (substantial — four labs, one per sub-section)
**Environment**: Python 3.11+, Foundry (forge/anvil), Slither, an LLM API (Claude or GPT-class). Lab target: **Damn Vulnerable DeFi** (https://www.damnvulnerabledefi.xyz/) — all four labs run against this. No live mainnet targets.

> All four labs use Damn Vulnerable DeFi as the target. Each challenge in DVD is a known-vulnerable DeFi protocol with a real exploit path. This makes it possible to measure detection, exploitation, and patching against ground truth.

---

## Learning objectives

1. Run Slither against a known-vulnerable contract and measure raw precision; add LLM triage and measure improvement.
2. Implement an invariant extraction and checking harness; identify at least one invariant violation.
3. Build a Foundry-based exploit PoC on forked mainnet with structured evidence.
4. Build a patch generation and verification pipeline with the four cascaded gates.

---

## Phase 1 — Slither + LLM Triage (35 min)

### 1.1 Set up the environment

```bash
# Install Foundry
curl -L https://foundry.paradigm.xyz | bash && foundryup
# Install Slither
pip install slither-analyzer solc-select
solc-select install 0.8.20 && solc-select use 0.8.20
# Clone Damn Vulnerable DeFi
git clone https://github.com/tinchoabbate/damn-vulnerable-defi.git
cd damn-vulnerable-defi
forge install
```

### 1.2 Run Slither against a DVD challenge

Pick the "Unstoppable" challenge (a flash loan / oracle manipulation vulnerability).

```bash
# Run Slither, capture JSON output
slither ./contracts/unstoppable/ --json slither-unstoppable.json
# Count raw findings
python3 -c "import json; d=json.load(open('slither-unstoppable.json')); print(f'{len(d)} raw findings')"
```

### 1.3 Measure raw precision

Damn Vulnerable DeFi documents the intended vulnerability for each challenge (in the challenge README / solution). Tag each Slither finding as: real (relates to the known vulnerability), false positive (benign pattern flagged), or irrelevant (different, non-target issue).

```python
import json

findings = json.load(open("slither-unstoppable.json"))
# Manual ground-truth tagging against DVD's documented vulnerability
real = [f for f in findings if relates_to_known_vuln(f)]
fps = [f for f in findings if not relates_to_known_vuln(f)]
precision = len(real) / len(findings) if findings else 0
print(f"Raw Slither: {len(findings)} findings, {len(real)} real, precision={precision:.2%}")
```

### 1.4 Add LLM triage and re-measure

For each Slither finding, call an LLM with the finding's location, the detector name, the relevant code snippet, and the challenge's context. Ask: is this finding real and exploitable in this context, or a false positive?

```python
async def triage_slither_finding(finding, challenge_context, llm_client):
    prompt = f"""
    You are a smart contract security triage analyst. Slither flagged this:

    Detector: {finding['check']}
    Location: {finding['elements'][0]['source_mapping']['filename']}:
              line {finding['elements'][0]['source_mapping']['lines']}
    Description: {finding['description']}

    Relevant code:
    {finding['code_snippet']}

    Challenge context: {challenge_context}

    Questions:
    1. Is this a real vulnerability (not a false positive on a benign pattern)?
    2. Is it exploitable in this specific protocol context?
    3. Does it relate to the challenge's intended vulnerability class?

    Respond as JSON: {{"real": bool, "exploitable": bool, "reasoning": str}}
    """
    result = await llm_client.complete(prompt)
    return json.loads(result)
```

Measure precision after LLM triage. Compare to raw Slither precision.

### Deliverable
- [ ] Slither raw findings count and precision against DVD ground truth
- [ ] LLM-triaged findings count and precision
- [ ] Comparison table: raw precision vs. triaged precision
- [ ] Documented false positives that the LLM correctly filtered

---

## Phase 2 — Invariant Extraction and Checking (40 min)

### 2.1 Extract candidate invariants

Pick the "Side Entrance" challenge (a flash loan / deposit-withdraw logic vulnerability). Read the challenge contracts and documentation. Use an LLM to extract candidate invariants.

```python
async def extract_invariants(contract_source, llm_client):
    prompt = f"""
    You are a smart contract auditor. Read this DeFi protocol and identify
    the invariants that MUST hold for the protocol to be safe.

    An invariant is a property that must be true across all reachable states.

    Contract source:
    {contract_source}

    For each invariant, state:
    - The invariant in plain language
    - Which functions/state variables it involves
    - How it could be checked (runtime assertion, fuzz target, or formal spec)

    Respond as JSON: {{"invariants": [{{"statement": str, "involves": [str], "check_method": str}}]}}
    """
    result = await llm_client.complete(prompt)
    return json.loads(result)["invariants"]
```

### 2.2 Formalize and check invariants

For each extracted invariant, implement a check:

- **Runtime assertions** — add `assert()` or custom checks to the contract, deploy in a test, and fuzz.
- **Foundry invariant tests** — use `forge test` with `invariant` prefix functions and `forge test --fuzz-runs 1000`.

```solidity
// Foundry invariant test for "deposits sum == contract balance"
contract SideEntranceInvariantTest is Test {
    SideEntrancePool pool;

    function setUp() public {
        pool = new SideEntrancePool();
    }

    // Invariant: the pool's ETH balance equals the sum of all deposits
    function invariant_balance_equals_deposits() public {
        assertEq(address(pool).balance, pool.totalDeposits());
    }
}
```

### 2.3 Identify the violation

Run the invariant tests. When an invariant breaks under fuzzing or a constructed attack, you have found the logic bug.

```bash
forge test --match-test invariant_ -vvv
```

Construct the attack that violates the invariant (the flash loan path). Confirm the LLM judges it as economically exploitable.

### Deliverable
- [ ] List of extracted candidate invariants (3+)
- [ ] Formalized checks (Foundry invariant tests)
- [ ] At least one invariant violation identified
- [ ] LLM confirmation that the violation is economically exploitable (flash-loan reachable)

---

## Phase 3 — Foundry Exploit PoC on Forked Mainnet (40 min)

### 3.1 Set up a forked mainnet environment

For a reentrancy-focused challenge (e.g., "The Rewarder" or a custom vulnerable vault), configure Foundry to fork mainnet.

```bash
# In foundry.toml
[rpc_endpoints]
mainnet = "${MAINNET_RPC_URL}"
```

### 3.2 Write the exploit PoC

```solidity
// test/Exploit.t.sol
import {Test} from "forge-std/Test.sol";

contract ExploitTest is Test {
    VulnerableVault vault;
    address attacker = makeAddr("attacker");

    function setUp() public {
        // Fork mainnet at a block where the target is deployed
        vm.createFork("mainnet", BLOCK_NUMBER);
        vault = VulnerableVault(VAULT_ADDRESS);
        vm.deal(attacker, 100 ether);
    }

    function test_reentrancy_exploit() public {
        uint256 vaultBalanceBefore = address(vault).balance;
        uint256 attackerBalanceBefore = attacker.balance;

        vm.startPrank(attacker);
        AttackContract attack = new AttackContract(vault);
        attack.attack{value: 10 ether}();
        vm.stopPrank();

        uint256 vaultBalanceAfter = address(vault).balance;
        uint256 attackerBalanceAfter = attacker.balance;

        // Verification: vault drained, attacker profit
        assertLt(vaultBalanceAfter, vaultBalanceBefore, "vault not drained");
        assertGt(attackerBalanceAfter, attackerBalanceBefore, "no attacker profit");

        // Economic impact
        uint256 profit = attackerBalanceAfter - attackerBalanceBefore;
        emit log_named_uint("Attacker profit (wei)", profit);
    }
}
```

### 3.3 Capture structured evidence

```python
import subprocess, json

def run_poc_and_capture(poc_path, fork_block):
    result = subprocess.run(
        ["forge", "test", "--match-test", "test_reentrancy_exploit", "-vvv", "--json"],
        capture_output=True, text=True, cwd=poc_path
    )
    test_output = json.loads(result.stdout)
    # Extract: transaction hash, call trace, state delta, gas used
    evidence = {
        "fork_block": fork_block,
        "test_passed": test_output["test_results"][0]["status"] == "success",
        "call_trace": test_output["test_results"][0]["decoded_logs"],
        "gas_used": test_output["test_results"][0]["gas_used"],
        # Economic impact from the emitted log
    }
    return evidence
```

### Deliverable
- [ ] Working Foundry exploit PoC on forked mainnet (test passes)
- [ ] Structured evidence: transaction trace, state before/after, economic impact
- [ ] PoC file reproducible with `forge test`
- [ ] The exploit confirms the finding is real (not theoretical)

---

## Phase 4 — Patch Generation with Cascaded Verification (45 min)

### 4.1 Generate a patch

For the vulnerability exploited in Phase 3, use an LLM to generate a patch.

```python
async def generate_patch(vulnerability, exploit_poc, contract_source, llm_client):
    prompt = f"""
    You are a smart contract security engineer. Generate a minimal patch
    that fixes this vulnerability WITHOUT changing the contract's intended behavior.

    Vulnerability: {vulnerability['description']}
    Location: {vulnerability['location']}
    Exploit PoC: {exploit_poc}
    Contract source: {contract_source}

    Requirements:
    - The patch must remove the vulnerability.
    - The patch must preserve all intended behavior (do not remove functionality).
    - Output a unified diff.

    Respond with the diff only.
    """
    return await llm_client.complete(prompt)
```

### 4.2 Implement the four verification gates

```python
class PatchVerifier:
    def __init__(self, contract_dir, poc_test):
        self.contract_dir = contract_dir
        self.poc_test = poc_test  # the Foundry test from Phase 3

    def gate1_static_recheck(self, patched_dir) -> tuple[bool, str]:
        """Original finding gone? No new Slither findings?"""
        result = subprocess.run(
            ["slither", patched_dir, "--json", "-"],
            capture_output=True, text=True
        )
        findings = json.loads(result.stdout)
        original_pattern = self.original_finding_pattern
        original_gone = not any(f["check"] == original_pattern for f in findings)
        new_findings = [f for f in findings if f not in self.baseline_findings]
        return original_gone and len(new_findings) == 0, f"original_gone={original_gone}, new={len(new_findings)}"

    def gate2_test_suite(self, patched_dir) -> tuple[bool, str]:
        """All existing tests + property tests pass?"""
        result = subprocess.run(
            ["forge", "test", "--json"],
            capture_output=True, text=True, cwd=patched_dir
        )
        results = json.loads(result.stdout)["test_results"]
        all_pass = all(r["status"] == "success" for r in results)
        return all_pass, f"{sum(r['status']=='success' for r in results)}/{len(results)} passed"

    def gate3_exploit_rerun(self, patched_dir) -> tuple[bool, str]:
        """The exploit PoC now FAILS (attack path closed)?"""
        result = subprocess.run(
            ["forge", "test", "--match-test", self.poc_test, "--json"],
            capture_output=True, text=True, cwd=patched_dir
        )
        results = json.loads(result.stdout)["test_results"]
        # The exploit test should now FAIL (meaning the exploit no longer works)
        exploit_fails = results[0]["status"] != "success"
        return exploit_fails, f"exploit test status: {results[0]['status']}"

    def gate4_formal_verification(self, patched_dir) -> tuple[bool, str]:
        """Formal property holds? (where feasible)"""
        # If Halmos or Certora is available, run it on the patched invariant
        # Otherwise, mark as N/A
        return True, "N/A (no formal prover configured)"

    def verify(self, patched_dir) -> dict:
        results = {}
        for name, gate in [("gate1", self.gate1_static_recheck),
                           ("gate2", self.gate2_test_suite),
                           ("gate3", self.gate3_exploit_rerun),
                           ("gate4", self.gate4_formal_verification)]:
            passed, detail = gate(patched_dir)
            results[name] = {"passed": passed, "detail": detail}
            if not passed:
                break  # fail fast
        all_passed = all(r["passed"] for r in results.values())
        results["all_gates_passed"] = all_passed
        results["ready_for_approval"] = all_passed
        return results
```

### 4.3 Run the cascade and document the approval gate

1. Apply the generated patch to the contract.
2. Run all four gates.
3. If any gate fails, feed the failure back to the LLM and regenerate (max 3 attempts).
4. If all gates pass, produce the approval package: patch diff, rationale, gate results, original finding, exploit PoC.
5. Document that a human auditor must review before deployment (the harness does NOT deploy).

### Deliverable
- [ ] Generated patch (unified diff)
- [ ] All four gate results documented
- [ ] Gate 1: original finding gone, no new Slither findings
- [ ] Gate 2: test suite / property tests pass
- [ ] Gate 3: exploit PoC now fails
- [ ] Gate 4: formal verification result (or N/A with justification)
- [ ] Approval package produced (diff + rationale + gate results)
- [ ] Documented that human approval is required before deployment

---

## Stretch goals

1. **Cross-contract invariant extraction** — extend Phase 2 to extract invariants that span multiple contracts (e.g., "the oracle price consumed by Vault equals the price reported by Oracle"). Use Heimdallr's call-graph-extension approach.
2. **Automated patch regeneration** — when a gate fails, automatically feed the failure detail back to the LLM and regenerate the patch. Measure how many attempts are needed on average.
3. **Formal verification integration** — integrate Halmos (symbolic execution for Foundry) or Certora and run it as gate 4 on at least one property. Document where formal verification is feasible and where it is not.
4. **Run all four phases against a second DVD challenge** and compare results. Which challenge classes (reentrancy vs. flash loan vs. logic) does the harness handle best?