Verified Egress Inference (VEI)

Formerly "Logically Airgapped Inference" (LAGI)—a content-verified egress gate that blocks responses failing formal validation.

Formally verified network sentry for AI inference using eBPF data diodes.

For Apart's hackathon. See comms/whitepaper/main.pdf for motivation and background.

Quick Start

Prerequisites

Linux host with:

• Docker Engine with Compose V2
• Rust nightly toolchain with rust-src component
• bpf-linker for compiling eBPF
• Lean 4 via elan

Install Rust toolchain:

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
rustup install nightly
rustup component add rust-src --toolchain nightly
cargo install bpf-linker

Install Lean 4:

curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh

Step 1: Clone and enter repository

git clone <repo-url>
cd adversarial-network-tapped-inference-hackathon

Step 2: Download the muInference ISO

./enclaves/muenclave/scripts/download-iso.sh

This downloads the ~55MB bootable ISO that runs llama2.c inference.

Step 3: Build eBPF diodes

cd sentry
make
cd ..

This compiles eBPF filters to sentry/build/:

Rust diodes (reference implementations):

• rust_minimal.o - Printable ASCII check
• rust_json.o - JSON depth validation
• rust_hateless.o - Content filtering (blocks "hate")

Lean diodes (specification-derived):

• lean_json_start.o - Size < 1400, starts with {
• lean_json_prefix.o - Starts with { or [
• lean_printable16.o - First 16 bytes printable ASCII
• lean_printable64.o - First 64 bytes printable ASCII

Step 4: Start the stack

docker compose up -d

This starts:

• muenclave (172.30.0.11:8080) - QEMU VM running muInference
• sentry (host network, privileged) - eBPF filter attachment
• dashboard (localhost:8501) - Streamlit monitoring UI

Step 5: Open the dashboard

open http://localhost:8501

Or use curl to test directly:

curl -H "Content-Type: application/json" \
  http://172.30.0.11:8080/api/generate \
  -d '{"prompt": "Once upon a time", "wait_time": 10}'

Testing the Diode

With the hateless diode (default), content containing "hate" is blocked:

# This passes (no "hate" in response)
curl -H "Content-Type: application/json" \
  http://172.30.0.11:8080/api/generate \
  -d '{"prompt": "Once upon a time", "wait_time": 10}'

# This gets blocked (prompt echoed in response contains "hate")
curl -H "Content-Type: application/json" \
  http://172.30.0.11:8080/api/generate \
  -d '{"prompt": "I hate bananas", "wait_time": 10}'

Watch filter decisions:

docker logs -f lagi-sentry

Architecture

┌─────────────────────────────────────────────────────────────────┐
│                       DOCKER HOST                                │
│                                                                  │
│   ┌────────────────────────────────────────────────────────┐    │
│   │           Docker Bridge: 172.30.0.0/24                  │    │
│   │                                                         │    │
│   │   ┌──────────────┐       veth       ┌──────────────┐   │    │
│   │   │   sentry     │◄─────────────────►│  muenclave   │   │    │
│   │   │              │    TC FILTER      │ 172.30.0.11  │   │    │
│   │   │ - Rust eBPF  │    ATTACHED HERE  │              │   │    │
│   │   │ - hateless   │                   │ - QEMU VM    │   │    │
│   │   │   diode      │                   │ - llama2.c   │   │    │
│   │   └──────────────┘                   └──────────────┘   │    │
│   │                                                         │    │
│   └────────────────────────────────────────────────────────┘    │
│                                                                  │
│   ════════════════════════════════════════════════════════════  │
│                      HOST KERNEL                                 │
│                 eBPF filters run HERE                            │
└─────────────────────────────────────────────────────────────────┘

Components

Component	Description
sentry/	eBPF diode implementations (Rust/Aya) + Lean 4 specifications
enclaves/muenclave/	QEMU VM running muInference ISO with VNC+OCR API
dash/	Streamlit dashboard for interactive testing
tests/	End-to-end test suite and configuration

Available Diodes

Rust (reference implementations):

Diode	Property Checked	Use Case
rust_minimal.o	Printable ASCII (first 16 bytes)	Baseline sanity
rust_json.o	JSON depth ≤ 2	Structural validation
rust_hateless.o	No "hate" in first 512 bytes	Content filtering

Lean (specification-derived):

Diode	Property Checked	Use Case
lean_json_start.o	Size < 1400, starts with {	JSON object filter
lean_json_prefix.o	Starts with { or [	JSON value filter
lean_printable16.o	First 16 bytes printable	ASCII sanity
lean_printable64.o	First 64 bytes printable	Extended ASCII sanity

Commands

# Start everything
docker compose up -d

# Stop everything
docker compose down

# View sentry logs
docker logs -f lagi-sentry

# Rebuild after code changes
cd sentry && make && cd ..
docker compose restart sentry

# Run Lean specification tests
cd sentry/spec && lake build

Troubleshooting

"rust_hateless.o not found" or "lean_*.o not found"

cd sentry && make

"muinference.iso not found"

./enclaves/muenclave/scripts/download-iso.sh

Container unhealthy

docker compose down
docker compose up -d
docker ps  # Check health status

Permission denied (eBPF)

The sentry container requires privileged: true and host network mode. Ensure Docker has appropriate permissions.

Formal Verification

The sentry/spec/ directory contains Lean 4 specifications and a compiler that generates eBPF bytecode directly from formally specified predicates. The Lean-compiled diodes (lean_*.o) are built alongside the Rust reference implementations.

See sentry/spec/CLAUDE.md for details on the verification architecture and predicate DSL.