本文へジャンプ

理論に基づく正しいソフトウェア開発:
バグのないソフトウェアを目指して

寺内研究室 TERAUCHI Laboratory
教授:寺内 多智弘(Terauchi Tachio)

E-mail:terauchijaist.ac.jp
[研究分野]
プログラミング言語、プログラム検証、プログラム解析、情報セキュリティ
[キーワード]
型システム、自動定理証明、ソフトウェアモデル検査、ソフトウェア工学

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

数理論理・集合論など基礎理論について基本的な知識があることが望まれます。また、特に言語の指定はありませんが、プログラミングができることが望まれます。また、必須ではありませんが、計算量理論・コンパイラ・情報セキュリティなどについての知識があるとよいです。

この研究で身につく能力

プログラミング言語およびソフトウェア(プログラム)検証・解析について最先端の研究を学ぶことができます。指導教員の寺内は、POPL・PLDI・LICS・TOPLASなど本研究分野の最高峰の国際会議・国際ジャーナルに論文を通すなど国内有数の研究業績を誇り、高い水準の研究指導を行います。

【就職先企業・職種】 情報通信業・情報処理産業・電気電子産業など

研究内容


図1.自動抽象詳細化による高階プログラム検証の概要

図2.情報漏洩解析問題の分類

背景:

今日の情報化社会において、コンピュータソフトウェアは生活のいたるところで使用されており、ソフトウェアの不具合は大きな社会的課題となっています。不具合を検出・防止する手段としてプログラム解析・プログラム検証があります。これは、ソフトウェアプログラムを自動的に解析し不具合を検出し、また、逆に不具合が起こり得ないということを数理論理的に保証する技術です。プログラム解析・検証は数理論理学・プログラミング言語・定理自動証明など複数の研究分野を横断する研究です。

最近の研究テーマ:

①高レベル言語プログラムの検証
近年、マイクロソフト社のSLAMモデル検査器など、「ソフトウェアモデル検査」によるプログラム検証が注目を集めています。しかし、現在のソフトウェアモデル検査は主にC言語など低レベル言語で記述されたプログラムを対象にしており、関数型言語やオブジェクト指向言語で記述された高階関数・オブジェクトなど高レベル機能を含むプログラムは上手く扱えません。本研究室では、高レベルプログラムに対して有効なソフトウェアモデル検査技術の確立を目指し研究を推進しています。例えば、型システムを用いた高階プログラムの到達可能性検証の手法を提案するなど、この研究で顕著な業績を上げています。
②よりよい抽象詳細化アルゴリズム
ソフトウェアモデル検査など多くの近年のプログラム検証の鍵となる技術が、「述語論理式によるプログラムの抽象化」です。2000年代にプログラム展開等で得た「プログラムの部分」から抽象化に用いる適切な述語を推論する手法が提案され、現代のプログラム検証の発展に大きな影響を与えました。本研究室では、よりよい述語発見を目指し研究を推進しています。例えば、分岐を含むプログラム部分に対して効率よく述語発見を行う手法や、述語が検証全体に与える影響の理論的解明についての研究などを行っています。
③情報セキュリティへの応用
個人情報など機密情報を扱うプログラムが第三者に情報漏洩を行わないかの検証、また、攻撃によりどれほどの情報漏洩が起こり得るのかの解析などの研究を行っています。また、これは、外部からの攻撃に対して強固なシステムの構築に役立つなど、情報セキュリティ研究分野とプログラム解析・検証研究分野を縦断する研究となっています。本研究室は、情報漏洩量をプログラム変換とソフトウェアモデル検査を用いて自動的に解析する手法を提案するなどこの分野で顕著な業績を挙げています。また、近年では、サイドチャネル攻撃に対する耐タンパー技術への応用なども研究しています。

主な研究業績

  1. A. Murase, T. Terauchi, N. Kobayashi, R. Sato, and H. Unno. Temporal Verification of Higher-Order Functional Programs. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pp. 57-68, ACM, January, 2016.
  2. T. Terauchi. Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR. In Proceedings of the 22nd International Static Analysis Symposium (SAS 2015), Lecture Notes in Computer Science 9291, pp.128-144, Springer, September, 2015.
  3. H. Yasuoka and T. Terauchi. Quantitative Information Flow - Verification Hardness and Possibilities. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium(CSF 2010), pp.15-27, IEEE Computer Society, July, 2010.

研究室の指導方針

輪講・学生主導型ゼミ・指導教員とのミーティングなどを定期的に行うことにより研究指導を行います。輪講では、オートマトン・形式言語・計算量理論など基礎的な理論計算機科学、また、型システム・定理証明・モデル検査など応用的課題について学習します。また、修士および博士学位論文執筆・プレゼンテーションの指導を行います。また、学生の力量に応じて、雑誌論文・会議論文など学術論文執筆の指導を行います。

[研究室HP] URL:http://www.jaist.ac.jp/~terauchi/index-j.html

ページの先頭へもどる