Hyperproperties

One tier worse than regular properties.

I wrote about hyperproperties on my blog four years ago, but now an intriguing client problem got me thinking about them again.¹

We're using TLA+ to model a system that starts in state A, and under certain complicated conditions P, transitions to state B. They also had a flag f that, when set, used a different complicated condition Q to check the transitions. As a quick decision table (from state A):

The interesting bit is the second-to-last row: Q has to be strictly more permissible than P. The client wanted to verify the property that "the system more aggressively transitions when f is set", ie there is no case where the machine transitions only if f is false.

Regular system properties are specified over states in a single sequence of states (behaviors). Hyperproperties can hold over sets of sequences of states. Here the hyperproperties are:

1. For any two states X and Y in separate behaviors, if the only difference in variable-state between X and Y is that X.f = TRUE, then whenever Y transitions to B, so does X.
2. There is at least one such case where X transitions and Y does not.

That's pretty convoluted, which is par for the course with hyperproperties! It makes a little more sense if you have all of the domain knowledge and specifics.

The key thing is that makes this a hyperproperty is that you can't just look at individual behaviors to verify it. Imagine if, when f is true, we never transition to state B. Is that a violation of (1)? Not if we never transition when f is false either! To prove a violation, you need to find a behavior where f is false and the state is otherwise the same and we transition to B anyway.

Aside: states in states in states

I dislike how "state" refers to three things:

1. The high-level "transition state" of a state-machine
2. A single point in time of a system (the "state space")
3. The mutable data inside your system's machine.

These are all "close" to each other but just different enough to make conversations confusing. Software is pretty bad about reusing colloquial words like this; don't even get me started on the word "design".

There's a reason we don't talk about hyperproperties

Or three reasons. First of all, hyperproperties make up a vanishingly small percentage of the stuff in a system we care about. We only got to "f makes the system more aggressive" after checking at least a dozen other simpler and more important not-hyper properties.

Second, most formal specification languages can't express hyperproperties, and the ones that can are all academic research projects. Modeling systems is hard enough without a generalized behavior notation!

Third, hyperproperties are astoundingly expensively to check. As an informal estimation, for a state space of size N regular properties are checked across N individual states and 2-behavior hyperproperties (2-props) are checked across N² pairs. So for a small state space of just a million states, the 2-prop needs to be checked across a trillion pairs.

These problems don't apply to "hyperproperties" of functions, just systems. Functions have a lot of interesting hyperproperties, there's an easy way to represent them (call the function twice in a test), and quadratic scaling isn't so bad if you're only testing 100 inputs or so. That's why so-called metamorphic testing of functions can be useful.

Checking Hyperproperties Anyway

If we do need to check a hyperproperty, there's a few ways we can approach it.

The easiest way is to cheat and find a regular prop that implies the hyperproperty. In client's case, we can abstract P and Q into pure functions and then test that there's no input where P is true and Q is false. In TLA+, this would look something like

\* TLA+
QLooserThanP ==
  \A i1 \in InputSet1, i2 \in Set2: \* ...
    P(i1, i2, …) => Q(i1, i2, …)

Of course we can't always encapsulate this way, and this can't catch bugs like "we accidentally use P even if f is true". But it gets the job done.

Another way is something I talked about in the original hyperproperty post: lifting specs into hyperspecs. We create a new spec that initializes two copies of our main spec, runs them in parallel, and then compares their behaviors. See the post for an example. Writing a hyperspec keeps us entirely in TLA+ but takes a lot of work and is very expensive to check. Depending on the property we want to check, we can sometimes find simple optimizations.

The last way is something I explored last year: dump the state graph to disk and treat the hyperproperty as a graph property. In this case, the graph property would be something like

Find all graph edges representing an A → B transition. Take all the source nodes of each where f = false. For each such source node, find the corresponding node that's identical except for f = true. That node should be the source of an A → B edge.

Upside is you don't have to make any changes to the original spec. Downside is you have to use another programming language for analysis. Also, analyzing graphs is terrible. But I think this overall the most robust approach to handling hyperproperties, to be used when "cheating" fails.

What fascinates me most about this is the four-year gap between "I learned and wrote about hyperproperties" and "I have to deal with hyperproperties in my job." This is one reason learning for the sake of learning can have a lot of long-term benefits.

Blog Rec

This week's rec is Robert Heaton. It's a "general interest" software engineering blog with a focus on math, algorithms, and security. Some of my favorites:

• Preventing impossible game levels using cryptography and the whole "Steve Steveington" series
• I was 7 words away from being spear-phished is a great deep dive into one targeted scam
• Making peace with Simpson's Paradox is the best explanation of Simpson's Paradox I've ever read.

Other good ones are PySkyWiFi: completely free, unbelievably stupid wi-fi on long-haul flights and How to pass a coding interview with me. The guy's got breadth.

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.