HOME > 研究紹介 > プログラミング言語研究室

研 究 紹 介
プログラミング言語研究室
システムソフトウェア・ネットワーク分野 千代 英一郎 准教授

プログラムを科学する

計算機の誕生から半世紀以上経った現代では膨大な数の計算機およびプログラムが交通・金融・医療など各分野で我々の生活を支える基盤として働いています。安心して暮らせる社会を実現するために、このようなプログラムを科学的に分析しその正しさを確認する手段が求められています。本研究室ではプログラミング言語理論・数理論理学にもとづき、プログラムの振る舞いや性質の解析・検証・変換技術の研究に取り組んでいます。

研究内容

本研究室の一番の特徴は研究対象がプログラムであるということです。対象プログラムが与えられたときに、そのプログラムの持つ性質(たとえば実行中にエラーが発生することはない等)を静的に調べるための理論や技術を扱います。

そのようなことは実行してみればわかるのに? と思うかもしれませんが、実行してわかるのはあるひとつの状況、たとえばひとつの入力パターンにおける動きでしかありません。そうではなく、どのようなときにも成り立つ性質を得るためにはプログラムからその振る舞いを表す数学的モデルを作り網羅的に解析を行う必要があります。物体の動きを調べるときには運動方程式などの微分方程式によって数学的にモデル化するということをしますが、同様のことをプログラムを対象に行うと考えてください。ただし使うのは微分方程式ではなく状態遷移系や論理式を用います。

研究課題としては、モデルをどう定義すべきか、プログラムからどのようにモデルを生成するか、およびそれをどう調べるかが大きな柱になりますが、これらのすべてにプログラムの意味を数学的に基礎づけるプログラミング言語理論が大きく関係しています。

下の図は本研究室で扱う代表的な分野です。網羅的に振る舞いを調べるという特徴は、特にプログラムの信頼性やセキュリティのような、不具合が許されない問題を扱うのに適しています。

本研究室で扱う代表的な分野

ここにあげた分野以外にもデータベース分野やセマンティックweb分野における各種問い合わせ(これもプログラムの一種です)への応用も検討しており、特にグラフ構造を持つデータを対象に準同型写像を利用した研究を進めています。

研究テーマ例: webセキュリティ脆弱性検査技術

本テーマはwebサービスと総称される種類のソフトウェア(プログラム)を対象とする研究です。わかりやすい例としてはamazonや楽天のようなオンラインショップをイメージしてもらえればよいかと思います。このようなサービスを実現するプログラムにセキュリティ上の不備(脆弱性)があると、そこで管理されている個人情報の流出(情報漏洩)等、システムに多大な被害をもたらす危険性があります。この種の問題はたえず発生しており、時には100億円以上にも及ぶ対策費が必要になるケースも報告されています。

有名なセキュリティ脆弱性のひとつにSQLインジェクションがあります。SQLインジェクションはプログラムにおけるSQL文の発行方法の不備により発生する脆弱性で、悪意のある外部の攻撃者によりデータベース内の情報が外部に流出したり、データベースの内容が書き換えられるといった大きな被害につながる危険性の高いものです。昔から知られているにもかかわらず2012年のIPA報告でも今だに被害件数は最多であり、その防止技術が求められています。

本研究室ではプログラムを解析しSQLインジェクション脆弱性の有無をサービス開始前に検知するための技術を研究をしています。下図は開発中のツールによるJava Servletプログラムの検証例です。画面中央の赤い×マークに脆弱性の発生源が存在することを指摘しています。

開発中のツールによるJava Servletプログラムの検証例

copyright(C) Seikei University. all rights reserved.