「L4マイクロカーネルファミリー」の版間の差分
削除された内容 追加された内容
→商業的展開: 英語版へのリンクの修正 |
en:L4 microkernel family 01:20, 27 May 2018の翻訳をベースにHigh assurance: seL4の内容を一部追加 |
||
110行目:
ほとんどはクアルコムのワイヤレスモデムチップである。他のものには車載インフォティメントシステムが含まれる。
[[Apple A7|A7]]以降のAシリーズ{{仮リンク|Appleモバイルアプリケーションプロセッサ|en|Apple mobile application processors}}に含まれるSecure EnclaveコプロセッサではNICTAが2006年に開発したL4-embeddedカーネルベースのL4オペレーティングシステムが動作している。これは現在、全てのiOSデバイスでL4が出荷されていることを意味し、2015年の総出荷量はおよそ3億1000万台とされる。
==高度な保証：seL4==
2006年にNICTAのグループは'''seL4'''と呼ばれる第3世代マイクロカーネルの設計を開始した。これは[[コモンクライテリア]]（Common Criteria：略称CC [[ISO]]/[[IEC]] 15408規格）を満たす、あるいはそれ以上のセキュリティ要件を満たすために高い安全性と信頼性が得られるような基本方針で設計された。最初からカーネルの形式的証明を目指して開発を行った。性能と検証の時に相反する要求を満たすために、チームは[[Haskell]]で書かれた実行可能な定義からソフトウェアによる処理を行いその結果を用る方法をとった。<ref name=Derrin_EKCC_06>{{cite conference
| first = Philip
| last = Derrin
| author2 = Elphinstone, Kevin |author3=Klein, Gerwin |author4=Cock |author5=David |author6= Chakravarty, Manuel M. T.
| title = Running the manual: an approach to high-assurance microkernel development
| booktitle = ACM SIGPLAN Haskell Workshop
|date=September 2006
| pages = 60–71
| location = [[Portland, Oregon]]
| url = http://portal.acm.org/citation.cfm?id=1159842.1159850&coll=portal&dl=ACM&type=series&idx=1159842&part=Proceedings&WantType=Proceedings&title=Haskell&CFID=18785943&CFTOKEN=93152956
}}</ref>
seL4ではオブジェクトのアクセス権についての形式的推論を可能にするために [[Capability-based security|capability-basedアクセス制御]] を用いている。
機能の正しさの形式的証明は2009年に完了した。<ref Name="Klein_EHACDEEKNSTW_09">
{{ cite conference
|first1 = Gerwin
|last1 = Klein
|first2 = Kevin
|last2 = Elphinstone
|first3 = Gernot
|last3 = Heiser
|author3-link = Gernot Heiser
|first4 = June
|last4 = Andronick
|first5 = David
|last5 = Cock
|first6 = Philip
|last6 = Derrin
|first7 = Dhammika
|last7 = Elkaduwe
|first8 = Kai
|last8 = Engelhardt
|first9 = Rafal
|last9 = Kolanski
|first10 = Michael
|last10 = Norrish
|first11 = Thomas
|last11 = Sewell
|first12 = Harvey
|last12 = Tuch
|first13 = Simon
|last13 = Winwood
|title = seL4: Formal verification of an OS kernel
|booktitle = 22nd ACM Symposium on Operating System Principles
|pages =
|date = October 2009
|location = Big Sky, MT, USA
|doi =
|url = http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
|deadurl = no
|archiveurl = http://archive.wikiwix.com/cache/20110715225243/http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
|archivedate = 2011-07-15
|df =
}}</ref>
この証明はカーネルの実装がその定義に対して正しいことを示し、従ってデッドロック、ライブロック（あるプロセスがbusy状態のまま実行権を放さなくなってしまう状態を指す）、バッファオーバーフロー、数値演算の例外、初期化していない変数の使用などの実装バグの無いことを意味する。seL4は汎用のOSカーネルとしては初めて正しいと確認されたという主張がなされている。<ref Name="Klein_EHACDEEKNSTW_09" />
== 脚注 ==
| |||