「L4マイクロカーネルファミリー」の版間の差分
削除された内容 追加された内容
日本語表現の修正 |
m bot: 解消済み仮リンクロックウェル・コリンズを内部リンクに置き換えます |
||
210行目:
2014年7月29日、{{仮リンク|NICTA|en|NICTA}}と[[ジェネラル・ダイナミクス]]・{{仮リンク|ミッション・システムズ|en|General Dynamics Mission Systems}}は隅から隅まで検証されたseL4をオープンソースでリリースした。カーネルコードと検証コードは[[GPLv2]]で提供され、ほとんどのライブラリとツールは2条項[[BSDライセンス]]で提供されている。研究者のコメントによれば、ソフトウェアの形式的証明のコストはより高い信頼性を提供するにも関わらず従来の「高度な保証」を有するソフトウェアを設計するコストよりも低いとしている。<ref>{{cite journal | last1 = Klein | first1 = Gerwin | last2 = Andronick | first2 = June | last3 = Elphinstone | first3 = Kevin | last4 = Murray | first4 = Toby | last5 = Sewell | first5 = Thomas | last6 = Kolanski | first6 = Rafal | last7 = Heiser | first7 = Gernot | year = 2014 | title = Comprehensive formal verification of an OS microkernel | url = http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf | format = PDF | journal = ACM Transactions on Computer Systems | volume = 32 | issue = | page = 64 | doi = 10.1145/2560537 | deadurl = no | archiveurl = https://web.archive.org/web/20140803122308/http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf | archivedate = 2014-08-03 | df = }}</ref> 具体的には、従来の「高度な保証」を有するソフトウェアでは1行あたりのコストは1000米ドルであるのに対し、開発中のseL4の1行あたりのコストは400米ドルと見積もられた。<ref>{{YouTube|lRndE7rSXiI|seL4 Is Free – What Does This Mean For You?}}</ref>
NICTAは[[アメリカ国防高等研究計画局]](DARPA)の高保証サイバー軍事システム計画（[https://www.darpa.mil/program/high-assurance-cyber-military-systems High-Assurance Cyber Military Systems](HACMS)の下でプロジェクトパートナーの
|title = DARPA selects Rockwell Collins to apply cybersecurity technology to new platforms
|url = https://www.rockwellcollins.com/Data/News/2017-Cal-Yr/GS/FY17GSNR38-HACMS.aspx
| |||