2013 Fiscal Year Final Research Report
Verification of Quantitative Information Flow
| Project/Area Number |
23700026
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
TERAUCHI Tachio 名古屋大学, 情報科学研究科, 准教授 (70447150)
|
|---|
| Project Period (FY) |
2011 – 2013
|
| Keywords | セキュリティ / プログラミング言語 / プログラム検証 / 量的情報流 |
|---|
| Research Abstract |
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.
|
