On bounding problems of quantitative information flow

Hirotoshi Yasuoka, Tachio Terauchi

Research output: Contribution to journalArticle

9 Citations (Scopus)

Abstract

Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, belief, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the "bounding problem" of quantitative information flow, defined as follows: Given a program M and a positive real number q, decide if the quantitative information flow of M is less than or equal to q. We prove that the bounding problem is not a k-safety property for any k (even when q is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free Boolean programs. Specifically, we show that the problem is PP-hard for all definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow.

Original languageEnglish
Pages (from-to)1029-1082
Number of pages54
JournalJournal of Computer Security
Volume19
Issue number6
DOIs
Publication statusPublished - 2011
Externally publishedYes

Fingerprint

Entropy
Hardness
Channel capacity
Chemical analysis

Keywords

  • program verification
  • quantitative information flow
  • Security

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality
  • Hardware and Architecture
  • Computer Networks and Communications

Cite this

On bounding problems of quantitative information flow. / Yasuoka, Hirotoshi; Terauchi, Tachio.

In: Journal of Computer Security, Vol. 19, No. 6, 2011, p. 1029-1082.

Research output: Contribution to journalArticle

Yasuoka, Hirotoshi ; Terauchi, Tachio. / On bounding problems of quantitative information flow. In: Journal of Computer Security. 2011 ; Vol. 19, No. 6. pp. 1029-1082.
@article{22422c2ee05b4f9fbaec6c0d1d47c2bc,
title = "On bounding problems of quantitative information flow",
abstract = "Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, belief, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the {"}bounding problem{"} of quantitative information flow, defined as follows: Given a program M and a positive real number q, decide if the quantitative information flow of M is less than or equal to q. We prove that the bounding problem is not a k-safety property for any k (even when q is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free Boolean programs. Specifically, we show that the problem is PP-hard for all definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow.",
keywords = "program verification, quantitative information flow, Security",
author = "Hirotoshi Yasuoka and Tachio Terauchi",
year = "2011",
doi = "10.3233/JCS-2011-0437",
language = "English",
volume = "19",
pages = "1029--1082",
journal = "Journal of Computer Security",
issn = "0926-227X",
publisher = "IOS Press",
number = "6",

}

TY - JOUR

T1 - On bounding problems of quantitative information flow

AU - Yasuoka, Hirotoshi

AU - Terauchi, Tachio

PY - 2011

Y1 - 2011

N2 - Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, belief, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the "bounding problem" of quantitative information flow, defined as follows: Given a program M and a positive real number q, decide if the quantitative information flow of M is less than or equal to q. We prove that the bounding problem is not a k-safety property for any k (even when q is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free Boolean programs. Specifically, we show that the problem is PP-hard for all definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow.

AB - Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, belief, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the "bounding problem" of quantitative information flow, defined as follows: Given a program M and a positive real number q, decide if the quantitative information flow of M is less than or equal to q. We prove that the bounding problem is not a k-safety property for any k (even when q is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free Boolean programs. Specifically, we show that the problem is PP-hard for all definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow.

KW - program verification

KW - quantitative information flow

KW - Security

UR - http://www.scopus.com/inward/record.url?scp=84858174770&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84858174770&partnerID=8YFLogxK

U2 - 10.3233/JCS-2011-0437

DO - 10.3233/JCS-2011-0437

M3 - Article

VL - 19

SP - 1029

EP - 1082

JO - Journal of Computer Security

JF - Journal of Computer Security

SN - 0926-227X

IS - 6

ER -