安全性の高いシステムソフトへ一歩前進
C言語→型付きアセンブリ言語への変換で
前田助教ら、数年後にも実用化を目指す

　コンピュータ科学専攻の前田俊行助教らのチームは、C言語で記述されたプログラムを型付きアセンブリ言語に変換する手法を考案した。これにより、C言語で記述されたシステムソフトウェアの安全性保証に向けて一歩前進した。この研究は、JSTのCREST研究領域「実用化を目指した組み込みシステム用ディペンダブル・オペレーティングシステム」の研究課題「ディペンダブルシステムソフトウェア構築技術」の一環。C言語から型付きアセンブリ言語に変換するのに大きな制約条件がないため、幅広い応用が期待できる。安全性、信頼性の確保が要求される計算機システムにとって朗報で、プログラムの実行性能に関する問題等を解消できれば、数年後には実用化したい考え。

　計算機システムで最も重要なソフトウェアの一種であるOSなどのシステムソフトウェアは、主にC言語で記述されている。しかし、C言語は安全な言語ではないため、誤って記述された安全でないC言語プログラムが、実行時に異常動作したり、機密情報が漏洩したりする危険性が指摘されており、実際、多くの問題が生じている。システムソフトウェアの記述においては、C言語よりも適した言語がなかったことも相まって、現在まで長い間使われてきた。また、C言語で記述したシステムソフトウェアを安全性の高い言語で書き直そうとすると、膨大なコストがかかるのがネックだった。

※画面をクリックして拡大画像をご覧下さい

　これに対し、前田助教らのチームは、安全性、信頼性を高める技術的手段として、型付きアセンブリ言語技術（型理論に基づいて設計されたアセンブリ言語）に注目した。型理論とは、プログラム中の変数やメモリー上のデータがどのような「型」を持つかを解析し、実行時に変数が誤って利用されて異常が発生しないかどうかなどを検査するための理論。この検査により、プログラムが実行中に不正なメモリー操作を行ったり、不正なコード実行を行ったりすることを、プログラムのソースコードなしに未然に防ぐことができる。

　前田助教らのチームは、従来の型付きアセンブリ言語の理論を拡張し、C言語プログラムからの変換が可能となるように、C言語特有の安全でない言語機構にも対応した新しい型付きアセンブリ言語を設計・実装した。また実際に、C言語プログラムを型付きアセンブリ言語へ変換する変換器についてもプロトタイプ実装を行った。この変換器は、Fail-Safe CやVITC、CCuredなどの安全化コンパイラの手法を応用し、安全でないC言語プログラムに対しては型安全性が保証された動的検査コードを挿入することで、型付きアセンブリ言語への変換を実現している。これにより、ほとんどのC言語プログラムの変換が大きな制約なしに可能となった。

　今後は、C言語からの変換後の型付きアセンブリ言語プログラムの実行性能を向上させるために変換手法を改善し、また、変換のための前処理を既存のC言語コンパイラと同程度にまで利便性を高めるなどして、数年後には実用化したい考えだ。

　前田助教のCREST研究プロジェクトでは、ほかにも、オペレーティングシステムなどのシステムソフトウェアの記述に適した型付きアセンブリ言語、特に、SMPやマルチコア環境などの複数のプログラムが同時に実行されるような環境や、ハードウェア割り込みが発生するような環境においても型安全性を保証できる型付きアセンブリ言語の研究、また、C言語で記述されたシステムソフトウェアのモデル検査を、クラスタなどの大規模計算機上で効率的に実行することを試みる研究などを行っており、これらの研究を組み合わせることにより、ディペンダブルなオペレーティングシステムの構築手法の実現を目指している。