| --- |
| license: other |
| license_name: snapkitty-tri-license |
| license_link: https://huggingface.co/Snapkitty/bf-jwt-policy/blob/main/LICENSE |
| tags: |
| - snapkitty |
| - cryptography |
| - python |
| --- |
| |
| > Source: [github.com/SNAPKITTYWEST/bf-jwt-policy](https://github.com/SNAPKITTYWEST/bf-jwt-policy) |
|
|
| # BF-JWT-Policy |
|
|
| [](bf_vm/) |
| [](LICENSE) |
| [](bf_vm/) |
| [](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 |
|
|
| ```bash |
| # 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](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20bf-jwt-policy)** · A.parr@belespritdaccord.uk |
|
|
