Ironclad – リアルタイム対応のUnix系OSカーネル

 (ironclad-os.org)
1 ポイント 投稿者 GN⁺ 2025-11-10 | 1件のコメント | WhatsAppで共有
  • アイアンクラッド（Ironclad） は、一般用途および組み込み環境向けの 形式検証ベースのリアルタイム対応Unix系カーネル
    • 形式検証（Formal verification） : ランタイムエラー不在（AoRTE, Absence of Runtime Errors） とコンポーネントの正確性を保証するために、カーネルコードが経る一連のプロセスと検査
  • SPARKとAda で記述されており、100%自由ソフトウェア で構成
  • POSIX互換インターフェース、プリエンプティブマルチタスク、強制アクセス制御（MAC）、ハードリアルタイムスケジューリング をサポート
  • GPLv3ライセンス で配布され、ファームウェアブロブなしで完全な オープンソース構成 を維持
  • 複数のプラットフォームへ移植可能で、Gloire などのディストリビューションを通じてエコシステムを拡大中

Ironcladオペレーティングシステムカーネル概要

  • Ironcladは、形式検証（formal verification） を部分的に適用した リアルタイム対応のUNIX系カーネル
    • 汎用システムおよび組み込みシステムの両方を対象に設計
    • 形式検証（Formal verification）: ランタイムエラー不在（AoRTE, Absence of Runtime Errors） とコンポーネントの正確性を保証するために、カーネルコードが経る一連のプロセスと検査
    • このために、Ada のサブセットである ** SPARK** を利用
    • 全コードが 自由ソフトウェア で構成
  • カーネルは POSIX互換インターフェース を提供し、プリエンプティブマルチタスク と 強制アクセス制御（MAC）、ハードリアルタイムスケジューリング をサポート
    • 従来のUNIX環境に近い開発体験を提供
    • リアルタイム制御が必要なシステムに適した構造

自由ソフトウェアとしての特徴

  • Ironcladは GPLv3ライセンス の下で完全なオープンソースとして配布
    • カーネルに ファームウェアブロブ（firmware blob） は含まれない
    • スタックのすべての構成要素がオープンソースの形で提供される

形式検証（Formal Verification）

  • SPARK言語の形式検証機能 を活用して、主要コンポーネントのエラー不在と正確性を保証
  • SPARKはAdaコードに 事前条件（Pre）、事後条件（Post）、依存関係（Depends） などを記述し、コードの論理的一貫性を数学的に検証する
    • 検証対象には 暗号化モジュール、MACシステム、ユーザーインターフェース関連機能 などが含まれる

移植性と開発環境

  • Ironcladは複数の プラットフォームとボード にポーティングされており、追加移植が容易になるよう設計
    • GNUツールチェーン のみに依存し、容易な クロスコンパイル が可能
    • POSIX互換性 により、ソフトウェアの移植と開発が容易

ディストリビューションとエコシステム

  • Ironcladプロジェクトは、さまざまなアーキテクチャとボード向けの ディストリビューション を提供
    • 代表的な自由オープンソースディストリビューションは Gloire
    • ダウンロード可能な tarball形式の配布イメージ を提供

プロジェクト支援と継続性

  • Ironcladは 利用、研究、改変が自由なプロジェクト として維持されている
    • プロジェクト運営は 寄付と助成金 に依存
    • すべての貢献がプロジェクトの拡大と発展に直接的な影響を与える

関連記事

1件のコメント

 
GN⁺ 2025-11-10
Hacker Newsのコメント

  • 興味深いプロジェクトだ。最悪実行時間(WCET) の形式的検証の限界が気になる。
    seL4 や atmosphere のような他の検証済みカーネルもあるし、genode のように POSIX 互換レイヤーを積むこともできる。
    QNX や VxWorks のように完全互換で成熟したカーネルもあるので、完全な検証が大きな付加価値にならない可能性もある。
    ただし WCET + 形式検証 + POSIX 互換性をすべて備えた例は、ほとんど見たことがない。
    現段階では、ドキュメントにあるリアルタイム用途にすぐ使えるほど成熟度が高いとは言いがたい。

    • どの政府であれ OS に RCE を得られる世界だ。だからこそプロセス分離の形式的検証が本当に重要になる。
      seL4 は Linux よりずっと高速だが、これは遅そうに見える。POSIX には本質的な欠陥があり、MAC は複雑すぎて実務では使いにくい。
    • まだ stone レベルだが、今後 公式認証 も取得できそうだ。形式的に検証された OS は、セキュリティ向上における大きな前進だ。

  • Ada は Wirth 系言語(Pascal 系)に属する。これまで Wirth 系言語で書かれた Unix ライクなカーネルとしては TUNIS しか知らなかった。
    TUNIS は Concurrent Euclid で実装されていた。

    • 90年代にはワシントン大学で開発された SPIN もあった。Modula-3 で書かれたマイクロカーネルベースのシステムで、Digital UNIX のシステムコールインターフェースをサポートしていた。
      また 80年代の INRIA の Sol は Pascal 方言で実装され、Unix 互換環境を提供しており、その後 Chorus へとつながった。

  • Ironclad という名前の NDA 関連企業もある。商標権の問題には注意すべきだ。
    それでもこうした試みは本当に歓迎したい。だが現実には、セキュリティの最も弱い輪はファームウェア層だ。
    私の夢は、Framework Computer のようなハードウェアが 検証済み EFI ファームウェア と、各コンポーネントごとに監査されたファームウェアを備えることだ。

    • Ironclad は Common Lisp の主要な 暗号ライブラリ の名前でもある (ironclad GitHub)。
    • MNT Research も見てみる価値がある。修理可能なノートPCを作っており、ハードウェアとソフトウェアの両方をオープンソースで公開している (mnt.re)。
    • ファームウェアの検証には別個のカーネルが必要だ。こうした部分は今や 規制レベル で管理されるべきだ。
    • 商標は同じ名前でも 異なる業界分野 なら問題ない。たとえば Apple Computer と Beatles の Apple Music の事例のように (xkcd 386)。

  • 新しい OS を作るというのは本当に野心的なことだ。最近 Radiant Computer も投稿されていたが、ほかにも似たような面白いプロジェクトがあるのか気になる。

    • Asterinas (Linux 互換カーネル) と Redox OS が有望だ。
    • SerenityOS もある。
    • 古い選択肢ではあるが Haiku OS もいまだに興味深い。
    • 私にも OS のアイデアがある。ハードウェア、カーネル、ユーザープログラムまで含む複数の構成要素を構想中だ。
    • ReactOS も発展を続けている。完全に新しい OS ではないが、それでも新しいと思う。

  • いつか完全に 形式検証されたカーネル が一般化してほしい。
    Linux 全体を検証するのは不可能だろうが、seL4 はスマートフォンのような市場でチャンスをつかめるかもしれない。

  • 彼らの 検証ロードマップ を見る限り、これを「形式検証」と呼ぶのは大げさだ。
    カーネルの中核的な性質に対する証明がなく、seL4 や Tock のようなカーネルの水準には達していない。

  • CuBit は SPARK/Ada で書かれた別の OS だ。
    ソースは GitHub で見られる。

  • 一般ユーザーの立場では、カーネルだけでは役に立たない。
    Ironclad カーネルを使う OS の例としては Gloire がある。

  • MAC 関連のドキュメントはよく整理されている (Mandatory Access Control)。

  • SPARK の「価格についてお問い合わせください」という文言を見ると、これは 「自由ソフトウェア」 というより別の意味での free のようだ。

    • 上の GitHub リンクの大半も商用サポートは有料だ。価格問い合わせは一般的な手続きなので、特に不自然ではない。
    • 結局のところ 開発者も生計を立てる必要がある、それは当然のことだ。