I am reading the paper Foundations and tools for the static analysis of Ethereum contracts, by Grischenko et al. Sometimes the authors speak about hyper properties (e.g. Section 5). What exactly is a hyper property in this context?


A trace is a (finite or infinite) sequence of program steps. (Some works only consider finite traces, or only infinite ones.)

A property is a set of traces. E.g. all those traces where variable $x$ is never negative.

A hyperproperty is a set of sets of traces. E.g. the sets of traces $T$ where each trace in $T$ is finite.

Some complex security goals can not be described as a property. Non-interference, for instance, can not be checked on a single trace, but only on the set of all the possible traces a given system can generate during execution.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.