Ada 2022 / SPARK · provable immutability

Backups that cannot be deleted before they expire

dezhan is an air-gapped, immutable backup vault that speaks S3. Write an object under a retention and the vault refuses to delete or expire it early - and "refuses" is a state machine proved with gnatprove to have no path that deletes a retained object.

  • S3-compatible
  • Air-gapped
  • SPARK-proved
  • Kubernetes-native
dezhanctl demo: check health, store an object under a compliance retention, show its metadata, watch a delete-before-expiry be refused, then open the live dashboard
dezhanctl: store under retention, watch a delete-before-expiry be refused, then open the live dashboard.
Operate it

A live dashboard, not just an API.

dezhanctl is a control CLI with a live dashboard. It reads the vault's control plane (health, seal state, objects, audit chain, scrub) and needs no AWS SDK, so it works against a local or air-gapped server.

dezhanctl live dashboard showing health, seal state, object and audit counts, and the object list
Why dezhan

Most vaults promise immutability. dezhan proves it.

The modern ransomware playbook deletes the backups first, then encrypts. WORM and Object Lock exist to stop that - but only if the enforcement itself cannot be turned off. dezhan makes that enforcement a machine-checked theorem.

01

Provable, not configurable

The retention rule is a SPARK state machine, and gnatprove discharges every path on every commit: 325 checks, 0 unproved. "Immutable" is a property of the build, not a promise in a datasheet.

02

Speaks S3

Point aws-cli, restic, Veeam, Velero, or boto3 at the endpoint. Buckets, versioning, multipart, presigned URLs, SigV4, and Object Lock / WORM with legal hold - validated against the AWS SDK.

03

Air-gapped & self-verifying

No external runtime dependency. Data is content-addressed, encrypted, and erasure-coded; a background scrub verifies and self-heals, and every operation is written to an append-only, hash-chained audit log.

What it proves

Four invariants, machine-checked on every commit

The trusted core is written in SPARK. Each row below is expressed as a contract and discharged by gnatprove - the CI job fails on a single unproved check. Not tested. Proved.

Verified component Invariant it guarantees How
retention state machine Retention may be extended, never shortened; a retained object cannot be deleted before expiry SPARK contracts, discharged by gnatprove
clock-integrity guard A rewound or tampered system clock cannot expire a lock; the vault seals instead of releasing proved monotonic trusted time
append-only audit chain Every operation is hash-chained; recorded history cannot be rewritten undetectably proved append-only structure
erasure coding Data survives drive loss and reconstructs exactly, or is quarantined - never returned wrong proved reconstruction

The cryptography - SHA-256/512, ChaCha20, HMAC, Ed25519 - is implemented in-tree with no external runtime dependency, so the whole integrity path is auditable in one place.

Architecture

A single writer, formally guarded

A vault is one writer over durable storage - a single-replica StatefulSet on a ReadWriteOnce volume. The immutability and audit-chain guarantees assume one writer; cross-node durability comes from the StorageClass beneath it.

Three images, one code base

  • dezhan - the vault server. For a plain install this is all you need.
  • dezhan-operator - reconciles a DezhanVault CR into a StatefulSet, Service, PVC, and PodDisruptionBudget.
  • dezhan-csi - exposes a vault as PersistentVolumes, one bucket per PVC, via mountpoint-s3.

Measured, not asserted

The proof gate (scripts/prove.sh) fails the build on any unproved check. Throughput is measured on one VM with the same harness. dezhan trades write speed for durability and integrity: writes are deliberately slow (about 1.2 MB/s at 4 MiB, small objects fsync-bound near 1 op/s) while reads are faster (about 37 MB/s at 4 MiB). Unlike Veeam, which enforces immutability in the storage layer, dezhan proves the delete-before-expiry path unreachable in its trusted core. Per-chunk encrypt, hash and erasure-code work runs across the CPUs, and objects of any size store and restore.

Benchmark harness & results ↗
Install

Three ways to run dezhan

One on-prem binary, a Helm chart for the Kubernetes operator, or the image from GHCR. For a plain install you only need the server.

On-prem (one command)

curl --proto '=https' --tlsv1.2 -sSf \
  https://raw.githubusercontent.com/obsernetics/dezhan/main/install.sh | sh

Helm (Kubernetes operator)

helm repo add dezhan https://obsernetics.github.io/dezhan
helm repo update
helm install dezhan dezhan/dezhan

Container image (GHCR)

docker pull ghcr.io/obsernetics/dezhan:latest

Declare a vault

apiVersion: dezhan.obsernetics.io/v1alpha1
kind: DezhanVault
metadata:
  name: my-vault
spec:
  storage: 100Gi
  requireAuth: true
  deleteQuorum: 2                # deletes need 2 co-signatures
  secretName: my-vault-secrets   # DEZHAN_VAULT_KEY, DEZHAN_SECRET, ...

Reach the vault in-cluster at http://my-vault.<namespace>.svc:8080, then point any S3 client at it. Enabling Object Lock on a bucket makes it Immutable / WORM.

Immutability you can prove.

Write once, keep it honest: the delete-before-expiry path is machine-checked unreachable.