Author:

Keywords:

Hyperproperties, Coinductive verification, Coinductive predicates, Incremental hyperproperties, Holistic hyperproperties, Security, Games

Abstract:

The importance of security and reliability of software systems makes formal methods of paramount significance for guaranteeing that a system satisfies a particular specification. Hyperproperties can be seen as an abstract formalization of security policies. Because of this, it is desirable to establish a generic verification methodology for at least the class of security-relevant hyperproperties. Unfortunately, such a generic verification methodology is lacking. This is the main motivation of this dissertation.We observe that most interesting hyperproperties that are relevant in practice come from a class of security-relevant policies, specified using universal and possibly existential quantification on traces, as well as relations on those traces. We formalize such definitions and call them holistic hyperproperties. Then our goal becomes to find a methodology for the verification of holistic hyperproperties. To that end, we explore an incremental, coalgebraic perspective on systems and specifications and as a result we arrive at a different, but related kind of specifications: incremental hyperproperties (essentially coinductive predicates). Given some holistic hyperproperty H, the respective incremental version is called H′ and its definition naturally gives the notion of an H′-simulation relation. Such relations enable verification of holistic hyperproperties: finding an H′-simulation relation on a candidate system implies that the incremental hyperproperty H′ holds and thus the high-level, holistic hyperproperty H holds for the candidate system. We also introduce techniques that are often helpful in translating holistic hyperproperties into incremental ones.To show that incremental hyperproperties are important in practice, we explore their connection with the most closely related verification technique — via unwinding. To achieve this, we propose a framework for coinductive unwinding of security relevant hyperproperties based on Mantel’s MAKS framework and our work on holistic and incremental hyperproperties. Mantel’s MAKS framework cannot be used directly as it is geared towards reasoning about finite behavior and is thus not suitable to reason about holistic hyperproperties in general. However, our framework has a similar structure to MAKS: coinductive unwinding relations compose (or imply) coinductive Basic Security Predicates, which in turn compose a number of security-relevant, holistic hyperproperties. It turns out that the coinductive unwinding relations we introduce are instances of H′-simulation relations. More importantly, incremental hyperproperties can be expressed in well-behaved logics and this opens the door to their verification.Finally, we propose a generic verification approach for incremental hyperproperties via game-based model checking. To achieve this, we first show how to interpret incremental hyperproperty checking as games. Although one might do regular model checking of incremental hyperproperties on a transformed system, model checking games are advantageous as they do not only produce a yes-no answer, but also give more intuition about the security policy and what can potentially go wrong, by producing a concrete winning strategy. In order to show that the theory developed here is practical, we present and illustrate methods of using several off-the-shelf tools for verification of incremental hyperproperties expressed in the polyadic modal mu-calculus.