TOKYO TECH CYBERSECURITY

南出研究室の紹介

研究テーマ

ソフトウェア検証，プログラミング言語，形式言語理論

現在の社会は，ソフトウェアへの依存度をますます高めており，その信頼性の向上が課題となっています。例えば，ウェブに関連したソフトウェアにおいては，プログラムの小さな誤りが，クロスサイトスクリプティングや SQL インジェクションなどの脆弱性の原因となり，情報漏洩などの深刻な問題を起こしています。本研究室では，ソフトウェアの信頼性を高めるための理論や技術を研究しています。特に，形式言語やオートマトンの理論に基づく検証技術の研究に注力しています。

研究内容

1. 形式言語理論のソフトウェア検証への応用

ソフトウェアの解析・検証に，形式言語理論（オートマトン，文脈自由文法などの理論）を応用します。PHP プログラムの性質・安全性の検証を文脈自由言語の理論を用いて行う研究や，HTML5 の構文解析器の解析にプッシュダウンオートマトンを利用する研究などを行っています。理論が実際の問題の解決に生かせます。

2. プログラミング言語の理論と実装

関数型プログラミング言語の型理論やコンパイラの研究を行ってきました。現在は，ウェブに関連したプログラミング言語に関する研究を主に行っています。近年の研究成果としては，文字列を操作するプログラムで重要な役割を果たす正規表現マッチングの計算量（オーダ）を決定する手法を開発しました。これは，正規表現マッチングが原因となるDoS 脆弱性(ReDoS) の検出に応用できます。

3. 証明支援系・定理自動証明器の応用

証明支援系は，コンピュータ上でプログラムを書くように証明を書くためのシステムです。近年，証明支援系が，ソフトウェア検証，数学の証明，プログラム言語理論などで利用されるようになってきています。本研究室では，コンパイラの検証，形式言語に関する新しいアルゴリズムの正当性の証明等で，証明支援系を利用してきています。