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
|
| Project Status |
Completed (Fiscal Year 2013)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2013: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2012: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2011: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| 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.
|
Report
(4 results)
Research Products
(27 results)
