【研究分野】ソフトウエア

【研究領域課題番号】23700026 (KAKENデータベースで見る）

【研究キーワード】

セキュリティ / プログラミング言語 / プログラム検証 / 量的情報流 / 情報セキュリティ / プログラム解析 / ソフトウェアモデル検査

【研究成果の概要】

量的情報流の困難性に関する研究を行い、beliefやmin entropy channel capacityなど様々な情報理論的尺度に基づく量的情報流に関する検証・推論問題の困難性を解明した。計算量理論的困難性のみならず、「hyperproperty」と呼ばれるプログラム検証問題の分類を用いての困難性も考察した。また、ソフトウェアモデル検査技術と#SATソルバ等カウンティングアルゴリズムを応用した高精度な量的情報流上限検証・推論アルゴリズムを提案した。また、検証アルゴリズムの基礎となるソフトウェアモデル検査技術の改良に関する研究を行った。

【研究種目】若手研究(B)

【研究期間】2011 - 2013

【配分額】4,160千円 (直接経費: 3,200千円、間接経費: 960千円)

【研究分野】ソフトウエア

【研究領域課題番号】21300006 (KAKENデータベースで見る）

【研究キーワード】

横断的関心事 / アスペクト指向 / 文脈指向 / セキュリティ / 意味論 / 型安全性 / プログラミング言語 / モジュール性 / 最適化 / アスペクト指向プログラミング / セキュリティーポリシー / イベント駆動 / 文脈指向プログラミング / モジュール化 / EventCJ / ContextJ / セキュリティポリシー / AspectJ / 分散ソフトウェア

【研究成果の概要】

横断的関心事や環境に適応した振舞をモジュール化するアスペクト指向プログラミング・文脈指向プログラミング言語に関して、基礎的な計算体系の構築・型システムの改良による記述力の向上・セキュリティ応用のための言語提案・事象に基づく制御機構を持った言語提案による応用範囲の拡大といった研究を行った。これらの提案はJava,AspectJを拡張した言語処理系を作成し、実際のアプリケーショプログラム記述を通して有効性を検証している。

【研究種目】基盤研究(B)

【研究期間】2009 - 2012

【配分額】12,350千円 (直接経費: 9,500千円、間接経費: 2,850千円)