wal-postgresqldb

Made 🄯 libre (free as in freedom) with ❤️ at Politehnica University of Timișoara — quite possibly the first formally-verified (machine-checked proof of no run-time errors) PostgreSQL / TimescaleDB one-way WAL mirror for replicating a live database across an air gap. Built specifically for industrial control and SCADA — power grids, water treatment plants, oil & gas pipelines, railways, and telecommunications networks — where the historian must be readable from the corporate side without the corporate side being able to reach, or write to, the plant.

Because we care — and because critical-infrastructure protection should not depend on proprietary / closed-source systems, and should be made FREE.

A high-assurance Ada/SPARK PostgreSQL WAL mirror — PostgreSQL WAL archive shipping and real-time page streaming over a strictly one-way link, with the reconstruction path proved free of run-time errors and the integrity gate authenticated rather than merely checksummed.

On the name and TimescaleDB. This mirrors PostgreSQL's WAL, so it works for TimescaleDB exactly the same — TimescaleDB is a PostgreSQL extension, its hypertables and compression are ordinary WAL, replicated verbatim. Nothing here knows or cares which it is; "wal-postgresqldb" just names the engine whose write-ahead log crosses the diode.

Data flows one way through a data diode (a media converter with the TX fibre only). There is no return path: no ACK, no retransmission, no feedback. A standby replays what arrives and serves read-only SQL. Everything hard about this design follows from that one sentence.

Why a mirror is a good fit for a diode — and where it bites

PostgreSQL's WAL archive shipping is the only built-in replication mode that is inherently unidirectional: the primary's archive_command hands off a finished 16 MiB segment and does not care what happens next. Streaming replication, by contrast, needs the standby to report its flush LSN — a back-channel a diode cannot give it.

The bite: a permanently lost segment blocks the standby forever. PostgreSQL replays WAL in strict order, so a hole is not a gap you skip — it is a wall. With no retransmission, forward error correction is not an optimisation here, it is the whole ballgame.

Two payload sizes, two erasure codes

This is the design decision the project turns on, and it is not the obvious one.

Mode	Unit	Fragments	Code	Why
archive	16 MiB WAL segment	~12 400	LT fountain (K = 7375 × 1356 B)	At this K, a Reed-Solomon decode is an O(K³) matrix inversion over GF(2⁸) — roughly 10¹² operations. Infeasible. LT peeling is O(K log K), and a rateless code lets the sender keep emitting fresh coding symbols for a segment that has not decoded yet.
streaming	8 KiB WAL page	~7	Reed-Solomon over GF(2⁸)	At K ≈ 7 a fountain code's overhead buys nothing. RS is MDS: any K of K+M fragments rebuild the page exactly, with a hard guarantee rather than a probability.

Fountain codes are not "better" than Reed-Solomon; each is optimal in a different regime, and this project happens to span both. (The same reasoning, run the other way, is why the sibling project opc-diode uses RS and no fountain rung: an OPC UA message is capped at 64 KiB, so K ≤ 72, and LT would only add overhead.)

Both codes are fed AEAD-sealed bytes — encrypt-then-encode — so the erasure coder protects ciphertext, and a forged or mis-decoded packet fails its Poly1305 tag and is dropped, never replayed into the mirror.

What is proven, and why these particular things

The units this project adds are proved AoRTE by gnatprove: 224 checks, 0 unproved, 0 justified (./tools/prove.sh). They never name a socket, never allocate, and hold no global mutable state; the trusted shell hands them buffers and they hand back verdicts. This is the security-critical new code — the parsers that chew hostile bytes off the wire, the reassembler, and the AEAD position gate:

Unit	What it is, and the obligation it discharges
wal_envelope	The 256-byte archive header. Proves the filename is a safe path component — no /, no .., no NUL-splicing, non-empty. The receiver builds archive_dir/<filename> from a field that came off the wire; without this, ../../etc/cron.d/pwn is a write outside the archive. The shell may concatenate the name it gets from here without any further check — that obligation is discharged, not assumed.
wal_stream	The 44-byte page header. Proves the offset is page-aligned and inside the segment, so an attacker-chosen offset cannot become an out-of-bounds write; and applies the same path gate to the segment name.
wal_segment	Page reassembly. Is_Complete is a quantifier over the bitmap, not a counter. A counter that over-counted by one would finalize a segment with a zero-filled hole in it, and PostgreSQL would replay it as if it were sound — a silently corrupt mirror. Completeness is true by definition here, not by an arithmetic argument that could drift.
wal_sealed	Chunked AEAD (64 KiB chunks, since a 16 MiB object cannot be sealed at once). Binds each chunk's position into its nonce, because the tag alone does not stop an attacker replaying or reordering chunks that were legitimately sealed: chunk 5 of yesterday's segment carries a perfectly good tag. Splice it where chunk 3 belongs and you have corrupted a WAL segment using nothing but authentic material.
secure	The ChaCha20-Poly1305 wrapper over SPARKNaCl — proved AoRTE and proved to satisfy SPARKNaCl's preconditions, so the cryptographic strength is inherited, not re-established.

Vendored, proven upstream — relied on, not re-proved here. The three engines underneath are each proven in their own home and vendored verbatim, exactly as a trusted-but-proven dependency:

Engine	Source	Proof
LT fountain codec (lt_*)	gnat-lt-pro	175 checks, 0 unproved
Reed-Solomon codec + relay (gf256, rs, rs_matrix, relay, diode_wire)	opc-diode	part of its 387
ChaCha20-Poly1305 (deps/sparknacl)	SPARKNaCl (BSD)	its own published proof

All three are still exercised end-to-end for function by bin/test_core (byte-exact LT and RS round-trips, AEAD seal/open, the position-splice defence) — a different question from the safety the proof settles. Full boundary in docs/ASSURANCE.md.

Trusted, and unprovable by nature (SPARK_Mode Off): PostgreSQL itself, file and socket I/O, and inotify (for the streaming path). They stay in the shell, just as the socket/transport plumbing does in the sibling projects.

What changed from the C original, and why

Three things, all of them about not silently corrupting a database you cannot ask to resend.

MD5 → ChaCha20-Poly1305. The C envelope authenticated a segment with an MD5. MD5 is a corruption check, not an authenticator: on a one-way fibre, anyone able to inject frames can forge a WAL segment with a matching digest — and replaying WAL is arbitrary write access to the mirror database. The envelope is now sealed, and the header rides inside the sealed plaintext, so a tampered filename or sequence number breaks the tag.

The Python fountain coder is gone. The C version's lossy-link transport shelled out to datadiode-RobustSoliton — Python 3.11 + numpy, spawned as a subprocess, decoding hostile bytes off the fibre inside the trusted path. On critical infrastructure that is a large, unverified attack surface. It is replaced by gnat-lt-pro's proven codec: no Python, no numpy, and the decode path is AoRTE.

Streaming pages no longer rely on IP fragmentation. The C version sent 8 236-byte UDP datagrams (44 + 8192). Those are fragmented by IP into ~6 pieces, and losing one piece loses the whole page — on a lossy diode, precisely the wrong failure mode. Pages are now split into MTU-sized fragments with Reed-Solomon parity, so a lost fragment is recovered, not fatal.

Build, test, prove

Toolchain: GNAT 14.2.0 + gprbuild + gnatprove (SPARK). tools/env.sh puts them on PATH.

./tools/build.sh        # -> bin/  (bootstraps the vendored SPARKNaCl library once)
./tools/prove.sh        # gnatprove over this project's units: 224 checks, 0 unproved, 0 justified
./tools/check.sh        # build + proof + core sanity + archive-mode loopback
./tools/loopback-test.sh  # a 16 MiB segment across the diode: cleartext, encrypted, wrong-key

tools/prove.sh scopes the proof to the units written for this project; the LT and Reed-Solomon codecs and SPARKNaCl are vendored already-proven (see the table above and docs/ASSURANCE.md).

Running the mirror

The trusted shell is where the proven core meets sockets and PostgreSQL. Both replication paths are implemented and tested end-to-end — a 16 MiB WAL segment crosses the diode and is rebuilt byte-identical, in the clear and AEAD-encrypted, with a wrong key dropped.

Archive mode — whole 16 MiB segments as an LT fountain (reliable, MD5-verified-complete equivalent):

# low side (standby): recover segments into the archive directory
./bin/wt_arch_recv 9701 /var/lib/wal-mirror/archive <seed> [--key <64 hex>]

# high side (primary): PostgreSQL fires this per finished segment --
#   archive_command = 'wt_arch_send %p <standby_ip> 9701 <seed> --key <64 hex>'
./bin/wt_arch_send <segment_file> <standby_ip> 9701 <seed> [--key <64 hex>] [--overhead 1.6]

<seed> and the key are pre-shared out of band and must match; the diode has no back-channel, so --overhead (default 1.6) sets how many LT coding packets per K to blast.

Streaming mode — individual 8 KiB pages as Reed-Solomon fragments, for ~100 ms lag:

# low side: reassemble pages (2048-bit bitmap) and finalize whole segments
./bin/wt_stream_recv 9702 /var/lib/wal-mirror/staging /var/lib/wal-mirror/archive [--key <64 hex>]

# high side (production): watch pg_wal/, follow the current segment, rotate automatically
./bin/wt_stream_send /var/lib/postgresql/data/pg_wal <standby_ip> 9702 --pg-wal [--key <64 hex>] [--parity 3] [--interleave 16]

# high side (single file): follow one growing segment
./bin/wt_stream_send <segment_file> <standby_ip> 9702 --follow [--key <64 hex>]

--pg-wal tracks the current (highest-named) WAL segment in the directory, streams each 8 KiB page as it is written (~100 ms poll), and on rotation sends a SEGMENT_COMPLETE marker for the filled segment and switches to the next. A page is written to the standby only via the proven Is_Complete bitmap gate, so a segment with a hole is never published.

Each page is Reed-Solomon-protected into K data + --parity (M) fragments, so any M losses per page are recovered. Those N = K+M fragments would otherwise go out back-to-back — vulnerable to a burst. --interleave D buffers D pages and sends them column-major (fragment 1 of each, then fragment 2, …), so a burst of up to M×D consecutive losses still costs ≤ M per page and stays recoverable. D is capped at the receiver's in-flight capacity (16); the receiver needs no change — it regroups by page sequence whatever the order. (tools/burst-test.sh shows an 8-packet burst that corrupts a segment at --interleave 1 and is fully recovered at --interleave 16.) Both modes: with --key, each unit is ChaCha20-Poly1305-sealed (streaming uses a unique nonce per page) before it is coded, so a wrong key or any tampering is dropped, never written. The standby's restore_command = 'cp archive/%f %p' replays finalized segments.

Transports: UDP (default) or DPDK kernel-bypass (opt-in)

The proven core never names a socket, so the transport lives wholly in the trusted shell. The default is GNAT.Sockets UDP. An optional DPDK poll-mode backend moves the streaming daemons' packets as raw Ethernet frames (EtherType 0x88B8), bypassing the kernel:

DPDK_PREFIX=/path/to/dpdk-install WITH_DPDK=yes ./tools/build.sh   # or apt install libdpdk-dev
./tools/dpdk-test.sh                                               # memif end-to-end, no root/NIC

# then --with-dpdk --eal "<EAL args>" on both streaming ends (instead of a UDP port)
sudo ./bin/wt_stream_recv 0 <staging> <archive> --with-dpdk --eal "-l 0 -a 0000:03:00.0" [--key ...]
sudo ./bin/wt_stream_send <pg_wal> 0 0 --pg-wal --with-dpdk --eal "-l 1 -a 0000:03:00.0" [--key ...]

A default build is DPDK-free (nm finds zero rte_* symbols); --with-dpdk on it exits with "built without DPDK support". The trade: DPDK moves its EAL, mempool and NIC PMD — a large third-party C body — plus a small mandatory C shim (src/net/dpdk/wt_dpdk_shim.c) onto the data path inside the TCB, and real bypass (vfio-pci) also needs root, an IOMMU and a spare NIC. Safety and integrity are unaffected; what grows is what you trust (docs/ASSURANCE.md). Archive mode (one-shot per segment) stays UDP; DPDK is wired into the long-lived streaming daemons.

Running it for real on Intel 10G cards — the full vfio-pci recipe (IOMMU, hugepages, safely binding the spare NIC, building a DPDK with the Intel PMDs) is in KERNEL-BYPASS.txt, with tools/vfio-setup.sh (safe bind/unbind that refuses your SSH card) and tools/dpdk-build-nic.sh.

Licence

AGPL-3.0-or-later. Copyright © 2026 Alin-Adrian Anton. SPARKNaCl is BSD (© Protean Code Limited) and is vendored under deps/.