Quantitative Information Flow as Safety and Liveness Hyperproperties

TL;DR

This paper uses hyperproperties to classify and analyze the verification problems of quantitative information flow, extending previous results and introducing a new subclass called 'k-observable hyperproperties' that can be checked efficiently.

Contribution

It introduces 'k-observable hyperproperties' for quantitative information flow and provides a unified framework for their verification using hyperproperties.

Findings

Unified classification of verification problems

Identification of 'k-observable hyperproperties'

Verification via reachability oracle and self composition

Abstract

We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call "k-observable hyperproperties", that can be checked relative to a reachability oracle via self composition.