Verification of Quantitative Information Flow

点击翻译按钮获取中文摘要

We solved open problems concerning the complexity of various quantitative information flow verification problems. We considered quantitative information flow definitions based on various information theoretic notions such as belief and min entropy channel capacity, and studied the problems both from the computational complexity theoretic aspect and the program verification property classification aspect formalized by the notion of "hyperproperties." We also proposed algorithms for precisely inferring and verifying the quantitative information flow bounds that utilize software model checking and counting algorithms. We also proposed new approaches to software model checking.