理論を現実の問題に：
信頼できるソフトウェア、セキュアなシステム

※新規の学生受入は行っていません

小川研究室　OGAWA Laboratory
教授：小川 瑞史（OGAWA Mizuhito）

E-mail：
［研究分野］
理論計算機科学、形式手法
［キーワード］
Formal language, Combinatorics, Rewriting systems, State transition systems, Formal methods, SMT solver, Binary code analysis

研究を始めるのに必要な知識・能力

数学的思考能力（離散数学・数理論理・形式言語・組み合わせ理論などにおける基礎概念の深い理解。つまり数学的定義が再構成できること、そのノントリビアルな実例を３つあげられること）、および英語による論理的コミュニケーション能力・読み書きの能力。（研究室内のセミナーは英語。読む文献は英語論文が基本です。修士論文も英文が望ましく、博士論文は英文が必須となります。）

この研究で身につく能力

本研究室は、企業等ですぐに役立つ知識や技術の習得は目的としません。かわりに、基本的概念の理解と理論に基づき現実の問題に挑戦する方法論、未知の領域に対する学習とアプローチ法の習得を目的とします。具体的には、学生の興味と能力に応じ、理論問題（過去には定理証明手法など）や、形式手法における推論・解析ツールの研究開発（過去には、制約解消系、セキュリティプロトコル解析、Java コード解析、丸め誤差自動解析、バイナリコード解析、SQL の形式意味の代数的仕様記述など）から、問題設定・アプローチの考案・アイデアの具体化・プロトタイプ実装・論文執筆のサイクルを経験してもらい、上記方法論習得のケーススタディとします。これらの能力の習得を標準年限での修了より重視しています。

【就職先企業・職種】 大学、研究機関（博士）、ソフトウェア関連企業（修士）

研究内容

　現在、計算機科学の成熟、計算機の高速化により、実用的システムの高信頼化へ応用可能性を拡げています。例えばモデル検査、充足性検査、定理証明などの自動推論技術は、現在の CPU 開発には欠かせぬものとなっています。
　本研究室は、計算モデル・アルゴリズム・離散数学等の基礎理論、その成果の自動推論ツールへのプロトタイプ実装、さらに現実のソフトウェアへ応用可能性を追求しています。主な理論分野は、組み合わせ理論（グラフ理論や順序構造）、書換系、形式言語、数理論理、数学的証明の形式化などです。その際、一見無関係に見える理論的成果の結合、忘れられた理論的成果の温故知新を重視します。
　ツールのプロトタイプ実装は、既存ツールの最大限の利用と拡張を試み、それらの限界を明らかにした上で行います。現在の計算量理論は実用的効率を正しく反映していません。たとえば SAT ソルバのように NP 完全だが現実のシステム検証では高速な場合も多くあります。理論的に解明できなくとも、定性的原理に従い、実用的アルゴリズムを設計し、実験により有効性を示すなどのアプローチを試みています。
　具体的な研究トピックとして、以下の項目を主に国際共同研究により進めています。

1．形式言語の単調なWell-Quasi-Order (WQO) による特徴付け：

有限語の正規言語の合同関係による特徴付けは Myhill-Nerode定理として広く知られています。単調なWQOによる特徴付けは1982年にEhrenfechetらにより提案されました。ω語の正規言語の合同関係による特徴付けは古くはBuchiにより当たられています。本研究室では、単調なWQOによる特徴付け、ならびにそのための必要十分条件として周期的拡張と連続的拡張の概念を提案し、その性質を示しました。現在、性質の深化とともに他のデータ構造・形式言語クラスに対し、研究を進めています。（ロシア・エルショフ研究所、カザン連邦大学と共同）

2．Well-Structured Pushdown System（WSPDS）の決定可能性：

スタックを持つ無限状態遷移システムに順序構造（Well Quasi Order）による制 約を仮定することで、被覆可能性を含む様々な性質の決定可能性を示す一般的な枠組み WSPDSを提案しました。WSPDS は並行プログラム、実時間システムの多くの既存モデルの決定可能性を統一的に扱うことができます。さらにVASS (Vector Addition System、ペトリネット）の到達可能性、Branching VASSの到達可能性の決定可能性への応用の研究を進めています。（上海交通大学、名古屋大学、サンクトペテルスブルグ大学と共同）

3．非（左）線形項書換系の合流性の十分条件：

項書換系の主たる性質は合流性と停止性です。非停止な項書換系における合流性の十分条件は1970年代に提案された左線形・無曖昧性が基本です。左非線形の場合は1980年代より研究されていますが、多くの問題が未解決です。左線形にかえ右線形の場合の合流性（1990年の未解決問題）に対し共同研究を進めています。（名古屋大学、仏 Ecole Polytech-nique・清華大学と共同）

4．実数上の非線形制約解消系（SMTソルバ）raSATの実装開発：

もともとの動機は、mpeg4 など DSP デコーダーにおける丸め誤差自動解析（組み込みシステム等では、リファレンスアルゴリズムの浮動小数点演算を固定小数点演算に変更することが多いため、誤差が生じる）でしたが、その推論エンジンに注目し、実数・整数上の非線形制約（多項式制約）充足性検査系 raSAT の研究を進めています。国際競技会 SMT-COMP 2016、2017では QF_NRA カテゴリで Yices2に次ぐ2位を獲得しました。現在、LORIA で開発する veriT との融合を進めています。（仏ロレーヌ大学 LORIA、ベトナム国家大学ハノイ校と共同）

5．マルウェアを対象としたバイナリレベル動的記号実行器：

PC マルウェアは、比較的小規模なバイナリコードですが、アンチウィルスソフトをかいくぐる隠蔽手法が用いられているため、その制御構造は非常に複雑です。たとえば、バイナリコードにはデータとコードの区別がないことを利用した自己改変、制御のジャンプ先や戻り先隠蔽、特定の API 実行による sandbox 環境検出はポピュラーな手法です。ここでは動的記号実行を用いたプッシュダウンモデル生成器 BE-PUMを開発し、PC マルウェアのx86ディスアセンブリとマルウェア作成時に使用されたパッカー同定に成功しました。現在、ARM, MIPSなどIoTデバイスで用いられる他プラットフォームへの拡張をめざし、命令セットの英語マニュアル（自然言語仕様）から形式的意味の自動抽出を行い、動的記号処理系自動生成に成功しました（Githubにて公開）。今後、マルウェアのディスアセンブルによるマルウェア手法の意味解明や、IoTマルウェアの制御構造による分類を目的とした深層学習を試みています。（ベトナム国家大学ホーチミン校、ベトナム・レクイドン工科大学、仏ロレーヌ大学 LORIA と共同）

6．オートマトン操作に基づく決定手続きの効率化：

オートマトンはその制約（有限オートマトン、プッシュダウンオートマトン等）により、さまざまな決定可能性を持ち、ソフトウェア検証に用いられています。しかし理論計算量はしばしば指数時間となり状態爆発を起こします。実用的手法として、漸増的生成に加え、アンチチェーンに基づくアルゴリズムが有力です。本研究室では、過去に Visibly Pushdown Automaton への拡張を行いましたが、原点に戻り、アンチチェーンアルゴリズムの各要素の精査と形式化を通じて、その原理の理論的解明と効率化を進めています。（墺インスブルック大学と共同）

主な研究業績

1. V.A.Vu, M.Ogawa: Formal Semantics Extraction from Natural Language Specifications for ARM. 23rd International Symposium on Formal Methods (FM 2019), LNCS 11800, 465-483, 2019.
2. M.Ogawa, V.L.Selivanov: On Classes of Regular Languages Related to Monotone WQOs. 21st International Conference on Descriptional Complexity of Formal Systems (DCFS 2019), LNCS 11612, 235-247, 2019.
3. T. X. Vu, V. K. To, M. Ogawa. raSAT : An SMT Solver for Polynomial Constraints. Formal Methods in System Design 51(3). 462-499, 2017.

使用装置

通常のノートＰＣがあれば十分です。