Everything Is a Program - Chapter 2 - Properties

Original post: here.

In the first post of this series we introduced a definition of what a program is that succinctly captures a universal concept. In the second post of the series, we discussed how all machines abstract and physical, are also programs via their configuration spaces.

Now, in this third series we will dive into the world of formal verification.

Properties

How could we have a discussion about some given program P? We could discuss what it does and/or what it does not do. But, how might we discuss the totality of what it is? Does there exist an abstract tool to utilize in capturing this? Yes. These tools are called: properties.

According to Defining Liveness by Alpern And Schneider a property is defined as such:

Def. 0 - Property - a set of sequences.

Interesting, that is exactly the definition of program that we provided in Chapter 0 of this series. But, the important part of this definition is found in the corollary:

Cor. 0 - a program P has a property ρ iff all sequences in P are also in ρ.

This is the critical part. So, “properties” in the world of formal verification are really nothing more than program comparisons.

This also implies the following:

Thrm 1. - the set of all programs ρ$^k$ that fully contain a given program P are the complete set of properties for the given program. Where “contains” is a comparison operation that shows an intersection between the set of sequences in P and the set of sequences in each program in ρ$^k$.

So, the blog post could end right here as it seems that the work has been done decades ago for me. But, for the fun of it, let’s dive into the properties of properties.

Existential vs. Universal

The basic way to interpret a property of a single-sequence is by asking a question or making an assertion and seeing if that question is properly answered and/or that assertion holds true.

1. Existentially: At some point within the sequence
2. Universally: At all points during the run of the sequence

Usually, negative properties (things a program should not do) are defined to be universal. Whereas, positive properties are often defined as a desirable “eventuality” during the sequence’s execution and are thus defined existentially.

But, positive and negative properties can be defined existentially or universally. For example, a negative existential property would be something that a program for sure does not do at least once (and for some duration) during its execution.

In the literature, there are two most commonly addressed property types:

Def. 1 - Safety Property - any universal negative property satisfied by a sequence is a safety property of said sequence

and also

Def. 2 - Liveness Property - any existential positive property satisfied by a sequence is a liveness property of said sequence. We say that the sequence “eventually” satisfies the positive property.

Technically, when we use the term “eventually” to define a liveness property it encompasses all universal positive properties since they satisfy “eventuality” from the start of the sequence. Thus, liveness “eventuality” generalizes across all positive properties. Also, an existential negative property could be inverted into being seen as an existential positive property (by claiming that the desired eventuality is “positive” because it is being looked for). Thus, liveness properties tend to cover a lot and lead to the conclusion (as seen in the literature) that all properties can be defined as an intersection of some set of liveness and safety properties.

Cor. 1 - All properties can be defined as the intersection of some set of liveness and safety properties

Personally, I feel that this is less clear than sticking with the categorization of properties via quantifiers and positive/negative qualifiers. Technically, we could classify properties however we felt like. Reductionism is neither always necessary nor always helpful. I digress.

Hyperproperties

There is actually a higher abstraction of a property that encompasses the concept of a property, and that abstraction is called (in the literature, not my name) hyperproperties.

Def. 1.0 - Hyperproperty - a set of properties

Perhaps, the best way to differentiate it from a property is that a hyperproperty is not a program, but rather a set of programs. More specifically, unlike a property which could be seen as a set of single-sequence programs, we can view a hyperproperty as a set of multi-sequence programs.

Def. 1.1 - Hyperproperty - a set of multi-sequence programs

And in this way it perhaps becomes clearer how a hyperproperty is technically a set of properties by being a set of programs (and all properties are programs themselves and vice/versa).

More technically, a program P satisfies a hyperproperty H if and only if P is an element of H.

A Hyperproperty is a relation on sequences. In fact, the hyperproperty “version” of a property ρ can be seen as the powerset of ρ. Which seems trivial when you realize that any k-subset of sequences of a property also satisfy that property.

For example, in Hyperproperties by Clarkson and Schneider they generalize the notion of safety properties to k-safety hyperproperties.

A k-safety hyperproperty is a safety property in which the specified negative property never involves more than k sequences.

Any k-safety hyperproperty of a program P is equivalent to a safety property of P$^k$ or all k-subsets of sequences of P. Thus, the set of all safety properties for P is the set of all 1-safety hyperproperties of P. The simplest way to think about it is the following: if we execute/run the program P k-times then we what are we guaranteed? If we are guaranteed a negative property to universally not exist in any k runs then we have k-safety for that negative property.

Applications/Examples of Hyperproperties:

• Security Policies
• Aggregate Stats (e.g., Average Response Time)
• Answering questions about changes to a system/program such as:
  • Was this a correct optimization?
  • Was this a correct refactoring?
  • Do two versions of code produce the same output for the same input?
• Various questions about distributed systems such as: Does the distributed system degrade by at most N% if one server goes down?

The last properties concept that I will simply make mention too but not discuss is the idea of (hyper)properties of non-deterministic programs. These can be seen as being applied to a Markov Model of some type and they are called:

Def. 2 - Probabilistic Hyperproperties - assume probabilities are on state transitions for a program, we can construct a probability measure on state transition sequences (paths over the state space) that allows for adding probabilities across individual sequences (total never exceeding 1), we then use this measure to express a hyperproperty.

Applications/Examples of Probabilistic Hyperproperties:

• Probabilistic Noninterference
• Quantitative Information Flow
• Differential Privacy

As you may have already noticed, most of the applications currently discussed in the literature around properties are security focused as a lot of formal verification research is applied towards information security i.e., it’s an economically beneficial application.

Further reading references are provided in the [References](about:blank##References) section below. It is encouraged to anyone even slightly interested in the topic to read the references. There are also multiple formal verification languages that are designed and used based on the concepts in the papers referenced. But be warned, that it is a world to be dived into so it won’t be for the faint-hearted.

Conclusions

The purpose of this blog post was not to dive into the world of formal verification nor to even provide a proper introduction to the world of properties.

It was to extend the multi-post series of the basic concept that everything is a program. Even if we desire to describe, define, or interpret the meaning of a program we can only do it in terms of other programs.

The specifics of how this is done will be discussed in a later post. But the teaser is that the assessment of whether a program has a property or not requires an interpreter. In other words, every property must be constructed via an interpreter (assigning an interpretation to every sequence both in and not within the property – as to “having” that property or not). But, since we noted that properties are just programs then don’t all programs require an interpreter to be constructed? Yes, and we will see how that proves even more so that everything is a program.

References

• Lamport - Proving the Correctness of Multiprocess Programs - 1977
• Alpern & Schneider - Defining Liveness - 1984
• Clarkson & Schneider - Hyperproperties - 2009
• Abraham and Bonakdarpour - HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties - 2018
• Wayne - Hypermodeling Hyperproperties - 2020 - an extra blog post worth considering

Series

Find the entire series here!