本文へジャンプ

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

小川研究室 OGAWA Laboratory
教授:小川 瑞史(Ogawa Mizuhito)

E-mail:mizuhitojaist.ac.jp
[研究分野]
理論計算機科学、形式手法
[キーワード]
Formal language, Rewrting systems, infinite state transition systems, Formal methods, SMT, Binary analysis

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

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

この研究で身につく能力

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

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

研究内容

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

1.Well-Structured Pushdown System(WSPDS)の決定可能性

スタックを持つ無限状態遷移システムに順序構造(Well Quasi Ordering)による制約を仮定することで、さまざまな性質の決定可能性を示す一般的な枠組み WSPDS を提案しました。WSPDS は並行プログラム、実時間システムなどのさまざまなモデルの決定可能性を統一的に扱うことができます。(上海交通大学・名古屋大学と共同)

2.非(左)線形項書換系の合流性の十分条件

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

3.実数上の非線形制約解消系(SMTソルバ)raSATの実装開発

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

4.マルウェアを対象としたバイナリコード解析系BE-PUM

マルウェアは、比較的小規模なバイナリコードですが、アンチウィルスソフトをかいくぐる隠蔽手法が用いられているため、その制御構造は非常に複雑です。 たとえば、バイナリコードにはデータとコードの区別がないことを利用した自己改変、制御のジャンプ先や戻り先の隠蔽、特定のAPI 実行による sandbox 環境の検出はポピュラーな手法です。ここでは動的記号実行を用いたプッシュダウンモデル生成器BE-PUM(bepum.jaist.ac.jp にて公開)を開発し、正確なマル ウェアのディスアセンブリとマルウェア作成時に使用されたパッカー同定に成功しています。(ベトナム国家大学ホーチミン校、仏ロレーヌ大学LORIA と共同)

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

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

6.定理証明系Isabelle/HOL を用いた存在証明の分析

古典論理による存在証明は、アルゴリズムに対し奇妙な現象を引き起こします。たとえば Graph-minor 定理は、多くのグラフ問題に対し二乗時間アルゴリズムの存在を保証しますが、アルゴリズム自体が構成できない問題も多く知られています。ここでは、定理証明系Isabelle/HOL 上の形式証明(Higman、Lovaszの補題等)に対する構造解析・変換によるアルゴリズム抽出を目的にしています。

主な研究業績

  1. T. X. Vu, V. K. To, M. Ogawa. raSAT : SMT Solver for Polynomial Constraints. IJCAR 2016, Springer LNCS 9706, pp.228-237.
  2. G. Li., M. Ogawa, S. Yuen, Nested Timed Automata with Frozen Clocks, FORMAT 2015, Springer LNCS 9268, pp.189-205.
  3. M. H. Nguyen, M. Ogawa, T. T. Quan, Obfuscation code localization based on CFG generation of malware, FPS 2015, Springer LNCS 9482, pp.229-247.

使用装置

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

研究室の指導方針

本研究室は企業等ですぐに役立つ知識や技術の習得は目的としません。かわりに、基本的概念の理解と理論に基づき現実の問題に挑戦する方法論、未知の領域に対する学習とアプローチ法の習得、自らの深い思考による論理構成力を目的とし、学生の興味と能力に応じたソフトウェア分野での問題設定により研究の一サイクルを経験してもらいます。各学生は全く異なる研究トピックを前提とします。理論研究を基礎とし、本人の希望と能力により、実装との比率を勘案します。プログラミング言語は Ocaml, Maude などの関数型言語を習得し、実装は主にそれらを用います。さらに学位論文の執筆を通して、総合的な表現力の体得をめざします。これらの能力の習得を標準年限での修了より重視しています。

[研究室HP] URL:http://www.jaist.ac.jp/~mizuhito

ページの先頭へもどる