|
研究協力者らとともに，以下を含む研究を行なった．
・セキュリティ型付きλ計算の環境双模倣の検証と改良．情報を「高機密」「低機密」ないし「高信頼」「低信頼」に「静的に」（プログラム実行前に）分類する「セキュリティ型システム」を備えた計算モデルにおいて，現実的に必要な高機密から低機密への「非機密化」の操作があってもある種の安全性を証明する「環境双模倣」（研究代表者らによるプログラム等価性の理論）に対し，「定理証明支援器」による厳密な検証を試み，型システムを改良した．
・並行性・非決定性・状態・暗号を備えたNetKAT．いわゆるインターネットのようなネットワークにおける「パケット」（通信データ）処理を記述・検証する体系であるNetKATに対し，同時に複数の処理が行われる「並行性」，タイミング等によって異なる処理が行われる「非決定性」，複数の通信主体が共有する「状態」，および暗号化・復号の操作を導入した．本研究により，従来のNetKATは「並行性」と「非決定性」の区別が困難で，「リプレイ攻撃」を防ぐ等の目的で「状態」を持つ現実的なシステムを十分に表現できず，NatKATの正則言語に適切な並行演算子を導入する必要があることがわかった．
以下については字数制限および引き続き研究中につき詳細は省略する．・Polymorphic gradual typing with holes．・型システムを用いたロックフリースタックの検証．・Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion.
|
