Incremental Hyperproperty Model Checking via Games

Hyper-properties were proposed as an abstract formalization of security policies, but unfortunately they lack a generic verification methodology. In an attempt to remedy this, the authors introduced the notion of Incremental Hyper-Properties (IHPs), motivated by the observation that they have a clearer and more feasible verification methodology. To show that verification is indeed feasible, a decidable IHP verification methodology via games is presented and evaluated. The main advantage of the approach is that the games in combination with winning strategy evidence give valuable intuition about the security of a system and are very helpful when analyzing systems w.r.t. policy specifications.

Provided by: Katholieke Universiteit Leuven Topic: Security Date Added: Jul 2013 Format: PDF

Find By Topic