マイクロカーネル
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/10/12 01:55 UTC 版)
セキュリティ
マイクロカーネルはセキュリティ面で優れているとよく言われてきた[17][18]。セキュリティの観点では、マイクロカーネルの極小原則は、全てのコードについて必要とされる機能を提供するのに必要な権限だけを持つべきであるという最小権限の原則の直接的帰結である。極小性は、システムのトラステッド・コンピューティング・ベース (TCB) を極小に保つべきであることを要求する。カーネル（ハードウェアの特権モードで実行されるコード）は常にTCBの一部であり、セキュリティ指向設計ではそれを極小化するのが自然である。
結果として、マイクロカーネル設計は高度なセキュリティを要求される用途で採用されており、例えばKeyKOS、EROS、軍用システムなどがある。実際、コモンクライテリア (CC) の最高保証レベル（評価保証レベル (EAL) 7）では、対象の評価が「単純」であること、複雑なシステムの真の信頼性を確立するのに実際的不可能性を確認できることを明示的に要求している。
第三世代
近年のマイクロカーネル研究開発は、カーネルAPIの形式仕様とそのAPIのセキュリティ属性の形式的証明に集中している。第一の例として、EROSでの隔離機構の数学的証明があり、EROS API を単純化したモデルに基づいている[19]。より最近の例として、L4のバージョンの一種である seL4 のプロテクションモデルについて自動検証された包括的な証明がなされている[20]。
それにより「第三世代マイクロカーネル」と呼ばれるものが生まれている[21]。これはセキュリティ指向のAPI、ケイパビリティによるリソースアクセス制御、最重要概念としての仮想化、カーネル資源管理への革新的アプローチ[22]、形式的分析に適した設計、などを特徴としつつ、性能向上を目標としたものである。例として、Coyotos、seL4、Nova[23][24]、Fiasco.OC[23][25]などがある。
seL4の場合、実装についての完全な形式的検証がなされており[21]、形式仕様と実装が一致していることが数学的に証明されている。それにより、APIについて証明された属性が実際のカーネルでも保持されていることが保証でき、CC EAL7 をも越える保証の程度となっている。
ナノカーネル
ナノカーネル (nanokernel) またはピコカーネル (picokernel) という用語は歴史的には次のような意味で使われてきた。
- カーネルコードの量、すなわちハードウェアの特権モードで実行されるコードの量が極めて小さいカーネル。カーネルが極めて小さいことを強調する際に「ピコカーネル」という呼称も使われた。「ナノカーネル」という用語を生み出したのは Jonathan S. Shapiro で、The KeyKOS NanoKernel Architecture (1992) という論文で初めて使っている。それはMachへの冷笑的反応であった。彼はMachについて、本質的に非構造的であり、モノリシックであるのにマイクロカーネルと主張しているだけで、置き換えようとしているものより性能が悪いと評した。その用語が他でも使われ、さらにピコカーネルという呼称が生まれた背景には、従来のマイクロカーネルが「カーネルが小さい」という点から大きく外れていったことを示唆している。その後、ナノカーネルとピコカーネルはマイクロカーネルと同じ意味で使われるようになった。
- OSの下にある仮想化層。より正確には「ハイパーバイザ」と呼ばれる。
- カーネルの最下層部を形成している ハードウェア抽象化層。例えば Adeos があり、通常のOSにリアルタイム機能を提供するのに使われる。
また、小さくないカーネルをナノカーネルと呼ぶ用例も少なくとも1つあり、その場合はクロック間隔としてナノ秒単位までサポートしているカーネルを指す[26]。
- ^ “Porting UNIX/Linux Applications to Mac OS X”. Apple. 2011年4月26日閲覧。
- ^ a b c Liedtke, Jochen (September 1996). “Towards Real Microkernels”. Communications of the ACM 39 (9): 70–77. doi:10.1145/234215.234473.
- ^ Heiser, Gernot; Uhlig, Volkmar and LeVasseur, Joshua (January 2006). “Are Virtual-Machine Monitors Microkernels Done Right?”. ACM SIGOPS Operating Systems Review (ACM) 40 (1): 95–99. doi:10.1145/1113361.1113363.
- ^ Liedtke, Jochen (December 1993). "Improving IPC by kernel design". 14th ACM Symposium on Operating System Principles. Asheville, NC, USA. pp. 175–88.
- ^ QNX High Availability Toolkit
- ^ Wong, William (2007-04-27). “I/O, I/O, It's Off to Virtual Work We Go”. Electronic Design 2009年6月8日閲覧。.
- ^ Alexander, Michael T. (1971). “Organization and Features of the Michigan Terminal System”. Proceedings of the November 16–18, 1971, fall joint computer conference 40: 589–591. doi:10.1145/1478873.1478951.
- ^ Lions, John (1977-08-01). Lions' Commentary on UNIX 6th Edition, with Source Code. Peer-To-Peer Communications. ISBN 978-1-57398-013-5
- ^ a b Liedtke, Jochen (December 1995). "On µ-Kernel Construction". 15th ACM symposium on Operating Systems Principles. pp. 237–250. doi:10.1145/224056.224075。
- ^ Chen, Bradley; Bershad, Brian (December 1993). "The Impact of Operating System Structure on Memory System Performance". 14th ACM Symposium on Operating System Principles. Asheville, NC, USA. pp. 120–33. doi:10.1145/168619.168629。
- ^ Liedtke, Jochen; Elphinstone, Kevin; Schönberg, Sebastian; Härtig, Hermann; Heiser, Gernot; Islam, Nayeem; Jaeger, Trent (May 1997). "Achieved IPC performance (still the foundation for extensibility)". 6th Workshop on Hot Topics in Operating Systems. Cape Cod, MA, USA: IEEE. pp. 28–31.
- ^ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (April 2005). "Itanium—a system implementor's tale". USENIX Annual Technical Conference. Annaheim, CA, USA. pp. 264–278.
- ^ van Schaik, Carl; Heiser, Gernot (January 2007). "High-performance microkernels and virtualisation on ARM and segmented architectures" (PDF). 1st International Workshop on Microkernels for Embedded Systems. Sydney, Australia: NICTA. pp. 11–21. 2007年4月1日閲覧。
- ^ Härtig, Hermann; Hohmuth, Michael; Liedtke, Jochen; Schönberg, Sebastian (October 1997). “The performance of µ-kernel-based systems”. Proceedings of the sixteenth ACM symposium on Operating systems principles: 66–77. doi:10.1145/268998.266660. ISBN 0-89791-916-5.
- ^ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen; Elphinstone, Kevin J.; Uhlig, Volkmar; Tidswell, Jonathon E.; Deller, Luke; Reuther, Lars (2000). "The Sawmill multiserver approach". 9th ACM SIGOPS European Worshop. Kolding, Denmark. pp. 109–114.
- ^ Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot (September 2005). “User-level device drivers: achieved performance”. Journal of Computer Science and Technology 20 (5): 654–664. doi:10.1007/s11390-005-0654-4.
- ^ Tanenbaum, Andrew S., Tanenbaum-Torvalds debate, part II
- ^ Tanenbaum, A., Herder, J. and Bos, H. (May 2006).
- ^ Shapiro, Jonathan S.; Weber, Samuel. "Verifying the EROS Confinement Mechanism". IEEE Conference on Security and Privacy. 2016年3月3日時点のオリジナルよりアーカイブ。
- ^ Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin (2007). Verified Protection Model of the seL4 Microkernel. submitted for publication
- ^ a b Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA.
- ^ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (April 2008). "Kernel design for isolation and assurance of physical memory". 1st Workshop on Isolation and Integration in Embedded Systems. Glasgow, UK. doi:10.1145/1435458。
- ^ a b “TUD Home: Operating Systems: Research: Microkernel & Hypervisor”. Faculty of Computer Science. Technische Universität Dresden (2010年8月12日). 2011年11月5日閲覧。
- ^ Steinberg, Udo; Kauer, Bernhard (April 2010). "NOVA: A Microhypervisor-Based Secure Virtualization Architecture". Eurosys 2010. Paris, France. pp. 209–222.
- ^ Lackorzynski, Adam; Warg, Alexander (March 2009). "Taming Subsystems - Capabilities as Universal Resource Access Control in L4". IIES'09: Second Workshop on Isolation and Integration in Embedded Systems. Nuremberg, Germany.
- ^ http://www.eecis.udel.edu/~mills/database/papers/nano/nano2.pdf
「マイクロカーネル」の続きの解説一覧
- マイクロカーネルのページへのリンク
