Aegis7702

The proactive reachability shield for EIP-7702 & Permit2. Aegis7702 uncovers zero-delta deferred exploit traces missed by 1-step simulators, synthesizing verified on-chain recovery transactions.

Comment

Aegis7702 (Guard7702): Bounded Capability-Reachability Verifier & Recovery Engine

Project Name: Aegis7702

Inspiration

The inspiration for Aegis7702 originates directly from the shift in Ethereum's post-Pectra architecture. With the activation of EIP-7702, Externally Owned Accounts (EOAs) can delegate execution through a delegation designator that points to smart-contract code while preserving the EOA address. When coupled with widely used off-chain signature protocols such as Uniswap's Permit2 (PermitSingle, PermitBatch, PermitTransferFrom), authorization signing can be separated from the later on-chain execution that consumes that authorization.

This decoupling exposes a limitation in immediate, single-step transaction-security models. A simple immediate-delta baseline can be represented as:

$$ \mathrm{Safe}(s_0,\mathrm{tx}) \iff \Delta \mathrm{Balance}(s_0) \ge -\epsilon $$

When an attacker tricks a victim into signing an off-chain EIP-7702 authorization tuple,

$$ c=(\mathrm{chainId},\mathrm{address},\mathrm{nonce},y,r,s) $$

or a detached Permit2 signature, zero state changes occur on-chain at Step 0. An immediate-delta simulator can therefore observe \(\Delta \text{Balance}(s_0) = 0\) and emit a reassuring SAFE verdict. Later, an attacker may broadcast the authorization, install a delegation designator pointing to malicious logic or activate a Permit2 capability, and execute a loss-producing path. This creates a dangerous false negative for a purely immediate-delta baseline.

This threat surface is empirically documented. Research presented at USENIX Security 2026 by Huang et al. reports that, across a seven-chain dataset, over 63% of observed EIP-7702 authorization transactions were associated with malicious EOA-targeted attacks, identifying 924 malicious contract accounts, more than $2.3M in realized losses, and over $10M in exposed assets.

We built Aegis7702 around a single foundational mathematical thesis:

$$ \mathrm{SimulateCurrentExecution}(c,s_0) \not\Rightarrow \mathrm{SafeFutureCapability}(c,s_0) $$

Conventional simulation reveals what a proposed execution does under a particular current state \(s_0\). Detached capabilities demand a different question: What future attacker-controlled state transitions become reachable once this signed capability is released?

What it does

Aegis7702 is a typed, bounded Capability-Reachability Verifier (CRV) and State-Specific Recovery Synthesizer for EIP-7702 authorizations and Uniswap Permit2 signatures.

Instead of outputting an opaque probabilistic risk score, Aegis7702 executes a deterministic verification workflow against EVM state snapshots.

1. Typed Capability Extraction: Decodes signed authorization payloads into structured capabilities \(c \in \mathcal{C}\) across three supported domains:

  • EIP-7702 delegation authorization tuples
  • Uniswap Permit2 AllowanceTransfer (PermitSingle / PermitBatch)
  • Uniswap Permit2 SignatureTransfer (unordered nonce bitmaps)

2. Bounded Reachability Search (\(k \le 3\)): Generates candidate attacker action sequences within modeled semantics \(\mathcal{A}_{\text{modeled}}\) and explores downstream EVM state branches.

$$ \mathrm{Unsafe}{\le k}^{\mathcal A{\mathrm{modeled}}}(c,s_0) \iff \exists \pi=(a_1,\ldots,a_j),\; j\le k:\; L(s_0,T_\pi(s_0))>0 $$

Let \(\mathcal T\) denote the tracked assets and \(B_t(s)\) the victim's balance of asset \(t\) in state \(s\). The loss function is:

$$ L(s_0,s')=\sum_{t\in\mathcal T}\max{0,B_t(s_0)-B_t(s')} $$

3. Executable Counterexample Witness: When a loss path is discovered, Aegis7702 returns the exact reproducible multi-step exploit trace \(\pi\), for example:

RelayAuthorization → MaliciousDelegate.sweep

4. State-Specific On-Chain Recovery Synthesis: Inspects the relevant EVM state and synthesizes a protocol-specific counter-transaction.

  • Unconsumed EIP-7702 Authorization: Constructs a 0-value self-transaction to advance the victim's account nonce from \(n\) to \(n+1\). Because EIP-7702 checks the authorization nonce against the authority account nonce, the old authorization becomes unusable once the relevant nonce no longer matches.
  • Active EIP-7702 Delegation: Constructs an EIP-7702 Type-4 recovery transaction with authorization pointing to address(0) to clear the delegation designator.
  • Permit2 Allowance: Calls canonical Permit2.invalidateNonces() to advance the relevant nonce before the signed permit is consumed, or uses Permit2.lockdown() when zeroing active allowances is the intended recovery action.
  • Permit2 Signature: Calls Permit2.invalidateUnorderedNonces(wordPos, mask) to mark the corresponding unordered nonce as used.

5. Deterministic Replay Verification: Replays the discovered attacker trace \(\pi\) against the post-recovery state \(s_R\) and checks that the previously successful trace no longer causes tracked loss.

$$ L(s_0,T_\pi(s_0))>0 \land L(s_R,T_\pi(s_R))=0 $$

Depending on the recovery and trace, the replay may revert or become a clean no-op with respect to the tracked asset; the required condition is zero tracked loss after recovery.

How we built it

We implemented a unified and reproducible three-tier architecture:

.
├── contracts/                  # Solidity smart contracts & Foundry security suites
│   ├── src/                    # Guard7702Sentinel, MaliciousDelegate, MockUSDC
│   ├── test/                   # Permit2Allowance, Permit2Signature, EIP7702Attack, Guard7702Sentinel
│   └── foundry.toml            # Solc 0.8.17, via_ir = true, Prague EVM settings
│
├── engine/                     # TypeScript Capability-Reachability Engine
│   └── src/                    # Bounded DFS explorer (k ≤ 3), state-specific recovery synthesizer
│
└── app/                        # Interactive Visualizer Dashboard (React 19 + Vite 8)
    └── src/                    # Baseline contrast, trace view, recovery and replay UI

Solidity Smart Contracts & Foundry Suite

  • Implemented Guard7702Sentinel.sol to support Permit2 nonce invalidation operations within a delegated EOA execution context.
  • Built MaliciousDelegate.sol and MockUSDC.sol as controlled EVM fixtures for EIP-7702 delegation attacks.
  • Authored 4 Foundry test suites comprising 14 passing tests:
    • Permit2AllowanceTest: 4/4 passed.
    • Permit2SignatureTest: 3/3 passed.
    • EIP7702AttackTest: 4/4 passed.
    • Guard7702SentinelTest: 3/3 passed.

TypeScript Reachability Engine

  • Built on Viem and ephemeral Anvil child processes configured for the Prague hardfork where required.
  • Implemented depth-first reachability exploration bounded at \(k \le 3\), using EVM snapshots (evm_snapshot / evm_revert) for branch isolation and backtracking.
  • Authored 3 automated, self-contained Kill Tests (killTest.ts, killTestSignature.ts, killTest7702.ts) that can execute offline without external RPC dependencies.

Interactive Proof Visualizer Dashboard

  • Built with React 19, Vite 8, Lucide, and Tailwind CSS.
  • Displays the immediate-delta baseline alongside Aegis7702 reachability analysis, interactive trace inspection, state-specific recovery actions, and replay results.
  • Distinguishes live-engine results from bundled fixture results so that precomputed evidence is not presented as a fresh on-chain execution.

Challenges we ran into

1. Combinatorial EVM Action-Space Explosion

Arbitrary EVM calls expose a practically enormous action space; even a single 256-bit calldata word admits \(2^{256}\) possible values. Generic real-time brute-force exploration is therefore impractical. We addressed this with typed capability semantics: instead of enumerating arbitrary calls, the engine decodes capability parameters such as token addresses, spenders, nonces, and delegation targets, then instantiates only supported candidate actions from \(\mathcal{A}_{\text{modeled}}\). The search is bounded at \(k \le 3\), which is chosen to cover the canonical modeled sequences used by the current prototype, such as Relay → Drain → optional follow-up action.

2. Prague Hardfork Tooling

EIP-7702 is relatively recent and requires tooling that correctly handles Type-4 transactions and 0xef0100 delegation designators. We had to orchestrate Prague-configured Anvil instances, use EIP-7702-aware Viem functionality, and build Foundry test harnesses with delegation cheatcodes such as vm.attachDelegation to reproduce the relevant execution mechanics.

3. Permit2 Caller Identity Constraints

Canonical Permit2 security functions such as invalidateNonces, invalidateUnorderedNonces, and lockdown operate on msg.sender. A third-party contract cannot arbitrarily invalidate another user's Permit2 state. Recovery transactions therefore need to execute from the victim identity or through a delegated context whose effective caller semantics satisfy the Permit2 requirements.

4. Formulating Asymmetric Mathematical Claims

Because reachability search is bounded, Aegis7702 deliberately does not claim global safety.

$$ \mathrm{Found\ loss\ path} \Rightarrow \mathrm{concrete\ vulnerability\ witness} $$

$$ \mathrm{No\ path\ found} \not\Rightarrow \mathrm{globally\ safe} $$

A bounded verifier cannot establish safety against every unmodeled action or arbitrarily deep DeFi composition. However, when Aegis7702 finds a path, it provides a concrete and reproducible counterexample within the modeled action space and tested EVM state.

Accomplishments that we're proud of

1. Closed-Loop Verification & Recovery

We did not stop at detection. Aegis7702 implements a full workflow:

Capability Extraction → Reachability Exploration → Concrete Exploit Witness → Recovery Synthesis → Post-Recovery Replay Verification

2. Offline Reproducibility

The 14 Foundry contract tests and the 3 core TypeScript Anvil kill tests are designed to run without external RPC dependencies, third-party API keys, or reliance on a public chain endpoint for their controlled fixtures.

3. Formal Mathematical Grounding

The project connects its bounded reachability formulation to the real EIP-7702 threat surface documented by the USENIX Security 2026 empirical study and discusses authorization control through the Key Sovereignty framework of Matthias Hauser (arXiv:2605.01210).

4. High-Fidelity Dashboard UI

The interactive Vite dashboard allows technical judges and users to compare an immediate-delta baseline with downstream reachability, inspect the discovered trace, review the synthesized recovery, and inspect post-recovery replay evidence.

What we learned

  • Key Sovereignty: Under Matthias Hauser's Key Sovereignty framework (arXiv:2605.01210), account-based authorization ultimately remains tied to the authority of the controlling key. EIP-7702 delegation expands the account's executable behavior, making it important to reason about both authorization and the state transitions that authorization can enable.
  • Mempool Frontrunning & Transaction Ordering: A recovery transaction can be logically correct but still lose a race if an attacker transaction is included first. Private transaction channels such as Flashbots Protect or MEV-Share can reduce public-mempool exposure, but they do not remove the need to reason about inclusion and ordering.
  • Deterministic Witnesses vs. Probabilistic Heuristics: A concrete, executable multi-step counterexample on an EVM state snapshot gives directly inspectable evidence of a modeled loss path, which is more informative than an unexplained scalar risk score for the same scenario.

What's next for Aegis7702

1. MetaMask Snap & Browser Extension Integration

Package the Aegis7702 reachability engine into a MetaMask Snap or browser extension to intercept eth_signTypedData_v4 and EIP-7702 authorization requests before the user signs them.

2. Expanding Action-Space Semantics (\(\mathcal{A}_{\text{modeled}}\))

Expand the candidate transition generator to model broader DeFi composability vectors, including Uniswap v3/v4 liquidity pools, Aave and Morpho collateral borrow/liquidate loops, and cross-chain bridge deposit contracts.

3. Direct Private Relay Integration

Integrate private transaction submission paths so the dashboard can dispatch recovery transactions with reduced public-mempool exposure and better control over transaction ordering.

4. Symbolic EVM Execution & SMT Integration

Explore symbolic EVM execution and formal-analysis tooling, such as Halmos or Certora Prover, to strengthen verification beyond the current bounded search depth and broaden the classes of behaviors that can be reasoned about.

Built With

  • account-abstraction
  • anvil
  • eip-712
  • eip-7702
  • erc-20
  • ethereum
  • flashbots-protect
  • formal-verification
  • foundry
  • mev-protection
  • pectra
  • permit2
  • reachability-analysis
  • react
  • smart-contract-security
  • solidity
  • solmate
  • tailwindcss
  • typescript
  • viem
  • vite
  • wallet-security
  • web3-security
Share this project:

Updates

Submission history