豪研究所、カーネルの安全性を数学的に検証する手法を開発

文:Tom Espiner(ZDNet.co.uk) 翻訳校正:湯本牧子、高森郁哉 2009年08月17日 15時14分

  • このエントリーをはてなブックマークに追加

 オーストラリアの民間研究機関Information and Communications Technology Centre of Excellence(NICTA)の研究者らは現地時間8月12日、ミッションクリティカルなシステム向けの中核ソフトウェアが安全であることを検証する方法を発表した。

 研究者らによると、この方法により、飛行機や自動車におけるシステムの安全性とセキュリティを管理するソフトウェアが、エラーを含む大型クラスを持たないことを数学的に検証できるという。

 NICTAは、汎用OSカーネルに対する、マシンチェックによる初のフォーマル検証が完了したと発表した。このカーネルは、「Secure Embedded L4」(seL4)マイクロカーネルと呼ばれる。

 ケンブリッジ大学のコンピュータ研究所で演算論理学の教授を務めるLawrence Paulson氏は、英国時間8月13日にZDNet UKの取材に応じ、このマイクロカーネルの飛躍的進歩は企業各社にトリクルダウン効果をもたらすだろうと述べた。同氏は定理証明支援プログラム「Isabelle」を開発した人物で、NICTAはIsabelleを改変して同団体のカーネルをチェックした。

 「私はソフトウェア業界が完全に混乱していると考えている。コンピュータを使ったことがある人なら、それがどれほど不安定なものかを知っている。これは、安定性を改善する重要な手段になる」(Paulson氏)

 Paulson氏によれば、高品質のコードを厳密にテストするには費用がかかるが、こうした専門用途のテストやOSを開発することは、一般的なソフトウェアの向上という二次的効果をもたらすという。

 Paulson氏は、ドイツの「Verisoft」プロジェクトを例に挙げながら、欧州のチームがコンピュータシステムのフォーマル検証において飛躍的進歩を遂げたと付け加えた。

 フォーマル検証の研究チームを率いるNICTAの主任研究者Gerwin Klein氏は声明の中で、これまでの研究では特定システムの特性を検証することに注力していたと述べた。

 「特定(システム)の特性へのフォーマル検証は比較的小さなカーネルで実施されてきたが、われわれが実行したのは、実世界でこれまで1度も実現しなかった、これほど複雑な高性能ソフトウェアに対する一般的かつ機能的な正当性の検証だ」(Klein氏)

 NICTAは、seL4マイクロカーネルに対して、バッファオーバーフローの脆弱性を悪用する攻撃など、さまざまな攻撃が失敗に終わるはずだと主張した。

 NICTAの研究によって生み出された知的財産は、さらなる開発のため、NICTAからスピンオフした企業Open Kernel Labsに受け渡されることになる。今回の研究には4年を要し、NICTAの研究者12人がニューサウスウェールズ大学と合同で実施した。

この記事は海外CBS Interactive発の記事をシーネットネットワークスジャパン編集部が日本向けに編集したものです。原文へ

ZDNet Japan 記事を毎朝メールでまとめ読み(登録無料)

  • このエントリーをはてなブックマークに追加

この記事を読んだ方に

関連キーワード
開発

関連ホワイトペーパー

連載

CIO
ITアナリストが知る日本企業の「ITの盲点」
シェアリングエコノミーの衝撃
デジタル“失敗学”
コンサルティング現場のカラクリ
Rethink Internet:インターネット再考
インシデントをもたらすヒューマンエラー
トランザクションの今昔物語
エリック松永のデジタルIQ道場
研究現場から見たAI
Fintechの正体
米ZDNet編集長Larryの独り言
大木豊成「仕事で使うアップルのトリセツ」
山本雅史「ハードから読み解くITトレンド放談」
田中克己「展望2020年のIT企業」
松岡功「一言もの申す」
松岡功「今週の明言」
内山悟志「IT部門はどこに向かうのか」
林 雅之「デジタル未来からの手紙」
谷川耕一「エンプラITならこれは知っとけ」
大河原克行「エンプラ徒然」
内製化とユーザー体験の関係
「プロジェクトマネジメント」の解き方
ITは「ひみつ道具」の夢を見る
セキュリティ
エンドポイントセキュリティの4つの「基礎」
企業セキュリティの歩き方
サイバーセキュリティ未来考
ネットワークセキュリティの要諦
セキュリティの論点
スペシャル
エンタープライズAIの隆盛
インシュアテックで変わる保険業界
顧客は勝手に育たない--MAツール導入の心得
「ひとり情シス」の本当のところ
ざっくり解決!SNS担当者お悩み相談室
生産性向上に効くビジネスITツール最前線
ざっくりわかるSNSマーケティング入門
課題解決のためのUI/UX
誰もが開発者になる時代 ~業務システム開発の現場を行く~
「Windows 10」法人導入の手引き
ソフトウェア開発パラダイムの進化
エンタープライズトレンド
10の事情
座談会@ZDNet
Dr.津田のクラウドトップガン対談
Gartner Symposium
IBM World of Watson
de:code
Sapphire Now
VMworld
Microsoft WPC
Microsoft Connect()
HPE Discover
Oracle OpenWorld
Dell Technologies World
AWS re:Invent
AWS Summit
PTC LiveWorx
吉田行男「より賢く活用するためのOSS最新動向」
古賀政純「Dockerがもたらすビジネス変革」
中国ビジネス四方山話
ベトナムでビジネス
日本株展望
企業決算
このサイトでは、利用状況の把握や広告配信などのために、Cookieなどを使用してアクセスデータを取得・利用しています。 これ以降ページを遷移した場合、Cookieなどの設定や使用に同意したことになります。
Cookieなどの設定や使用の詳細、オプトアウトについては詳細をご覧ください。
[ 閉じる ]