Microsoft，タイプセーフなオペレーティングシステム Verve を発表

作者 James Vastbinder , 翻訳者 吉田 英人 投稿日 2010年12月12日

セクション

運用/インフラ,

デベロップメント

トピック

.NET ,

プログラミング ,

Architecture ,

OS ,

Singularity

共有 |

原文(投稿日：2010/12/08 )へのリンク

Microsoft Research は今週始めに公表した論文 に合わせて，Singularity プロジェクトから派生した Verve オペレーティングシステムのリリース を発表した。TAL (Typed Assembly Language，型付きアセンブリ言語) と Hoare 論理の採用を前提に最高レベルのセキュリティと安全性を実現するこのオペレーティングシステムは，核 (nucleus) とカーネル，ひとつないし複数のアプリケーションから構成される。

Verve は C# で記述されていて，自動的に TAL にコンパイルされた上で，型安全性を検証する第２のチェックが実行される。ただし Nucleus は直接，手作業でアサーションを施したアセンブリ言語で記述されている。アセンブリ言語の仕様検証には Boogie が採用され，TAL コードとハードウェアに対する安全なインタラクション実施を保証する。

Verve の成果

• アセンブリ言語命令のレベルで型安全性が機械的に検証される，初のオペレーティングシステムである。処理は起動後に実行され，静的な検証が行われる。
• 市販のハードウェア上で動作し，クラスや仮想メソッド，配列，プリエンプティブなスレッドなどの標準的な言語機能をサポートする。
• オブジェクト，メソッドテーブル，配列に Bartok コンパイラのネイティブレイアウトを使用して，高い効率性を実現する。
• 自動化技術，TAL，および自動定理証明を，オペレーティングシステムやランタイムの複雑かつ低レベルなコードの安全性検証手段として実証する。
• 自動定理証明によって検証された少量のコードによる，不定量の TAL コードのサポート可能性を実証する。

検証可能な型安全性を持つコードでは，メモリアクセスはオブジェクト参照と，それに関連するフィールドやプロパティなどの操作に限定される。メモリアクセス手段を明確に定義することにより，ランタイム – この場合はカーネル – が，アクセスすべきでない場所のメモリを操作してしないことが検証可能になる。そもそも型安全性とは，プログラムがオブジェクトに対して，有効でない操作を実行できないことを意味するものだ。Java や C# など現在のプログラム言語において，型安全性はもっとも本質的なセキュリティ要素を提供する。これをオペレーティングシステムのレベルにまで拡張した結果が効率性であり，さらに転じてパフォーマンスとなるのだ。

Verve の制限

• 例外処理など，多くの C# 機能が欠如している。
• 安全でないコードが含まれているため，標準 .NET クラスライブラリがサポートされない。
• コードの動的ロードが未実装である。
• シングルプロセッサ上でのみ動作する。
• Singularity SIPS や Java Isolates，C# AppDomains に相当する，包括的な分離機構を持たない。
• Verve が使用する検証済ガベージコレクタは Stop the World 形式であり，コレクション実行中は割り込みが無効になる。

このように Verve にはいくつかの制限があるが，開発者たちが重要なハードルと認識しているのはマルチプロセッサのサポートだけである。現在の形の根本的変更を要する可能性があるためだ。