2019 Fiscal Year Annual Research Report
ソフトウェアモデルへの量的尺度の導入とプログラム解析への応用
| Project/Area Number |
19H04083
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
関 浩之 名古屋大学, 情報学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小川 瑞史 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (40362024)
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | ソフトウェア検証 / セキュリティ / レジスタオートマトン / モデル検査 |
|---|
| Outline of Annual Research Achievements |
動的情報流の定量的尺度として，出力値観測後の機密入力値の自己情報量に基づく指標（QIF1）と, 機密入力値と出力値の同時情報量に基づく指標（QIF2）の２つを提案し，それらの定義の妥当性と特性を議論した．理論的考察として，ブールプログラムのQIF1とQIF2の計算問題に付随する判定問題の計算量を明らかにした．さらに，既存のモデル計数ツールを活用してこれらの動的QIFを計算するツールを実装し，ベンチマークプログラムを用いて計算実験を行った．さらに，プログラムの動的QIFを計算するとき，より規模の小さいプログラムに分解し，分解された部分プログラムのQIFの計算結果からもとのプログラムのQIFを得る手法として，プログラムの入出力値集合を分割する手法（ValDo）とプログラム構造を直列分解する手法（Seq）を提案した．ValDoはQIF計算の並列化に適し，Seqはプログラムがいくつかの直列フェーズに分解可能な場合に効果が大きいことが実験的に示された．
文脈自由文法(CFG)にデータ値を扱う能力を加えたレジスタCFG(RCFGと略記)が知られている．本研究では，データ値に対する任意の比較演算を許すように拡張した一般化RCFG（GRCFG）を提案した．稠密集合（有理数の集合など）上の大小関係を扱う実用上重要なGRCFGの部分クラスでは所属問題や空問題が判定可能である一方，一般にはこれらの問題は判定不能となることを証明した．また，これらの問題が判定可能となる簡潔で見通しのよい十分条件（模倣性と進行性）を提案した．
重み付きレジスタオートマトン（WRA）はレジスタオートマトンに重みを導入して拡張した計算モデルであり，重みによって遷移やレジスタ操作のコストを表現できる．またWRAは重み付き時間オートマトン（WTA）の拡張になっている．本研究では，WRA に対する最小重み実行問題を定義し，これを解く手法を提案した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究課題について，学術誌掲載論文２編，査読付き国際会議論文３編，国内口頭発表３件の成果を挙げており，順調に進展していると自己評価できる．
|
| Strategy for Future Research Activity |
再帰プログラムのための簡潔な計算モデルとしてプッシュダウンシステム(Pushdown System, PDSと略)が知られている．PDSは前方および後方正則保存性という良い性質をもち，この性質により，PDSに対するLTLモデル検査が可能であること等も知られている．しかしPDSではデータ値は捨象しているため現実のプログラムのモデルとしては単純すぎる．そこで本研究では今後，PDSをレジスタ付きに拡張したモデルに対する検証自動化を試みる．すでPDSにレジスタを導入したレジスタPDS(RPDSと略)に対して，データ言語の前方正則保存性をもつことが知られている．ここで，データ言語が正則であるとは，レジスタオートマトンで認識可能であることを意味する．研究代表者らは，RPDSは後方正則保存性をもつと予想しており，その厳密な証明に取り組む．これを応用し，RPDSのLTLモデル検査問題が判定可能かどうかも明らかにする．
|
