ジョン・ラッシュビー
詳細情報
- 代表的業績
- 分離カーネル、PVS
- 所属
- SRI International
1981年に分離カーネルを提唱したイギリスの計算機科学者。コンピュータを安全に共有する最善の方法は、複数台のふりをさせることだという発想である。
1981年のSOSP論文「Design and Verification of Secure Systems」は、問題の立て方を逆転させた。OS全体を検証するのではなく、小さなカーネルがパーティション同士を隔離することだけを行う。各パーティションは、明示的に許可された通信路を除いて独立したマシンのように振る舞う。こうすれば、証明すべき部分は実際に証明できる程度に小さくなる。
この考え方はMILSアーキテクチャ、航空電子機器、現代のハイパーバイザーやマイクロカーネルに生きている。SRI Internationalでは、1992年のPVS証明支援系の開発にも関わった。PVSは飛行制御アルゴリズムから暗号プロトコルまで、さまざまなものの検証に使われている。