Model Checking Quantitative Hyperproperties

TL;DR

This paper introduces a new model checking algorithm for quantitative hyperproperties expressed in HyperLTL, significantly improving efficiency by using model-counting techniques, and demonstrates its practical viability on systems with information flow constraints.

Contribution

It presents a novel model checking algorithm based on model-counting for quantitative hyperproperties in HyperLTL, reducing complexity and enabling practical analysis.

Findings

New algorithm reduces model checking complexity exponentially or doubly exponentially.

Prototype implementation successfully analyzes systems with quantitative information flow.

Counting approach is feasible for systems like passcode checkers.

Abstract

Hyperproperties are properties of sets of computation traces. In this paper, we study quantitative hyperproperties, which we define as hyperproperties that express a bound on the number of traces that may appear in a certain relation. For example, quantitative non-interference limits the amount of information about certain secret inputs that is leaked through the observable outputs of a system. Quantitative non-interference thus bounds the number of traces that have the same observable input but different observable output. We study quantitative hyperproperties in the setting of HyperLTL, a temporal logic for hyperproperties. We show that, while quantitative hyperproperties can be expressed in HyperLTL, the running time of the HyperLTL model checking algorithm is, depending on the type of property, exponential or even doubly exponential in the quantitative bound. We improve this complexity with a new model checking algorithm based on model-counting. The new algorithm needs only logarithmic space in the bound and therefore improves, depending on the property, exponentially or even doubly exponentially over the model checking algorithm of HyperLTL. In the worst case, the new algorithm needs polynomial space in the size of the system. Our Max#Sat-based prototype implementation demonstrates, however, that the counting approach is viable on systems with nontrivial quantitative information flow requirements such as a passcode checker.

Figures

Tables

Table 1. Table 1: Comparison between the expansion-based approach (MCHyper) and the Max#Sat-based approach (MCQHyper). #max is the number of maximization variables (set Y 𝑌 Y ). #count is the number of the counting variables (set X 𝑋 X ). TO indicates a time-out after 1 hour.

Benchmark	Specification	MCHyper				MCQHyper
		#Latches	#Gates	#Quan.	Time(sec)	#max	#count	Time(sec).
Pwd_8bit	1bit_leak	9	55	2	0.3	16	2	1
	2bit_leak			4	0.4	32	4	1
	3bit_leak			8	1.3	64	8	2
	4bit_leak			16	97	128	16	4
	5bit_leak			32	TO	256	32	8
	6bit_leak			64	TO	512	64	335
	8bit_leak			256	TO	2048	256	TO

Equations

$$\forall {\pi }_1.\dots \forall {\pi }_k.\phi \to (\#\sigma :X.\psi ◃n),$$

$$\forall \pi .\#\sigma :O.\text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}(\pi {=}_I\sigma )\le 2^c$$

$$\psi$$

$$\phi$$

$$\Pi {\models }_T\exists \pi .\psi$$

$$\Pi {\models }_T\forall \pi .\psi$$

$$\Pi {\models }_T{a}_{\pi }$$

$$\Pi {\models }_T\neg \psi$$

$$\Pi {\models }_T{\psi }_1\vee {\psi }_2$$

$$\Pi {\models }_T\text{leavevmode}to7.41pt\text{vbox}to7.41pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11943ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt2.58333pt\text{pgfsys@moveto}3.44443pt2.58333pt\text{pgfsys@curveto}3.44443pt4.48566pt1.90233pt6.02776pt0.0pt6.02776pt\text{pgfsys@curveto}-1.90233pt6.02776pt-3.44443pt4.48566pt-3.44443pt2.58333pt\text{pgfsys@curveto}-3.44443pt0.681pt-1.90233pt-0.8611pt0.0pt-0.8611pt\text{pgfsys@curveto}1.90233pt-0.8611pt3.44443pt0.681pt3.44443pt2.58333pt\text{pgfsys@closepath}\text{pgfsys@moveto}0.0pt2.58333pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}\psi$$

$$\Pi {\models }_T{\psi }_{1}U{\psi }_2$$

$$\text{and for all}0\le j<i\text{we have}\Pi [j,\infty ]{\models }_T{\psi }_1$$

$$\forall {\pi }_1,\dots ,{\pi }_k.\phi \to (\#\sigma :A.\psi ◃n)$$

$$\#\sigma :O.true\le 2^c$$

$$\forall \pi .\#\sigma :O.(\text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}(\pi {=}_I\sigma ))\le 2^c$$

$$\forall \pi .\#\sigma :I.(\text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}(\pi {=}_O\sigma ))>n$$

$$\forall {\pi }_1,\dots ,{\pi }_k.\forall {\pi }_1^{\prime },\dots ,{\pi }_{n+1}^{\prime }.\left({\psi }_{\iota }\wedge \underset{i\ne j}{\bigwedge }\text{leavevmode}to8.7pt\text{vbox}to8.7pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.76527ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt2.58333pt\text{pgfsys@lineto}4.09026pt6.67358pt\text{pgfsys@lineto}8.18053pt2.58333pt\text{pgfsys@lineto}4.09026pt-1.50694pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}({\pi }_i^{\prime }{\ne }_A{\pi }_j^{\prime })\right)\to \left(\underset{i}{\bigvee }\neg \psi [\sigma \mapsto {\pi }_i^{\prime }]\right)$$

$$\forall {\pi }_1,\dots ,{\pi }_k.\exists {\pi }_1^{\prime },\dots ,{\pi }_n^{\prime }.{\psi }_{\iota }\to \left(\underset{i\ne j}{\bigwedge }\text{leavevmode}to8.7pt\text{vbox}to8.7pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.76527ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt2.58333pt\text{pgfsys@lineto}4.09026pt6.67358pt\text{pgfsys@lineto}8.18053pt2.58333pt\text{pgfsys@lineto}4.09026pt-1.50694pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}({\pi }_i^{\prime }{\ne }_A{\pi }_j^{\prime })\right)\wedge \left(\underset{i}{\bigwedge }\psi [\sigma \mapsto {\pi }_i^{\prime }]\right)$$

$$\forall \pi .\#\sigma :O.\text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}(\pi {=}_I\sigma )\le 2^c,$$

$$\forall {\pi }_0.\forall {\pi }_1\dots \forall {\pi }_{2^c}.\left(\underset{i}{\bigwedge }\text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}({\pi }_i{=}_I{\pi }_0)\right)\to \left(\underset{i\ne j}{\bigvee }\text{leavevmode}to6.97pt\text{vbox}to6.97pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11945ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@roundjoin}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt-0.86111pt\text{pgfsys@lineto}0.0pt5.5972pt\text{pgfsys@lineto}6.45831pt5.5972pt\text{pgfsys@lineto}6.45831pt-0.86111pt\text{pgfsys@closepath}\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}({\pi }_i{=}_O{\pi }_j)\right).$$

$$\phi =\forall {\pi }_1,\dots ,{\pi }_k.{\psi }_{\iota }\to (\#\sigma :A.\psi ◃n)$$

$$\exists {\pi }_1,\dots ,{\pi }_k.{\psi }_{\iota }\wedge (\#\sigma :A.\psi \overline{◃}n)$$

$$\underset{{\sigma }_Y\in (2^Y{)}^{\omega }}{\max }|\{{\sigma }_X\in (2^X{)}^{\omega }\mid \exists {\sigma }_Z\in (2^Z{)}^{\omega }.{\sigma }_X\cup {\sigma }_Y\cup {\sigma }_Z\in L(B)\}|$$

$$\varphi =\underset{i\le k}{\bigwedge }[[K{]]}_{\mu }^{{\pi }_i}\wedge [[K{]]}_{\mu }^{\sigma }\wedge [[{\psi }_{\iota }{]]}_{\mu }^0\wedge [[\psi {]]}_{\mu }^0$$

Full text

1 Introduction

Model checking algorithms [17] are the cornerstone of computer-aided verification. As their input consists of both the system under verification and a logical formula that describes the property to be verified, they uniformly solve a wide range of verification problems, such as all verification problems expressible in linear-time temporal logic (LTL), computation-tree logic (CTL), or the modal $\mu$-calculus. Recently, there has been a lot of interest in extending model checking from standard trace and tree properties to information flow policies like observational determinism or quantitative information flow. Such policies are called hyperproperties [21] and can be expressed in HyperLTL [18], an extension of LTL with trace quantifiers and trace variables. For example, observational determinism [47], the requirement that any pair of traces that have the same observable input also have the same observable output, can be expressed as the following HyperLTL formula: $\forall\pi.\forall\pi^{\prime}.\,(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\pi=_{I}{\pi^{\prime}})\rightarrow(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\pi=_{O}{\pi^{\prime}})$. For many information flow policies of interest, including observational determinism, there is no longer a need for property-specific algorithms: it has been shown that the standard HyperLTL model checking algorithm [26] performs just as well as a specialized algorithm for the respective property.

The class of hyperproperties studied in this paper is one where, by contrast, the standard model checking algorithm performes badly. We are interested in quantitative hyperproperties, i.e., hyperproperties that express a bound on the number of traces that may appear in a certain relation. A prominent example of this class of properties is quantitative non-interference [43, 45], where we allow some flow of information but, at the same time, limit the amount of information that may be leaked. Such properties are used, for example, to describe the correct behavior of a password check, where some information flow is unavoidable (the password was incorrect''), and perhaps some extra information flow is accceptable (the password must contain a special character''), but the information should not suffice to guess the actual password. In HyperLTL, quantitative non-interference can be expressed [18] as the formula $\forall\pi_{0}.\ \forall\pi_{1}\ldots\forall\pi_{2^{c}}.~{}\left(\bigwedge_{i}\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}({\pi_{i}}=_{I}{\pi_{0}})\right)\rightarrow\left(\bigvee_{i\neq j}\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}({\pi_{i}}=_{O}{\pi_{j}})\right).$ The formula states that there do not exist $2^{c}+1$ traces (corresponding to more than $c$ bits of information) with the same observable input but different observable output. The bad performance of the standard model checking algorithm is a consequence of the fact that the $2^{c}+1$ traces are tracked simultaneously. For this purpose, the model checking algorithm builds and analyzes a $(2^{c}+1)$-fold self-composition of the system.

We present a new model checking algorithm for quantitative hyperproperties that avoids the construction of the huge self-composition. The key idea of our approach is to use counting rather than checking as the basic operation. Instead of building the self-composition and then checking the satisfaction of the formula, we add new atomic propositions and then count the number of sequences of evaluations of the new atomic propositions that satisfy the specification. Quantitative hyperproperties are expressions of the following form:

[TABLE]

where $\triangleleft\in\{\leq,<,\geq,>,=\}$. The universal quantifiers introduce a set of reference traces against which other traces can be compared. The formulas $\varphi$ and $\psi$ are HyperLTL formulas. The counting quantifer $\#\sigma:X.\,\psi$ counts the number of paths $\sigma$ with different valuations of the atomic propositions $X$ that satisfy $\psi$. The requirement that no more than $c$ bits of information are leaked is the following quantitative hyperproperty:

[TABLE]

As we show in the paper, such expressions do not change the expressiveness of the logic; however, they allow us to express quantitative hyperproperties in exponentially more concise form. The counting-based model checking algorithm then maintains this advantage with a logarithmic counter, resulting in exponentially better performance in both time and space.

The viability of our counting-based model checking algorithm is demonstrated on a Max#SAT-based prototype implementation. For quantitative hyperproperties of intrest, such as bounded leakage of a password checker, our algorithm shows promising results, as it significantly outperforms existing model checking approaches.

1.1 Related Work

Quantitative information-flow has been studied extensively in the literature. See, for example, the following selection of contributions on this topic: [43, 34, 19, 14, 1, 32]. Multiple verification methods for quantitative information-flow were proposed for sequential systems. For example, with static analysis techniques [15], approximation methods [35], equivalence relations [22, 3], and randomized methods [35]. Quantitative information-flow for multi-threaded programs was considered in [11].

The study of quantitative information-flow in a reactive setting gained a lot of attention recently after the introduction of hyperproperties [21] and the idea of verifying the self-composition of a reactive system [6] in order to relate traces to each other. There are several possibilities to measure the amount of leakage, such as Shannon entropy [24, 15, 37], guessing entropy [34, 3], and min-entropy [43]. A classification of quantitative information-flow policies as safety and liveness hyperproperties was given in [46]. While several verification techniques for hyperproperties exists [5, 31, 38, 42], the literature was missing general approaches to quantitative information-flow control. SecLTL [25] was introduced as first general approach to model check (quantitative) hyperproperties, before HyperLTL [18], and its corresponding model checker [26], was introduced as a temporal logic for hyperproperties, which subsumes the previous approaches.

Using counting to compute the number of solutions of a given formula is studied in the literature as well and includes many probabilistic inference problems, such as Bayesian net reasoning [36], and planning problems, such as computing robustness of plans in incomplete domains [40]. State-of-the-art tools for propositional model counting are Relsat [33] and c2d [23]. Algorithms for counting models of temporal logics and automata over infinite words have been introduced in [27, 28, 44]. The counting of projected models, i.e., when some parts of the models are irrelevant, was studied in [2], for which tools such as #CLASP [2] and DSharp_P [2, 41] exist. Our SAT-based prototype implementation is based on a reduction to a Max#SAT [29] instance, for which a corresponding tool exists.

Among the already existing tools for computing the amount of information leakage, for example, QUAIL [8], which analyzes programs written in a specific while-language and LeakWatch [12], which estimates the amount of leakage in Java programs, Moped-QLeak [9] is closest to our approach. However, their approach of computing a symbolic summary as an Algebraic Decision Diagram is, in contrast to our approach, solely based on model counting, not maximum model counting.

2 Preliminaries

2.1 HyperLTL

HyperLTL [18] extends linear-time temporal logic (LTL) with trace variables and trace quantifiers.

Let $\mathit{AP}$ be a set of atomic propositions. A trace $t$ is an infinite sequence over subsets of the atomic propositions. We define the set of traces $\mathit{TR}\coloneqq(2^{\mathit{AP}})^{\omega}$. A subset $T\subseteq\mathit{TR}$ is called a trace property and a subset $H\subseteq 2^{\mathit{TR}}$ is called a hyperproperty. We use the following notation to manipulate traces: let $t\in\mathit{TR}$ be a trace and $i\in\mathbb{N}$ be a natural number. $t[i]$ denotes the $i$-th element of $t$. Therefore, $t[0]$ represents the starting element of the trace. Let $j\in\mathbb{N}$ and $j\geq i$. $t[i,j]$ denotes the sequence $t[i]~{}t[i+1]\ldots t[j-1]~{}t[j]$. $t[i,\infty]$ denotes the infinite suffix of $t$ starting at position $i$.

HyperLTL Syntax.

Let $\mathcal{V}$ be an infinite supply of trace variables. The syntax of HyperLTL is given by the following grammar:

[TABLE]

where $a\in\mathit{AP}$ is an atomic proposition and $\pi\in\mathcal{V}$ is a trace variable. Note that atomic propositions are indexed by trace variables. The quantification over traces makes it possible to express properties like on all traces $\psi$ must hold'', which is expressed by $\forall\pi.~{}\psi$. Dually, one can express that there exists a trace such that $\psi$ holds'', which is denoted by $\exists\pi.~{}\psi$. The derived operators $\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$, $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$, and $\mathcal{W}$ are defined as for LTL. We abbreviate the formula $\bigwedge_{x\in X}(x_{\pi}\leftrightarrow x_{\pi^{\prime}})$, expressing that the traces $\pi$ and $\pi^{\prime}$ are equal with respect to a set $X\subseteq\mathit{AP}$ of atomic propositions, by $\pi=_{X}\pi^{\prime}$. Furthermore, we call a trace variable $\pi$ free in a HyperLTL formula if there is no quantification over $\pi$ and we call a HyperLTL formula $\varphi$ closed if there exists no free trace variable in $\varphi$.

HyperLTL Semantics.

A HyperLTL formula defines a hyperproperty, i.e., a set of sets of traces. A set $T$ of traces satisfies the hyperproperty if it is an element of this set of sets. Formally, the semantics of HyperLTL formulas is given with respect to a trace assignment $\Pi$ from $\mathcal{V}$ to $\mathit{TR}$, i.e., a partial function mapping trace variables to actual traces. $\Pi[\pi\mapsto t]$ denotes that $\pi$ is mapped to $t$, with everything else mapped according to $\Pi$. $\Pi[i,\infty]$ denotes the trace assignment that is equal to $\Pi(\pi)[i,\infty]$ for all $\pi$.

[TABLE]

We say a set of traces $T$ satisfies a HyperLTL formula $\varphi$ if $\Pi\models_{T}\varphi$, where $\Pi$ is the empty trace assignment.

2.2 System model

A Kripke structure is a tuple $K=(S,s_{0},\delta,\mathit{AP},L)$ consisting of a set of states $S$, an initial state $s_{0}\in S$, a transition function $\delta:S\rightarrow 2^{S}$, a set of atomic propositions $\mathit{AP}$, and a labeling function $L:S\rightarrow 2^{\mathit{AP}}$, which labels every state with a set of atomic propositions. We assume that each state has a successor, i.e., $\delta(s)\not=\emptyset$. This ensures that every run on a Kripke structure can always be extended to an infinite run. We define a path of a Kripke structure as an infinite sequence of states $s_{0}s_{1}\dots\in S^{\omega}$ such that $s_{0}$ is the initial state of $K$ and $s_{i+1}\in\delta(s_{i})$ for every $i\in\mathbb{N}$. We denote the set of all paths of $K$ that start in a state $s$ with $\mathit{Paths}(K,s)$. Furthermore, $\mathit{Paths}^{*}(K,s)$ denotes the set of all path prefixes and $\mathit{Paths}^{\omega}(K,s)$ the set of all path suffixes. A trace of a Kripke structure is an infinite sequence of sets of atomic propositions $L(s_{0}),L(s_{1}),\dots\in(2^{\mathit{AP}})^{\omega}$, such that $s_{0}$ is the initial state of $K$ and $s_{i+1}\in\delta(s_{i})$ for every $i\in\mathbb{N}$. We denote the set of all traces of $K$ that start in a state $s$ with $\mathit{TR}(K,s)$. We say that a Kripke structure $K$ satisfies a HyperLTL formula $\varphi$ if its set of traces satisfies $\varphi$, i.e., if $\Pi\models_{\mathit{TR}(K,s_{0})}\varphi$, where $\Pi$ is the empty trace assignment.

2.3 Automata over infinite words

In our construction we use automata over infinite words. A Büchi automaton is a tuple $\mathcal{B}=(Q,Q_{0},\delta,\Sigma,F)$, where $Q$ is a set of states, $Q_{0}$ is a set of initial states, $\delta:Q\times\Sigma\rightarrow 2^{Q}$ is a transition relation, and $F\subset Q$ are the accepting states. A run of $\mathcal{B}$ on an infinite word $w=\alpha_{1}\alpha_{2}\dots\in\Sigma^{\omega}$ is an infinite sequence $r=q_{0}q_{1}\dots\in Q^{\omega}$ of states, where $q_{0}\in Q_{0}$ and for each $i\geq 0$, $q_{i+1}=\delta(q_{i},\alpha_{i+1})$. We define $\textbf{Inf}(r)=\{q\in Q\mid\forall i\exists j>i.~{}r_{j}=q\}$. A run $r$ is called accepting if $\textbf{Inf}(r)\cap F\not=\emptyset$. A word $w$ is accepted by $\mathcal{B}$ and called a model of $\mathcal{B}$ if there is an accepting run of $\mathcal{B}$ on $w$.

Furthermore, an alternating automaton, whose runs generalize from sequences to trees, is a tuple $\mathcal{A}=(Q,Q_{0},\delta,\Sigma,F)$. $Q,Q_{0},\Sigma$, and $F$ are defined as above and $\delta:Q\times\Sigma\rightarrow\mathbb{B}^{+}{Q}$ being a transition function, which maps a state and a symbol into a Boolean combination of states. Thus, a run(-tree) of an alternating Büchi automaton $\mathcal{A}$ on an infinite word $w$ is a $Q$-labeled tree. A word $w$ is accepted by $\mathcal{A}$ and called a model if there exists a run-tree $T$ such that all paths $p$ trough $T$ are accepting, i.e., $\textbf{Inf}(p)\cap F\not=\emptyset$.

A strongly connected component (SCC) in $\mathcal{A}$ is a maximal strongly connected component of the graph induced by the automaton. An SCC is called accepting if one of its states is an accepting state in $\mathcal{A}$.

3 Quantitative Hyperproperties

Quantitative Hyperproperties are properties of sets of computation traces that express a bound on the number of traces that may appear in a certain relation. In the following, we study quantitative hyperproperties that are specified in terms of HyperLTL formulas. We consider expressions of the following general form:

[TABLE]

Both the universally quantified variables $\pi_{1},\dots,\pi_{k}$ and the variable $\sigma$ after the counting operator $\#$ are trace variables; $\varphi$ is a HyperLTL formula over atomic propositions $AP$ and free trace variables $\pi_{1}\ldots\pi_{k}$; $A\subseteq AP$ is a set of atomic propositions; $\psi$ is a HyperLTL formula over atomic propositions $AP$ and free trace variables $\pi_{1}\ldots\pi_{k}$ and, additionally $\sigma$. The operator $\triangleleft\in\{<,\leq,=,>,\geq\}$ is a comparison operator; and $n\in\mathbb{N}$ is a natural number.

For a given set of traces $T$ and a valuation of the trace variables $\pi_{1},\dots,\pi_{k}$, the term $\#\sigma:A.\,\psi$ computes the number of traces $\sigma$ in $T$ that differ in their valuation of the atomic propositions in $A$ and satisfy $\psi$. The expression $\#\sigma:A.\,\psi\triangleleft n$ is $\mathit{true}$ iff the resulting number satisfies the comparison with $n$. Finally, the complete expression $\forall\pi_{1},\dots,\pi_{k}.\,\varphi\rightarrow(\#\sigma:A.\,\psi\triangleleft n)$ is $\mathit{true}$ iff for all combinations $\pi_{1},\dots,\pi_{k}$ of traces in $T$ that satisfy $\varphi$, the comparison $\#\sigma:A.\,\psi\triangleleft n$ is satisfied.

Example 1 (Quantitative non-interference)

Quantitative information-flow policies [30, 13, 34, 20] allow the flow of a bounded amount of information. One way to measure leakage is with min-entropy [43], which quantifies the amount of information an attacker can gain given the answer to a single guess about the secret. The bounding problem [45] for min-entropy is to determine whether that amount is bounded from above by a constant $2^{c}$, corresponding to $c$ bits. We assume that the program whose leakage is being quantified is deterministic, and assume that the secret input to that program is uniformly distributed. The bounding problem then reduces to determining that there is no tuple of $2^{c}+1$ distinguishable traces [43, 45]. Let $O\subseteq AP$ be the set of observable outputs. A simple quantitative information flow policy is then the following quantitative hyperproperty, which bounds the number of distinguishable outputs to $2^{c}$, corresponding to a bound of $c$ bits of information:

[TABLE]

A slightly more complicated information flow policy is quantitative non-interference. In quantitative non-interference, the bound must be satisfied for every individual input. Let $I\subseteq AP$ be the observable inputs to the system. Quantitative non-interference is the following quantitative hyperproperty111We write $\pi=_{A}\pi^{\prime}$ short for $\pi_{A}=\pi^{\prime}_{A}$ where $\pi_{A}$ is the $A$-projection of $\pi$:

[TABLE]

For each trace $\pi$ in the system, the property checks whether there are more than $2^{c}$ traces $\sigma$ that have the same observable input as $\pi$ but different observable output.

Example 2 (Deniability)

A program satisfies deniability (see, for example, [7, 10]) when there is no proof that a certain input occurred from simply observing the output, i.e., given an output of a program one cannot derive the input that lead to this output. A deterministic program satisfies deniability when each output can be mapped to at least two inputs. A quantitative variant of deniability is when we require that the number of corresponding inputs is larger than a given threshold. Quantitative deniability can be specified as the following quantitative Hyperproperty:

[TABLE]

For all traces $\pi$ of the system we count the number of sequences $\sigma$ in the system with different input sequences and the same output sequence of $\pi$, i.e., for the fixed output sequence given by $\pi$ we count the number of input sequences that lead to this output.

4 Model Checking Quantitative Hyperproperties

We present a model checking algorithm for quantitative hyperproperties based on model counting. The advantage of the algorithm is that its runtime complexity is independent of the bound $n$ and thus avoids the $n$-fold self-composition necessary for any encoding of the quantitative hyperproperty in HyperLTL.

Before introducing our novel counting-based algorithm, we start by a translation of quantitative hyperproperties into formulas in HyperLTL and establishing an exponential lower bound for its representation.

4.1 Standard model checking algorithm: encoding quantitative hyperproperties in HyperLTL

The idea of the reduction is to check a lower bound of $n$ traces by existentially quantifying over $n$ traces, and to check an upper bound of $n$ traces by universally quantifying over $n+1$ traces. The resulting HyperLTL formula can be verified using the standard model checking algorithm for HyperLTL [18].

Theorem 4.1

Every quantitative hyperproperty $\forall\pi_{1},\dots,\pi_{k}.\ \psi_{\iota}\rightarrow(\#\sigma:A.\ \psi\triangleleft n)$ can be expressed as a HyperLTL formula. For $\triangleleft\in\{\leq\}(\{<\})$, the HyperLTL formula has $n+k+1(\text{resp. }n+k)$ universal trace quantifiers in addition to the quantifiers in $\psi_{\iota}$ and $\psi$. For $\triangleleft\in\{\geq\}(\{>\})$, the HyperLTL formula has $k$ universal trace quantifiers and $n$ $(\text{resp. }n+1)$ existential trace quantifiers in addition to the quantifiers in $\psi_{\iota}$ and $\psi$. For $\triangleleft\in\{=\}$, the HyperLTL formula has $n+k+1$ universal trace quantifiers and $n$ existential trace quantifiers in addition to the quantifiers in $\psi_{\iota}$ and $\psi$.

Proof

For $\triangleleft\in\{\leq\}$, we encode the quantitative hyperproperty $\forall\pi_{1},\dots,\pi_{k}.\ \psi_{\iota}\rightarrow(\#\sigma:A.\ \psi\triangleleft n)$ as the following HyperLTL formula:

[TABLE]

where $\psi[\sigma\mapsto\pi^{\prime}_{i}]$ is the HyperLTL formula $\psi$ with all occurrences of $\sigma$ replaced by $\pi^{\prime}_{i}$. The formula states that there is no tuple of $n+1$ traces $\pi^{\prime}_{1},\ldots,\pi^{\prime}_{n+1}$ different in the evaluation of $A$, that satisfy $\psi$. In other words, for every $n+1$ tuple of traces $\pi^{\prime}_{1},\ldots,\pi^{\prime}_{n+1}$ that differ in the evaluation of $A$, one of the paths must violate $\psi$. For $\triangleleft\in\{<\}$, we use the same formula, with $\forall\pi^{\prime}_{1},\ldots,\pi^{\prime}_{n}$ instead of $\forall\pi^{\prime}_{1},\ldots,\pi^{\prime}_{n+1}$.

For $\triangleleft\in\{\geq\}$, we encode the quantitative hyperproperty analogously as the HyperLTL formula

[TABLE]

The formula states that there exist paths $\pi^{\prime}_{1},\ldots,\pi^{\prime}_{n}$ that differ in the evaluation of $A$ and that all satisfy $\psi$. For $\triangleleft\in\{>\}$, we use the same formula, with $\exists\pi^{\prime}_{1},\ldots,\pi^{\prime}_{n+1}$ instead of $\forall\pi^{\prime}_{1},\ldots,\pi^{\prime}_{n}$. Lastly, for $\triangleleft\in\{=\}$, we encode the quantitative hyperproperty as a conjunction of the encodings for $\leq$ and for $\geq$.

Example 3 (Quantitative non-interference in HyperLTL)

As discussed in Example 1, quantitative non-interference is the quantitative hyperproperty

[TABLE]

where we measure the amount of leakage with min-entropy [43]. The bounding problem for min-entropy asks whether the amount of information leaked by a system is bounded by a constant $2^{c}$ where $c$ is the number of bits. This is encoded in HyperLTL as the requirement that there are no $2^{c}+1$ traces distinguishable in their output:

[TABLE]

This formula is equivalent to the formalization of quantitative non-interference given in [26].

Model checking quantitative hyperproperties via the reduction to HyperLTL is very expensive. In the best case, when $\triangleleft\in\{\leq,<\}$, $\psi_{\iota}$ does not contain existential quantifiers, and $\psi$ does not contain universal quantifiers, we obtain an HyperLTL formula without quantifier alternations, where the number of quantifiers grows linearly with the bound $n$. For $m$ quantifiers, the HyperLTL model checking algorithm [26] constructs and analyzes the $m$-fold self-composition of the Kripke structure. The running time of the model checking algorithm is thus exponential in the bound. If $\triangleleft\in\{\geq,>,=\}$, the encoding additionally introduces a quantifier alternation. The model checking algorithm checks quantifier alternations via a complementation of Büchi automata, which adds another exponent, resulting in an overall doubly exponential running time.

The model checking algorithm we introduce in the next section avoids the $n$-fold self-composition needed in the model checking algorithm of HyperLTL and its complexity is independent of the bound $n$.

4.2 Counting-based model checking algorithm

A Kripke structure $K=(S,s_{0},\tau,\textit{AP},L)$ violates a quantitative hyperproperty

[TABLE]

if there is a $k$-tuple $t=(\pi_{1},\dots,\pi_{k})$ of traces $\pi_{i}\in\textit{TR}(K)$ that satisfies the formula

[TABLE]

where $\overline{\triangleleft}$ is the negation of the comparison operator $\triangleleft$. The tuple $t$ then satisfies the property $\psi_{\iota}$ and the number of $(k+1)$-tuples $t^{\prime}=(\pi_{1},\dots,\pi_{k},\sigma)$ for $\sigma\in\textit{TR}(K)$ that satisfy $\psi$ and differ pairwise in the $A$-projection of $\sigma$ satisfies the comparison $\overline{\triangleleft}~{}n$ (The $A$-projection of a sequence $\sigma$ is defined as the sequence $\sigma_{A}\in(2^{A})^{\omega}$, such that for every position $i$ and every $a\in A$ it holds that $a\in\sigma_{A}[i]$ if and only if $a\in\sigma[i]$). The tuples $t^{\prime}$ can be captured by the automaton composed of the product of an automaton $A_{\psi_{\iota}\wedge\psi}$ that accepts all $k+1$ of traces that satisfy both $\psi_{\iota}$ and $\psi$ and a $k+1$-self composition of $K$. Each accepting run of the product automaton presents $k+1$ traces of $K$ that satisfy $\psi_{\iota}\wedge\psi$. On top of the product automaton, we apply a special counting algorithm which we explain in detail in Section 4.4 and check if the result satisfies the comparison $\overline{\triangleleft}~{}n$.

Algorithm 1 gives a general picture of our model checking algorithm. The algorithm has two parts. The first part applies if the relation $\overline{\triangleleft}$ is one of $\{\geq,>\}$. In this case, the algorithm checks whether a sequence over $\textit{AP}_{\psi}$ (propositions in $\psi$) corresponds to infinitely many sequences over $A$. This is done by checking whether the product automaton $B$ has a so-called doubly pumped lasso(DPL), a subgraph with two connected lassos, with a unique sequence over $\textit{AP}_{\psi}$ and different sequences over $A$. Such a doubly pumped lasso matches the same sequence over $\textit{AP}_{\psi}$ with infinitely many sequences over $A$ (more in section 4.4). If no doubly pumped lasso is found, a projected model counting algorithm is applied in the second part of the algorithm in order to compute either the maximum or the minimum value, corresponding to the comparison operator $\overline{\triangleleft}$. In the next subsections, we explain the individual parts of the algorithm in detail.

4.3 Büchi automata for quantitative hyperproperties

For a quantitative hyperproperty $\varphi=\forall\pi_{1}\dots\pi_{k}.~{}\psi_{\iota}\rightarrow(\#\sigma:A.\psi\triangleleft n)$ and a Kripke structure $K=(S,s_{0},\tau,\textit{AP},L)$, we first construct an alternating automaton $A_{\psi_{\iota}\wedge\psi}$ for the HyperLTL property $\psi_{\iota}\wedge\psi$. Let $A_{\psi_{1}}=(Q_{1},q_{0,1},\Sigma_{2},\delta_{1},F_{1})$ and $A_{\psi_{2}}=(Q_{2},q_{0,2},\Sigma_{2},\delta_{2},F_{2})$ be alternating automata for subformulas $\psi_{1}$ and $\psi_{2}$. Let $\Sigma=2^{\textit{AP}_{\varphi}}$ where $AP_{\varphi}$ are all indexed atomic propositions that appear in $\varphi$. $A_{\psi_{\iota}\wedge\psi}$ is constructed using following rules222The construction follows the one presented in [26] with a slight modification on the labeling of transitions. Labeling over atomic proposition instead of the states of the Kripke structure suffices, as any nondeterminism in the Kripke structure is inherently resolved, because we quantify over trace not paths:

[TABLE]

For a quantified formula $\varphi=\exists\pi.\psi_{1}$, we construct the product automaton of the Kripke structure $K$ and the Büchi automaton of $\psi_{1}$. Here we reduce the alphabet of the automaton by projecting all atomic proposition in $\textit{AP}_{\pi}$ away:

[TABLE]

Given the Büchi automaton for the hyperproperty $\psi_{\iota}\wedge\psi$ it remains to construct the product with the $k+1$-self composition of $K$. The transitions of the automaton are defined over labels from $\Sigma=2^{\textit{AP}^{*}}$ where $AP^{*}={\textit{AP}_{\sigma}\cup\bigcup_{i}\textit{AP}_{\pi_{i}}}$. $A_{\psi_{\iota}\wedge\psi}$. This is necessary to identify which transition was taken in each copy of $K$, thus, mirroring a tuple of traces in $K$. For each of the variables $\pi_{1},\dots\pi_{k}$ and $\sigma$ we use following rule:

[TABLE]

Finally, we transform the resulting alternating automaton to an equivalent Büchi automaton following the construction of Miyano and Hayashi [39].

4.4 Counting models of $\omega$-Automata

Computing the number of words accepted by a Büchi automaton can be done by examining its accepting lassos. Consider, for example, the Büchi automata over the alphabet $2^{\{a\}}$ in Figure 1. The automaton on the left has one accepting lasso $(q_{0})^{\omega}$ and thus has only one model, namely $\{a\}^{\omega}$. The automaton on the right has infinitely many accepting lassos $(q_{0}\{\})^{i}\{a\}(q_{1}(\{\}\vee\{a\}))^{\omega}$ that accept infinitely many different words all of the from $\{\}^{*}\{a\}(\{\}\vee\{a\})^{\omega}$.

Computing the models of a Büchi automaton is insufficient for model checking quantitative hyperproperties as we are not interested in the total number of models. We rather maximize, respectively minimize, over sequences of subsets of atomic propositions the number of projected models of the Büchi automaton. For instance, consider the automaton given in Figure 2.

The automaton has infinitely many models. However, the maximum number of sequences $\sigma_{b}\in 2^{\{b\}}$ that correspond to accepting lassos in the automaton with a unique sequence $\sigma_{a}\in 2^{\{a\}}$ is two: For example, let $n$ be a natural number. For any model of the automaton and for each sequence $\sigma_{a}:=\{\}^{n}\{a\}(\{\})^{\omega}$ the automaton accepts the following two sequences: $\{b\}^{n}\{\}\{b\}^{\omega}$ and $\{b\}^{\omega}$. Formally, given a Büchi automaton $\mathcal{B}$ over $\mathit{AP}$ and a set $A$, such that $A\subseteq\mathit{AP}$, an $A$-projected model (or projected model over $A$) is defined as a sequence $\sigma_{A}\in(2^{\mathit{A}})^{\omega}$ that results in the $A$-projection of an accepting sequence $\sigma\in(2^{\mathit{AP}})^{\omega}$.

In the following, we define the maximum model counting problem over automata and give an algorithm for solving the problem. We show how to use the algorithm for model checking quantitative hyperproperties.

Definition 1 (Maximum Model Counting over Automata (MMCA))

Given a Büchi automaton $B$ over an alphabet $2^{\textit{AP}}$ for some set of atomic propositions AP and sets $X,Y,Z\subseteq\textit{AP}$ the maximum model counting problem is to compute

[TABLE]

where $\sigma\cup\sigma^{\prime}$ is the point-wise union of $\sigma$ and $\sigma^{\prime}$.

As a first step in our algorithm, we show how to check whether the maximum model count is equal to infinity.

Definition 2 (Doubly Pumped Lasso)

For a graph $G$, a doubly pumped lasso in $G$ is a subgraph that entails a cycles $C_{1}$ and another different cycle $C_{2}$ that is reachable from $C_{1}$.

In general, we distinguish between two types of doubly pumped lassos as shown in Figure 3. We call the lassos with periods $C_{1}$ and $C_{2}$ the lassos of the doubly pumped lasso. A doubly pumped lasso of a Büchi automaton $B$ is one in the graph structure of $B$. The doubly pumped lasso is called accepting when $C_{2}$ has an accepting state. A more generalized formalization of this idea is given in the following theorem.

Theorem 4.2

*Let $B=(Q,q_{0},\delta,2^{\textit{AP}},F)$ be a Büchi automaton for some set of atomic propositions $\textit{AP}=X\cup Y\cup Z$ and let $\sigma^{\prime}\in(2^{Y})^{\omega}$. The automaton $B$ has infinitely many $X\cup Y$-projected models $\sigma$ with $\sigma=_{Y}\sigma^{\prime}$ if and only if $B$ has an accepting doubly pumped lasso with lassos $\rho$ and $\rho^{\prime}$ such that:

1. $\rho$ is an accepting lasso
2. $\textit{tr}(\rho)=_{Y}\textit{tr}(\rho^{\prime})=_{Y}\sigma^{\prime}$
3. The period of $\rho^{\prime}$ shares at least one state with $\rho$ and 4) $\textit{tr}(\rho)\not=_{X}\textit{tr}(\rho^{\prime})$.*

To check whether there is a sequence $\sigma^{\prime}\in(2^{Y})^{\omega}$ such that the number of $X\cup Y$-projected models $\sigma$ of $B$ with $\sigma=_{Y}\sigma^{\prime}$ is infinite, we search for a doubly pumped lasso satisfying the constraints given in Theorem 4.2. This can be done by applying the following procedure:

Given a Büchi automaton $B=(Q,q_{0},2^{\textit{AP}},\delta,F)$ and sets $X,Y,Z\subseteq\textit{AP}$, we construct the following product automaton $B_{\times}=(Q_{\times},q_{\times,0},2^{\textit{AP}}\times 2^{\textit{AP}},\delta_{\times},F_{\times})$ where: $Q_{\times}=Q\times Q$, $q_{\times,0}=(q_{0},q_{0})$, $\delta_{\times}=\{(s_{1},s_{2})\xrightarrow{(\alpha,\alpha^{\prime})}(s^{\prime}_{1},s_{2}^{\prime})\mid s_{1}\xrightarrow{\alpha}s_{2},s^{\prime}_{1}\xrightarrow{\alpha^{\prime}}s^{\prime}_{2},\alpha=_{Y}\alpha^{\prime}\}$ and $F_{\times}=Q\times F$. The automaton $B$ has infinitely many models $\sigma^{\prime}$ if there is an accepting lasso $\rho=(q_{0},q_{0})(\alpha_{1},\alpha^{\prime}_{1})\dots((q_{j},q_{j}^{\prime})(\alpha_{j+1},\alpha^{\prime}_{j+1})$ $\dots(q_{k},q^{\prime}_{k})(\alpha_{k+1},\alpha^{\prime}_{k+1}))$ in $B_{\times}$ such that: $\exists h\leq j.~{}q^{\prime}_{h}=q_{j}$, i.e., $B$ has lassos $\rho_{1}$ and $\rho_{2}$ that share a state in the period of $\rho_{1}$ and $\exists h>j.~{}\alpha_{h}\not=_{X}\alpha^{\prime}_{h}$, i.e., the lassos differ in the evaluation of $X$ in a position after the shared state and thus allows infinitely many different sequence over $X$ for the a sequence over $Y$. The lasso $\rho$ simulates a doubly pumped lasso in $B$ satisfying the constraints of Theorem 4.2.

Theorem 4.3

Given an alternating Büchi automaton $A=(Q,q_{0},\delta,2^{\textit{AP}},F)$ for a set of atomic propositions $\textit{AP}=X\cup Y\cup Z$, the problem of checking whether there is a sequence $\sigma^{\prime}\in(2^{Y})^{\omega}$ such that $A$ has infinitely many $X\cup Y$-projected models $\sigma$ with $\sigma=_{Y}\sigma^{\prime}$ is Pspace-complete.

The lower and upper bound for the problem can be given by a reduction from and to the satisfiability problem of LTL [4]. Due to the finite structure of Büchi automata, if the number of models of the automaton exceed the exponential bound $2^{|Q|}$, where $Q$ is the set of states, then the automaton has infinitely many models.

Lemma 1

For any Büchi automaton $B$, the number of models of $B$ is less or equal to $2^{|Q|}$ otherwise it is $\infty$.

Proof

Assume the number of models is larger than $2^{|Q|}$ then there are more than $2^{|Q|}$ accepting lassos in $B$. By the pigeonhole principle, two of them share the same $2^{|Q|}$-prefix. Thus, either they are equal or we found doubly pumped lasso in $B$.

Corollary 1

Let a Büchi automaton $B$ over a set of atomic propositions AP and sets $X,Y\subseteq\textit{AP}$. For each sequence $\sigma_{Y}\in(2^{Y})^{\omega}$ the number of $X\cup Y$-projected models $\sigma$ with $\sigma=_{Y}\sigma_{Y}$ is less or equal than $2^{|Q|}$ otherwise it is $\infty$.

From Corollary 1, we know that if no sequence $\sigma_{Y}\in(2^{Y})^{\omega}$ matches to infinitely many $X\cup Y$-projected models then the number of such models is bound by $2^{|Q|}$. Each of these models has a run in $B$ which ends in an accepting strongly connected component. Also from Corollary 1, we know that every model has a lasso run of length $|Q|$. For each finite sequence $w_{Y}$ of length $|w_{Y}|=|Q|$ that reaches an accepting strongly connected component, we count the number $X\cup Y$-projected words $w$ of length $|Q|$ with $w=_{Y}w_{Y}$ and that end in an accepting strongly connected component. This number is equal to the maximum model counting number.

Algorithm 2 describes the procedure. An algorithm for the minimum model counting problem is defined in similar way. The algorithm works in a backwards fashion starting with states of accepting strongly connected components. In each iteration $i$, the algorithm maps each state of the automaton with $X\cup Y$-projected words of length $i$ that reach an accepting strongly connected component. After $|Q|$ iterations, the algorithm determines from the mapping of initial state $q_{0}$ a $Y$-projected word of length $|Q|$ with the maximum number of matching $X\cup Y$-projected words.

Theorem 4.4

The decisional version of the maximum model counting problem over automata (MMCA), i.e. the question whether the maximum is greater than a given natural number $n$, is in $\mathit{NP}^{\#P}$.

Proof

Let a Büchi automaton over an alphabet $2^{\mathit{AP}}$ for a set of atomic propositions $\mathit{AP}$ and sets $\textit{AP}_{X},\textit{AP}_{Y},\textit{AP}_{Z}\subseteq\textit{AP}$ and a natural number $n$ be given. We construct a nondeterministic Turing Machine $M$ with access to a $\#P$-oracle as follows: $M$ guesses a sequence $\sigma_{Y}\in 2^{\mathit{AP_{Y}}}$. It then queries the oracle, to compute a number $c$, such that $c=|\{\sigma_{X}\in(2^{\textit{AP}_{X}})^{\omega}\mid\exists\sigma_{Z}\in(2^{\textit{AP}_{Z}})^{\omega}.~{}\sigma_{X}\cup\sigma_{Y}\cup\sigma_{Z}\in L(B)\}|$, which is a $\#P$ problem [27]. It remains to check whether $n>c$. If so, $M$ accepts.

The following theorem summarizes the main findings of this section, which establish, depending on the property, an exponentially or even doubly exponentially better algorithm (in the quantitative bound) over the existing model checking algorithm for HyperLTL.

Theorem 4.5

Given a Kripke structure $K$ and a quantitative hyperproperty $\varphi$ with bound $n$, the problem whether $K\models\varphi$ can be decided in logarithmic space in the quantitative bound $n$ and in polynomial space in the size of $K$.

5 A Max#Sat-based Approach

For existential HyperLTL formulas $\psi_{\iota}$ and $\psi$, we give a more practical model checking approach by encoding the automaton-based construction presented in Section 4 into a propositional formula.

Given a Kripke structure $K=(S,s_{0},\tau,\textit{AP}_{K},L)$ and a quantitative hyperproperty $\varphi=\forall\pi_{1},\dots,\pi_{k}.~{}\psi_{\iota}\rightarrow(\#\sigma:A.~{}\psi)\triangleleft n$ over a set of atomic propositions $\textit{AP}_{\varphi}\subseteq\textit{AP}_{K}$ and bound $\mu$, our algorithm constructs a propositional formula $\phi$ such that, every satisfying assignment of $\phi$ uniquely encodes a tuple of lassos $(\pi_{1},\dots,\pi_{k},\sigma)$ of length $\mu$ in $K$, where $(\pi_{1},\dots,\pi_{k})$ satisfies $\psi_{\iota}$ and $(\pi_{1},\dots,\pi_{k},\sigma)$ satisfies $\psi$. To compute the values $\max\limits_{(\pi_{1},\dots,\pi_{k})}|\{\sigma_{A}\mid(\pi_{1},\dots,\pi_{k},\sigma)\models\psi_{\iota}\wedge\psi\}|$ (in case $\triangleleft\in\{\leq,<\}$) or $\min\limits_{(\pi_{1},\dots,\pi_{k})}|\{\sigma_{A}\mid(\pi_{1},\dots,\pi_{k},\sigma)\models\psi_{\iota}\wedge\psi\}|$ (in case $\triangleleft\in\{\geq,>\}$), we pass $\phi$ to a maximum model counter, respectively, to a minimum model counter with the appropriate sets of counting and maximization, respectively, minimization propositions. From Lemma 1 we know that it is enough to consider lassos of length linear in the product automaton. The size of $\phi$ is thus exponential in the size of $\varphi$ and polynomial in the size of $K$.

The construction resembles the encoding of the bounded model checking approach for LTL [16]. Let $\psi_{\iota}=\exists\pi^{\prime}_{1}\dots\pi^{\prime}_{k^{\prime}}.~{}\psi^{\prime}_{\iota}$ and $\psi=\exists\pi^{\prime\prime}_{1}\dots\pi^{\prime\prime}_{k^{\prime\prime}}.~{}\psi^{\prime\prime}$ and let $\textit{AP}_{\psi_{\iota}}$ and $\textit{AP}_{\psi}$ be the sets of atomic propositions that appear in $\psi_{\iota}$ and $\psi$ respectively. The propositional formula $\phi$ is given as a conjunction of the following propositional formulas:

[TABLE]

where:

• •

$\mu$ is length of considered lassos and is equal to $\mu=2^{|\psi^{\prime}_{\iota}\wedge\psi^{\prime\prime}|}*|S|^{k+k^{\prime}+k^{\prime\prime}+1}+1$, which is one plus the size of the product automaton constructed from the $k+k^{\prime}+k^{\prime\prime}+1$ self-composition and the automaton for $\psi_{\iota}\wedge\psi$. The "plus one" is to additionally to check whether the number of models is infinite.

• •

$\llbracket K\rrbracket^{\pi}_{k}$ is the encoding of the transition relation of the copy of $K$ where atomic propositions are indexed with $\pi$ and up to an unrolling of length $k$. Each state of $K$ can be encoded as an evaluation of a vector of $\log{|S|}$ unique propositional variables. The encoding333We refer the reader to [16] for more information on the encoding is given by the propositional formula $I(\vv{v}_{0}^{\pi})\wedge\bigwedge_{i=0}^{k-1}\tau(\vv{v}_{i}^{\pi},\vv{v}_{i+1}^{\pi})$ which encodes all paths of $K$ of length $k$. The formula $I(\vv{v}_{0}^{\pi})$ defines the assignment of the initial state. The formulas $\tau(\vv{v}_{i}^{\pi},\vv{v}_{i+1}^{\pi})$ define valid transitions in $K$ from the $i$th to the $(i+1)$st state of a path.

• •

$\llbracket\psi_{\iota}\rrbracket_{k}^{0}$ and $\llbracket\psi\rrbracket_{k}^{0}$ are constructed using the following rules444We omitted the rules for boolean operators for the lack of space:

[TABLE]

in case of an existential quantifier over a trace variable $\pi$, we add a copy of the encoding of $K$ with new variables distinguished by $\pi$:

[TABLE]

We define sets $X=\{a^{i}_{\sigma}\mid a\in A,i\leq k\}$, $Y=\{a^{i}\mid a\in\textit{AP}_{\psi}\setminus A,i\leq k\}$ and $Z=P\setminus X\cup Y$, where $P$ is the set of all propositions in $\phi$. The maximum model counting problem is then $\textit{MMC}(\phi,X,Y,Z)$.

5.1 Experiments

We have implemented the Max#Sat-based model checking approach from the last section. We compare the Max#Sat-based approach to the expansion-based approach using HyperLTL [26]. Our implementation uses the MaxCount tool [29]. We use the option in MaxCount that enumerates, rather than approximates, the number of assignments for the counting variables. We furthermore instrumented the tool so that it terminates as soon as a sample is found that exceeds the given bound. If no sample is found after one hour, we report a timeout.

Table 1 shows the results on a parameterized benchmark obtained from the implementation of an 8bit passcode checker. The parameter of the benchmark is the bound on the number of bits that is leaked to an adversary, who might, for example, enter passcodes in a brute-force manner. In all instances, a violation is found. The results show that the Max#Sat-based approach scales significantly better than the expansion-based approach.

6 Conclusion

We have studied quantitative hyperproperties of the form $\forall\pi_{1},\dots,\pi_{k}.\ \varphi\rightarrow(\#\sigma:A.\ \psi\triangleleft n)$, where $\varphi$ and $\psi$ are HyperLTL formulas, and $\#\sigma:A.\varphi\triangleleft n$ compares the number of traces that differ in the atomic propositions $A$ and satisfy $\psi$ to a threshold $n$. Many quantitative information flow policies of practical interest, such as quantitative non-interference and deniability, belong to this class of properties. Our new counting-based model checking algorithm for quantitative hyperproperties performs at least exponentially better in both time and space in the bound $n$ than a reduction to standard HyperLTL model checking. The new counting operator makes the specifications exponentially more concise in the bound, and our model checking algorithm solves the concise specifications efficiently.

We also showed that the model checking problem for quantitative hyperproperties can be solved with a practical Max#SAT-based algorithm. The SAT-based approach outperforms the expansion-based approach significantly for this class of properties. An additional advantage of the new approach is that it can handle properties like deniability, which cannot be checked by MCHyper because of the quantifier alternation.