---
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

[![SPARK](https://img.shields.io/badge/SPARK-100%25%20proved-brightgreen)](bf_vm/)
[![License: Tri](https://img.shields.io/badge/license-AGPL%20%7C%20BSL%201.1%20%7C%20MIT-blue)](LICENSE)
[![GNATprove](https://img.shields.io/badge/GNATprove-0%20unproved-brightgreen)](bf_vm/)
[![Build](https://img.shields.io/badge/Rust%20FFI-Ada%20bridge-orange)](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