メモリ管理コードの包括的検証のための階層化されたメモリモデル吉野寿宏, 前田俊行, 米澤明憲 (東京大学情報理工学系研究科) 背景  これまでのプログラム検証では、メモリ管理コードはア・プリオリに与えられてきた • たとえば GC に依存していたり、 • 明示的な new, free があってもそれ自体は言語にビルトインであったり • Alias Types, Region-based Memory Management  それに対し、メモリ管理ルーチン自体を検証しようという研究が近年提案されている • TALK [Maeda et al. ’06] • Separation Logic による Topsy ヒープマネージャの正当性証明 [Nicolas et al. ’06] しかし  ユーザのコードにもメモリ管理ルーチン用の理論をそのまま適用することは正しいのだろうか？ • メモリ管理ルーチンとユーザコードに、それぞれ専用のシステムが必要なのは好ましくない • 既存研究ではメモリ管理専用の拡張を行っているものが多いが、そのままユーザプログラムに応用できるか？ • たとえばリンク済みバイナリ全体を検証する場合 • ユーザプログラム側が独自でメモリ管理ルーチンを持っている場合もある • 言語処理系などを相手にする場合には特によくあることそこで本研究では  OS の特権階層にヒントを得て、階層化されたメモリモデルを設計する • メモリ操作を包括的に検証するための理論を構築することを目標 • メモリ管理ルーチンからユーザプログラムまでをモデル化 • プロトタイプの意味論、型システムの設計を行った階層化されたメモリモデル  プログラムは、いくつかのモジュールから構成 • OS カーネル、libc (特にメモリ管理ルーチン)、ユーザプログラムなど  それらのモジュールを「階層」と考え、メモリ割り当て、解放を階層間インタラクションと捉える cf. リングプロテクションとシステムコール階層化されたメモリモデル malloc/free の作る階層メモリ割り当ては、自分の管理しているメモリを下位階層へ分譲することとして解釈できる  解放は逆に、分譲していた領域の回収  OS libc malloc call ユーザプログラム memory return 階層化されたメモリモデル malloc/free の作る階層  この各階層は隔離されている必要 • メモリブロックは各層で固有の意味を持って利用される (上位で利用をトレースする必要はない) • 上位には管理情報などが存在し、下位からはアクセスされたくない管理情報: 下位階層からはアクセス不可能 OS libc ユーザプログラム … int[2] メモリをどう使うかは割り当てられた側の自由 … 割り当てた側は関知しない inet_addr[8] 言語・型システムのプロトタイプの設計  Alias Type[Walker et al. ‘00] をベースに • メモリの明示的管理、型の strong update に対応 • CPS スタイルの関数呼び出し • Constraint の部分を、location と layer に関する記述に拡張することで実現できる • 新しい操作として、export, unexport を導入 • export がメモリブロックを他レイヤに与え、unexport で奪う言語・型システムのプロトタイプの設計構文定義 Alias Type の Heap Constraint にレイヤ情報追加関数にも実行レイヤ情報付加どのレイヤから割り当てられたか(origin)、また現在の所有者 (ownership)を識別言語・型システムのプロトタイプの設計静的意味論（抜粋）逆操作所有権の確認逆操作言語・型システムのプロトタイプの設計静的意味論（抜粋）読み込みは誰でも可能所有者のみが書き込めるこのモデルの性質 (1/2)  各階層ごとのメモリ割り当てについては、 containment が成り立つ • 上位階層の持つメモリ ⊇ 下位階層の持つメモリ • 同一のブロックについては委譲関係がリスト(origin 情報をたどれる)になっている • 現在の定式化では委譲関係を覚えておく必要がある • また同一ブロックの所有者(ownership = +)は常にただひとつの階層のみ  new-free の対応、export-unexport の対応がつけられるこのモデルの性質 (2/2)  各階層ごとに、同一メモリブロックに対して異なるビューが持てる • ポインタを、上位から見ると int に見えたりする • 階層間の隔離の緩和を定式化している • Strong update 時には、他のレイヤの invariant を壊さないように注意 • 現在の定式化では、int 型が subtyping relation における top 型に相当 • 現在他のレイヤでは int になっていることを制約として強制 Future Work (1/2)  レイヤに対して順序構造の導入 • 関数に呼び出し特権レベルなどを記述 • 順序構造に関する制約記述ができるように • モジュール化 • existential type の応用でできる  応用について考える • たとえば conservative GC の管理ルーチンの検証に応用することができると考えている • GC Safety を証明するには、reachability の概念が必要になるので、そのための拡張が必要 • その他に記述できるような性質はないか？ Future Work (2/2)  上位に int 以外でのビューを提供 • どういった形の invariant が書けるか？  Recursive Type, Union Type などの導入 • coercion においてレイヤ情報をどうやって保持するか  Dependent Type の導入 • split, concat による領域分割・結合 • より現実的なメモリ管理コードをチェックできるようになる Related Work  Region-based Memory Management [Tofte, Talpin ’97] • メモリを Region という単位に分けて管理するというアイデアを提唱  Capability Calculus [Crary et al. ‘99] • 上記の研究を拡張し、Capability という概念を用いることでメモリ管理を明示的に行うコードに型をつける • Capability ≒ 領域へのアクセス権限 • メモリ操作には capability を持っている必要 • そのため関数引数などに明示的に引き渡される • 複数のビューを持ったりはできない