Regexes in the Z3 Theorem Prover
Analyzing Teleport RBAC
Posted on January 19, 2022
| Andrew Helwer
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]
Two pictures of quantum computation
Quantum interference in the sum-over-paths formalism
Posted on December 10, 2020
| Andrew Helwer
Interpretations of quantum mechanics are boring. Boring! Maybe the universe has a strict partition between quantum and non-quantum. Maybe there are a bunch of parallel universes with limited crosstalk. Or maybe it’s whatever the Bohmian mechanics people are talking about. Shut up and calculate, I think. I don’t say this out of some disdain for idle philosophizing or to put on airs of a salt-of-the-earth laborer in the equation mines. It’s just there are so, so many interesting things you can learn about in quantum theory without ever going near the interpretation question.
[Read More]
How do you reason about a probabilistic distributed system?
Posted on September 11, 2020
| Andrew Helwer
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]
Meditation
Sadly my only weapon against the attention economy
Posted on August 29, 2020
| Andrew Helwer
This isn’t going to be a post about how adopting a several-thousand-year-old practice can make you a better servant of capital. Instead, let’s talk about when I feel the lowest of the low. It comes after spending any number of hours on my computer, maybe even a full day, endlessly circling around different websites in search of stimulation, the quick jolt that comes with learning an interesting fact or watching a funny short video or seeing someone get dunked on for having a bad political opinion.
[Read More]
Taking my home work setup seriously
Ergonomics & settling in for the long haul
Posted on August 14, 2020
(Last modified on January 23, 2022)
| Andrew Helwer
The headlines don’t lie. Microsoft, Google, Amazon, Facebook, and a whole host of other tech companies have announced employees will be working from home until early-mid 2021. There are reasons to believe this will be pushed back; even if the staggeringly ambitious timelines for vaccine development are met, a vaccine might not be a silver bullet and the pandemic could require management for the next 2-3 years. As a software engineer in big tech’s orbit, this means it’s time to settle in for the long haul and take my home work setup seriously.
[Read More]
Doing a math assignment with the Lean theorem prover
Posted on April 5, 2020
| Andrew Helwer
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]
Simulating physical reality with a quantum computer
Quantum chemistry for complete beginners
Posted on December 21, 2019
| Andrew Helwer
Quantum Computers: Not Just for Breaking RSA There’s no denying it, Shor’s algorithm was a blockbuster result. The thought of an exotic new computer breaking all widely-used public-key crypto plays well with the public imagination, and so you’d be forgiven for believing quantum computing is ultimately a sort of billions-dollar make-work project for software engineers: forcing our profession to relive a Y2K-like mass upgrade of old systems to new, quantum-safe encryption algorithms.
[Read More]
Walking the faster-than-light tightrope
Quantum entanglement and the CHSH game
Posted on December 7, 2018
| Andrew Helwer
Measurement and signaling in the nonlocal world Popular understanding of quantum mechanics usually focuses on three learning objectives:
At small scales, particle properties (position, momentum, spin, etc.) are in superposition - they don’t have a definite value, but instead are “smeared” across multiple possible values. Measuring a superposed particle property makes it collapse probabilistically to a specific value. We don’t simply discover the property’s pre-existing value; rather the property is forced to take on a definite value by the act of measurement.
[Read More]
Checking Firewall Equivalence with Z3
Posted on February 13, 2018
| Andrew Helwer
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
Posted on February 12, 2018
| Andrew Helwer
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]