「L4マイクロカーネルファミリー」の版間の差分

m
bot: 解消済み仮リンクロックウェル・コリンズを内部リンクに置き換えます
(日本語表現の修正)
m (bot: 解消済み仮リンクロックウェル・コリンズを内部リンクに置き換えます)
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)の下でプロジェクトパートナーの{{仮リンク|[[ロックウェル・コリンズ|en|Rockwell Collins}}]]社、[http://galois.com ガロア社]、[[ミネソタ大学]]、[[ボーイング社]]と共同でseL4ベースの[http://ts.data61.csiro.au/projects/TS/SMACCM/ 高保証ドローン]を保証ツールとソフトウェアと共に開発した。これはボーイングで開発中の操縦も可能な自律型無人ヘリコプター[[ボーイング AH-6]]への技術移転も計画されていた。最終的なHACMS技術のデモンストレーションは2017年4月、バージニア州スターリングで行われた。<ref name=hacms_demo>{{cite press release
|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
447,113

回編集