TLA+ has a small number of data structures — sets, functions, sequences, and records — but they compose into surprisingly expressive models. If you’ve read the introductory article and seen the bas...
The introductory article covered the fundamentals — state machines, PlusCal syntax, invariants, and basic model checking. This picks up where that left off. We’ll get into refinement mappings, spec...
Unit tests check that your code does the right thing for specific inputs you thought of. Property-based tests check that your code does the right thing for hundreds or thousands of inputs the compu...
Every module on a YubiKey has its own PIN, its own retry limit, and its own consequences when you get it wrong too many times. Some lock you out of a single function. Others wipe the entire module....
TLA+ is a formal specification language for designing and verifying concurrent and distributed systems. PlusCal is an algorithm language that compiles to TLA+, giving you a more familiar imperative...
You know what the kernel does. You know what GNOME does. But how does a framebuffer in kernel memory become pixels managed by Mutter? How does a USB interrupt from your keyboard become a keypress i...
This is a walkthrough of building a working Linux desktop environment entirely from source — the kernel, Xorg display server, and a full GNOME desktop with its filesystem stack. No package manager,...
The GPG fundamentals post covered key hierarchy, subkey generation, and YubiKey integration. This post goes deeper — Web of Trust mechanics, subkey rotation without breaking trust, air-gapped prima...
The first post covered the YubiKey 5C modules and basic hardening. The GPG post walked through subkeys and OpenPGP integration. This post goes deeper — PIV-based SSH and TLS, FIDO2 resident keys, d...
GPG (GNU Privacy Guard) is the open-source implementation of the OpenPGP standard. It handles encryption, signing, and authentication using a hierarchical key structure. Pairing it with a YubiKey m...