Regexes in the Z3 Theorem Prover

Analyzing Teleport RBAC

Republished from Teleport’s official blog (link). I received compensation from Teleport for writing this post. Z3 is a satisfiability modulo theories (SMT) solver developed by Microsoft Research. With a description like that you’d expect it to be restricted to esoteric corners of the computerized mathematics world, but it’s made impressive inroads addressing conventional software engineering needs: analyzing network ACLs and firewalls in Microsoft Azure, for example. Z3 is used to answer otherwise-unanswerable questions like “are these two firewalls equivalent? [Read More]

How do you reason about a probabilistic distributed system?

In which I am stunted upon by coin flips Wasn’t too long ago that I felt pretty good about my knowledge of distributed systems. All someone really needed in order to understand them, I thought, was a thorough understanding of the paxos protocol and a willingness to reshape your brain in the image of TLA+. Maybe add a dash of conflict-free replicated datatypes, just so you know what “eventual consistency” means. [Read More]

Doing a math assignment with the Lean theorem prover

Turn back the clock to 2009: a confused physics major newly infatuated with math and computer science, I enrolled in MATH 273: Numbers and Proofs at the University of Calgary. This wasn’t my first encounter with mathematical proof; in first-year calculus I’d mastered rote regurgitation of delta-epsilon proofs. Despite writing out several dozen, their meaning never progressed beyond a sort of incantation I can summon to this day (for every \( \epsilon > 0 \) there exists a \( \delta > 0 \) such that…). [Read More]

Checking Firewall Equivalence with Z3

Lessons I’ve learned from software engineering are uniformly cynical: Abstraction almost always fails; you can’t build something on top of a system without understanding how that system works. Bleeding-edge methods are a recipe for disaster Everything good is hype and you’ll only ever get a small fraction of the utility being promised. Imagine my surprise, then, when the Z3 constraint solver from Microsoft Research effortlessly dispatched the thorniest technical problem I’ve been given in my short professional career. [Read More]

Formal Verification, Casually Explained

Written during an interesting time in my life

Why are we here? What guarantees does formal verification provide? This question rests at the apex of a hierarchy of inquiry extending all the way down to how we can know anything at all! What do we mean by software correctness? There are precisely two different ways for a piece of software to be correct: The supreme deity of the universe descends from the heavens and decrees, with all the weight of Objective Truth, that a certain piece of software is correct. [Read More]