平成30年3月更新

寺内研究室 教授 寺内多智弘

当研究室を希望する方へ

プログラミング言語分野の研究を行っています。特に、「正しいソフトウェアの開発」を目標とし、プログラム検証、プログラム合成などの研究を行っています。

研究概要

近年、コンピュータソフトウェアは生活のいたるところで使用されており、ソフトウェアの不具合は大きな社会的課題となっています。また、テスト実行など従来のソフトウェア開発手法では、複雑化を増すソフトウェアの品質を保証することが難しくなっています。そこで、コンピュータアルゴリズムにより正式かつ機械的にプログラムの正しさを検証したり正しいプログラムを合成することにより、ソフトウェアの信頼性を向上しよう、というのが研究のねらいです。特に、本研究室では、定理証明・型システムなど数理論理学・理論計算機科学に根ざした手法の研究を行っています。

近年の研究テーマ

高レベル言語プログラムのためのソフトウェアモデル検査

近年、「ソフトウェアモデル検査」と呼ばれる高精度な自動プログラム検証手法が注目されています。これらは、SAT/SMTソルバなど近年急速に発展した自動定理証明技術を用いる手法であり、産業界でも検証器の開発・導入が進むなど(Microsoft, Facebook等)高い関心を集めています。 近年、本研究室では、国内外の研究者らと共同で(東京大学・筑波大学・米スティーブンス工科大学)、OCaml言語など高レベル言語で記述されたプログラムを効率よく検証するソフトウェアモデル検査手法を研究しています[POPL 2010, POPL 2013, CSL-LICS 2014, POPL 2016, POPL 2018]。

プログラム合成

近年、仕様や入出力パターン例などから自動的に求めたいプログラムを生成するプログラム合成の研究が盛んに行われており、商業ツールにも取り入られるなど(Microsoft FlashFill等)著しい成長を遂げています。本研究室では、分割とサンプリングにより、効率よく耐タンパ化された論理回路を生成する研究などを行っています[POST 2017]。

情報セキュリティへの応用

プログラム検証・合成などプログラミング言語技術を用いたセキュリティに関する研究を行っています。近年では、上記耐タンパ性合成の研究の他、量的情報流という機密情報漏洩の検出・防衛に関する研究[QAPL 2012, ESORICS 2010, CSF 2010]やタイミング攻撃の検出・防衛に関する研究[PLDI 2017]などを行っています。

分野キーワード

プログラミング言語   数理論理   ソフトウェア工学   情報セキュリティ   プログラム検証   プログラム合成   自動定理証明   型システム