ニュースは最近それを破った に含める提案がなされました。 のカーネル Linux 5.20 (または、ブランチの番号が 6.0 になるかもしれません。それはすべて、カーネル 5.19 リリースに関する彼のコメントによる Linus Torvalds の決定に依存します)。
行われた提案は約です RV メカニズムを実装した一連のパッチ (ランタイム検証)、これは、障害がないことを保証する信頼性の高いシステムで正しく動作することを検証する手段です。
検証 トレースポイントにハンドラーをアタッチすることにより、実行時に行われます システムの予想される動作を決定するオートマトンの事前定義された決定論的参照モデルに対して、実行の実際の進行状況をチェックします。
Linux 開発者、 ダニエル・ブリスト・デ・オリベイラは次のように述べています。
ここ数年、私はランタイム検証を使用して Linux カーネルの動作を検証する可能性を探ってきました。
ランタイム検証 (RV) は、従来の徹底的な検証手法 (モデル チェックや定理証明など) を複雑なシステムへのより実践的なアプローチで補完する、軽量 (かつ厳密) な方法です。 システムの詳細なモデル (命令レベルの再実装など) に依存する代わりに、VR は、システムの実際の実行トレースを分析し、システムの動作の正式な仕様と比較することによって機能します。
VR での決定論的オートマトンの使用は、十分に確立されたアプローチです。 Linux カーネルの特定のケースでは、この記事で Linux カーネルの複雑な動作をモデル化する方法を学ぶことができます。
デ・オリベイラ、ダニエル・ブリスト。 トマソ、クチノッタ。 デ・オリベイラ、ロムロ・シルバ。 *Linux カーネルの効率的なフォーマル検証。* In: International Conference on Software Engineering and Form Methods。 スプリンガー、チャム、2019年。 315-332。
そして、ここでこのアプローチがどれほど効率的か:
デ・オリベイラ、ダニエル・B。 De Oliveira、Romulo S.; クチノッタ、トマソ。 *PREEMPT_RT Linux カーネルのスレッド同期モデル。* Journal of Systems Architecture、2020 年、107: 101729。
TLDR: 複雑な動作は、(本番システムの場合でも) 許容可能なオーバーヘッドで、モジュール式にモデル化できます。
と言われています トラック ポイント情報は、モデルをある状態から別の状態に移動します、新しい状態がモデル パラメーターと一致しない場合は、警告が生成されるか、カーネルが "パニック" 状態になります (信頼性の高いシステムがそのような状況を検出して対応すると仮定します)。
オートマトンのモデル ある状態から別の状態への遷移を定義し、「ドット」形式にエクスポートします (graphviz)。その後、dot2c ユーティリティを使用して C 表現に変換されます。C 表現は、偏差を追跡するカーネル モジュールの形式で読み込まれます。 事前定義されたモデルからの実行。
実行時にモデルをチェックすることは、より軽量で簡単な方法として位置付けられています ミッションクリティカルなシステムでの実行の正確性を検証するために実装します。これは、モデルの検証や、コードが形式言語で指定された仕様に準拠していることの数学的証明など、信頼性を検証する従来の方法を補完します。
追跡サブシステムのメンテナーである Steven Rostedt は、次のようにまとめました。
» これは、このプル リクエストの最大の変更点です。 セキュリティ クリティカルなシステムで Linux を実行するために必要なランタイム検証を導入します。 これにより、決定論的オートマトン モデルをカーネルに挿入してトレースポイントにアタッチできます。これらのトレースポイントに関する情報は、モデルをある状態から別の状態に移動させます。
前述の RV の利点の中には、モデリング言語でシステム全体を個別に実装することなく厳密な検証を提供できることと、重要なシステムの障害の伝播をブロックするなど、予期しないイベントに柔軟に対応できることが挙げられます。
最後に、あなたがそれについてもっと知ることができることに興味があるなら、あなたはの詳細を調べることができます 次のリンク。