Formal models for quantitative analysis of software security

2017 Fiscal Year Final Research Report

• Project/Area Number: 26540025
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Nagoya University
• Principal Investigator: Seki Hiroyuki 名古屋大学, 情報学研究科, 教授 (80196948)
• Co-Investigator(Renkei-kenkyūsha): HASHIMOTO KENJI 名古屋大学, 大学院情報学研究科, 助教 (90548447)
• Project Period (FY): 2014-04-01 – 2018-03-31
• Keywords: セキュリティ / 量的情報流 / k-安全性 / XMLデータベース / 時間攻撃 / 差分プライバシー / SMT / SAT

Outline of Final Research Achievements

A few quantitative notions for security and privacy of software such as quantitative information flow (QIF) and differential privacy have been proposed. In this research, we developed methods that analyze given programs or systems based on such notions. Specifically, we proposed an approximation algorithm that computes leakage by timing attack against an RSA decoder, a verification algorithm of k-secrecy of XML databases. Furthermore, as a theoretical basis for QIF analysis of programs that dynamically generate strings, we propose algorithms that counts, for a given recognizable or algebraic series S and a natural number d, the summation of the coefficients (or weights) of words of length d in S efficiently. The proposed methods were shown to be effective either by computer simulation or by experiments based on the implemented tools.

Free Research Field

ソフトウェア基礎理論