Source: github.com/SNAPKITTYWEST/bf-jwt-policy

BF-JWT-Policy

Authors: Ahmad Ali Parr, Jessica L. Williams (SNAPKITTYWEST)

RIP Black Hat. Cipher. Quantum Hacker.
Every great system must be destroyed to stand strong.

BF256 (Brainfuck as a cryptographic primitive) was attacked, broken via linear algebra in O(n³), and replaced with the correct architecture.

---

The Architecture

JWT signature: HS256/ES256 (standard, secure)
    ↓
SPARK-verified Brainfuck VM (bf_vm/)
    ↓
BF program = authorization POLICY (not a key)
    ↓
GNATprove: 100% proved, 0 checks failed

Critical distinction:

Wrong	Right
BF as crypto key	BF as policy program
BF256 signature	Standard HS256/ES256 signature
Secret = initial tape	Secret = HMAC key
Broken in O(n³)	SPARK-verified correct

---

Why BF256 Was Broken

BF + and - operations are affine transformations over ℤ/256ℤ. With 2 known (message, signature) pairs:

sig₁ = Affine(secret_tape, hash(m₁))
sig₂ = Affine(secret_tape, hash(m₂))

Solve for secret_tape via linear algebra. O(n³) where n = tape size (typically < 100 cells). Total break.

Ahmad found this himself. Documented it. Built the correct thing.

---

What's Correct

The Brainfuck VM is Turing-complete, minimal, and formally verifiable. Used as a policy evaluation engine — not a crypto primitive — it's:

• Memory safe — no buffer overflows (SPARK proved)
• Terminating — step counter decreasing invariant (SPARK proved)
• Deterministic — same input → same output (SPARK proved)
• Non-interfering — secret inputs don't leak to public outputs (SPARK proved)

---

GNATprove Results

Summary: 100% proved, 0 checks failed, 0 checks unproved

All overflow checks, index checks, termination, and postconditions proved.

---

Quick Start

# Prove SPARK
cd bf_vm && gnatprove -P bf_vm.gpr --level=2 --report=all

# Build Rust (compiles Ada + FFI)
cd ../bf_jwt_policy && cargo build --release

# Run demo
cargo run --example jwt_policy_demo

Expected:

✅ Authorized! Context: PolicyContext { role: Admin, ... }
❌ User denied: Access denied by policy

---

License

Tri-license — AGPL-3.0 | BSL 1.1 → MIT | MIT
Copyright (C) 2026 Ahmad Ali Parr, Jessica L. Williams / SNAPKITTYWEST

💼 Commercial License

Snapkitty code is free and open under AGPL-3.0 for open-source use. Building a commercial product or service? A proprietary commercial license from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.

→ Get a commercial license · A.parr@belespritdaccord.uk