寺内研究室 教授 寺内多智弘
プログラミング言語分野の研究を行っています。特に、プログラムの正しさを自動的に検証する「プログラム検証」や正しいプログラムを自動生成する「プログラム合成」の研究、およびプログラム検証・合成技術のセキュリティへの応用に興味があります。加えて、型システム、数理論理学と(特に自動)定理証明、形式言語理論とオートマトン理論など基礎理論・基礎アルゴリズムに関する研究も行っています。
近年、コンピュータソフトウェアは生活のいたるところで使用されており、ソフトウェアの不具合は大きな社会的課題となっています。また、テスト実行など従来のソフトウェア開発手法では、複雑化を増すソフトウェアの品質を保証することが難しくなっています。そこで、コンピュータアルゴリズムにより正式かつ機械的にプログラムの正しさを検証することや、正しいプログラムを機械的に合成することにより、ソフトウェアの信頼性を向上しよう、というのが研究のねらいです。特に、本研究室では、型システム、数理論理学と(特に自動)定理証明、形式言語理論とオートマトン理論、形式検証理論など理論に根ざした手法の研究を行っています。
早稲田大学基幹理工学部のClose Upにバグのないソフトウェアを目指して：近年のプログラム検証研究の動向という記事を寄稿しました。そちらも参考にしてください。
研究室の論文は寺内のホームページから参照してください。
プログラム検証とは、プログラムコードを解析し、プログラムが仕様通り動作するか検証することです。近年、SAT/SMT/CHCソルバなど自動定理証明技術の著しい進歩もあり、ソフトウェアモデル検査など高精度な自動プログラム検証手法が注目されています。プログラム検証の研究には、扱える言語機能の拡張(例えば、高階関数の扱い)など様々な課題があります。当研究室では、高階関数や代数的エフェクト(algebraic effects)などを含む高レベル言語で記述されたプログラムを効率よく検証する技術を研究しています。加えて、関係性仕様(relational property)やハイパー性質(hyperproperty)と呼ばれる複数のプログラム実行に関する性質の検証の研究なども行っています。
仕様や入出力例などから自動的に正しいプログラムを生成することをプログラム合成といいます。プログラム検証と同様、自動定理証明技術を用いることが多く、これら技術の発展により急速に研究が進んでいます。当研究室では、SMTソルバを分割統治法的に使いサイドチャネル攻撃に対する耐タンパコードを合成する手法や、例を用いてReDoS(Regular expression Denial of Service)攻撃に対して非脆弱な正規表現を合成する手法などを研究しています。
プログラム検証・合成などプログラミング言語研究の技術をセキュリティに応用することができます。上記のサイドチャネル攻撃に対する耐タンパコードの合成やReDoS非脆弱な正規表現の合成はその例です。当研究室では、上記の例題の他、機密情報漏洩の検出・防衛に関する研究やタイミング攻撃の検出・防衛に関する研究なども行っています。
プログラミング言語研究には、定理証明など数理論理学に関する理論・アルゴリズムが深くかかわります。自動定理証明は論理式の真偽性を自動的に判定するアルゴリズムです。上記の通りプログラム検証・合成に不可欠な技術であり、当研究室でも自動定理証明および密接に関連する制約解消アルゴリズムの研究を行っています。特に、近年は、数学的帰納法のある種の形式化である循環証明(cyclic proof)という証明体系や、不動点論理(fixpoint logic)という再帰的(より正しくは、帰納的・余帰納的)に述語を定義することのできる論理体系に対する自動定理証明アルゴリズムなどを研究しています。
型システムは、型エラーが実行時に起こらないことを保証し、Javaなど多くのプログラミング言語が備え持つなど、正しいプログラム開発の重要な一端を担っています。当研究室では、まだ実用的なプログラミング言語への導入は限られている交差型(intersection types)、依存型(dependent types)、篩型(refinement types)、型エフェクトシステム(type and effect)、代数的エフェクト(algebraic effects)のための型システムなど、先進的な型システムについての研究を行っています。
拡張正規表現とは、後方参照(backreference)、先読み(lookahead)、後読み(lookbehind)といった古典的正規表現にはない拡張機能を含む正規表現です。当研究室では、どの拡張機能を含む拡張正規表現がどんな言語を表すことができるのか(すなわち、表現力の解明)など拡張正規表現の形式言語理論の研究を行っています。加えて、このような拡張機能は多くの現実の正規表現処理エンジンで実際にサポートされているものであるため、理論のみならず実用的にも重要な課題となっています。上記ReDoSに関する研究も拡張正規表現を対象にしています。
プログラミング言語 数理論理学 形式検証 形式言語理論 セキュリティ プログラム検証 プログラム合成 自動定理証明 型システム