Dec. 2023No.101
Interview
バグのないソフトウェアを目指して
世の中のさまざまな機器がソフトウェアで制御される現代において、バグは重大なトラブルを引き起こす。関山 太朗 准教授は、そうしたトラブルを防ぐべく、ソフトウェア科学の研究に取り組んでいる。
関山 太朗SEKIYAMA, Taro
国立情報学研究所
アーキテクチャ科学研究系 准教授
プログラミング言語理論でソフトウェアの安全性を検証
── ソフトウェア科学の分野において、どのような研究を進めているのでしょうか。
私が目指していることは一貫して、安全なソフトウェアを実現することです。ソフトウェアにバグ（欠陥）があると、例えば自動運転で人の命に関わる事故が起きたり、多額の仮想通貨が取引所から盗まれる事件が起きたりします。そのような事態を防ぐために、プログラミング言語理論を利用して、ソフトウェアにバグがないことを証明する研究を進めています。
プログラミング言語理論とは、プログラミング言語の意味や計算モデルを研究する学問です。仕事や社会に役立つソフトウェアを直接実装するわけではないのですが、バグのない正しいソフトウェアを書くにはどうしたらいいのかといった、ソフトウェアが重要な役割を持つ現代社会では大きなインパクトにつながる研究です。
── どのようにバグが存在しないことを証明するのでしょうか。
プログラミング言語理論の研究は数学的な手法で行われますが、そのためにはバグとはどういうものか、また関連したプログラムはどう動くべきかということを数学的に定義する必要があります。その上で与えられた定義に従ってプログラムが正しく動作しているかを検証することになります。
── どのようにバグが存在しないことを証明するのでしょうか。
プログラムのバグを検出する方法の一つに、式にさまざまな型を割り当て、値が正しく使われているかどうかを検査する、「型システム」があります。これまでの型システムは、大きく分けて二つあり、一つ目の「動的型付け」は、値の型をあらかじめ決めずに、プログラム実行時の実際の値によって正しく動作しているかどうかを検証する手法で、プログラムの実行を通して発見された誤りを報告してくれます。これに対して、「静的型付け」はプログラム実行前に、形式に合った正しい型のデータのみを処理することを検証・保証する手法になります。プログラムの実行前に型検査を行うことで、実行時にエラーが必ず起きないことを保証することができます。
現実でより使いやすい検証技術の開発を目指して
── 現在取り組んでいる研究について教えてください。
私が今進めている研究の一つは、いわゆる「副作用」を起こすソフトウェアの安全性を、静的型付けによって保証する研究です。副作用とは、「プログラムと外部環境とのインタラクション（相互作用）」のことで、例えば「メモリやストレージといった記憶装置の使用」「キーボードやマウスによるユーザーからの入力」「複数の計算が相互に依存しながら実行される状態（並列・並行計算)」といったものがあります。こうしたさまざまな副作用を統一的に捉える枠みとして、代数的作用 （副作用の意味を代数的に定義する仕組み)があり、これを静的型付けに取り入れることでさまざまな副作用を引き起こすソフトウェアの安全性を検証する研究を行っています。
── ゼロトラストによってIoTシステムを守る研究も進めているとのことですが、具体的にはどのような内容ですか。
従来のセキュリティ手法ではネットワークの内 外を区 別する「境界」を設け、守るべき情報資産へのアクセスを内部だけに限定することで安全性を確保していました。しかし、昨今ではこのような境界を設け、外部から内部への侵入を防ぐだけでは不十分になりつつあります。そこで「ゼロトラスト」という、境界の概念を捨て去り、情報資産にアクセスするものは全て信用せずに安全性を検証するという考え方が登場してきています。我々はソフトウェア理論とシステムソフトウェアの融合によって、ゼロトラストの概念を踏襲した、安全なIoTシステムの実現を目指しています。
理論研究では、IoTシステムの数学的モデルに基づく静的検証と実行時検証の融合を目指しています。また、システムソフトウェア研究では、理論的成果と連係して実行隔離・自動検知・自動対処機構を開発し、ゼロトラストIoTシステムを実証することを目指します。
「なんとなく」に数学的構造を見つけて事件や事故を防ぐ
──ソフトウェア科学を研究することの面白さはどこにあるのでしょうか。
私がソフトウェア科学、特にプログラミング言語理論に興味を持ったきっかけは、友人から教えてもらったプログラミング言語理論に関する書籍を読み、プログラムに数学的な構造を当てはめることができると知ったことでした。人間がなんとなくこう動くだろうと思っているソフトウェアに、きちんと数学的な構造を見つけてその意味を発見する。何があるのか分からないジャングルの中から、宝物を見つけるような感覚です。そういう発見が、コンピュータシステムの誤動作を防ぎ、実世界で起きる事故や事件を防ぐといった、大きな社会貢献につながると思っています。
── そうした研究に、国立情報学研究所（NII）の環境は適しているのですね。
そうですね。ここでは情報系の研究者が一つの建物に集まっているので、何か相談したいと思ったら、気軽に声を掛けられます。他の大学の場合、同じ分野の研究科でもキャンパスが分かれていることもあるので、みんなで議論しやすいのは良い環境だと思いますね。
一方でNIIは、一般的な大学のように教授や准教授、助教が一緒になって一つの研究に取り組むのではなく、個々の研究者が独立して研究できるという特徴もあります。一人で黙々と研究に専念できる環境でもあるのです。とはいえ、特に若手の研究者は積極的に他の研究者とつながって、いろんなコラボレーションをした方が、研究範囲が広がり面白いと思います。私自身も、現在NIIの中で包括的ソフトウェア研究として三つのプロジェクトに関わっており、いろんな先生からさまざまな知識を吸収しています。