Loading article…
デバイス ドライバーは、ソフトウェアまたは高レベルのコンピュータ プログラムがハードウェアデバイスと対話できるようにするプログラムです。これらのソフトウェア コンポーネントは、デバイスとオペレーティング システム間のリンクとして機能し、各システムと通信してコマンドを実行します。デバイス ドライバーは、上位のソフトウェアに抽象化レイヤーを提供し、オペレーティング システム カーネルと下位のデバイス間の通信を仲介します。
通常、オペレーティング システムには共通デバイス ドライバーのサポートが付属しており、通常、ハードウェア ベンダーはほとんどのプラットフォーム向けに自社のハードウェア デバイス用のデバイス ドライバーを提供しています。ハードウェア デバイスの急速な拡張と複雑なソフトウェア コンポーネントにより、デバイス ドライバーの開発プロセスは煩雑で複雑になっています。ドライバーのサイズと機能が増加し始めると、デバイス ドライバーはシステムの信頼性を定義する重要な要素になりました。これにより、デバイス ドライバーの自動合成と検証へのインセンティブが生まれました。この記事では、デバイス ドライバーの合成と検証のいくつかのアプローチについて説明します。
自動ドライバー合成と検証の動機
デバイス ドライバーは、ほとんどのシステムで主要な障害コンポーネントです。Berkeley Open Infrastructure for Network Computing (BOINC) プロジェクトでは、OS クラッシュの主な原因は、デバイス ドライバー コードの不備であることがわかっています。[ 1] Windows XPでは、報告された障害の 85% がドライバーによるものです。Linuxカーネル 2.4.1 では、デバイス ドライバー コードがコード サイズの約 70% を占めています。[2]ドライバーの障害は、カーネル モードで実行されているシステム全体をクラッシュさせる可能性があります。これらの調査結果から、デバイス ドライバーを検証するためのさまざまな方法論と手法が生まれました。代替案は、デバイス ドライバーを堅牢に合成できる手法を開発することでした。開発プロセスでの人間の介入を減らし、デバイスとオペレーティング システムを適切に指定することで、より信頼性の高いドライバーを実現できます。
ドライバー合成のもう 1 つの動機は、オペレーティング システムの種類とデバイスの組み合わせが多種多様であることです。これらのそれぞれに独自の入出力制御と仕様があるため、各オペレーティング システムでハードウェア デバイスをサポートするのは困難です。そのため、オペレーティング システムでデバイスを使用するには、対応するデバイス ドライバーの組み合わせが必要です。ハードウェア ベンダーは通常、Windows、Linux、Mac OS 用のドライバーを提供していますが、開発や移植のコストが高く、技術サポートが難しいため、すべてのプラットフォームでドライバーを提供することはできません。自動化された合成技術は、ベンダーがあらゆるオペレーティング システムであらゆるデバイスをサポートするドライバーを提供するのに役立ちます。
デバイスドライバの検証
デバイス ドライバーのテストを制限する課題が 2 つあります。
- ドライバーとカーネル間の相互作用に障害がある場合、正確な操作や時間を特定するのは非常に困難です。システムが矛盾した状態になり、クラッシュが長い時間後に報告され、クラッシュの実際の原因が不明瞭になる可能性があります。
- 通常の状況では正常に動作するドライバーでも、まれに例外的なケースでは誤動作を起こす可能性があり、従来のテスト手法ではドライバーの特殊なケースの動作を検出するのに役立たない場合があります。
デバイス ドライバーの検証の波は、2000 年という早い時期に Microsoft のSLAM プロジェクトを通じて始まりました。このプロジェクトのきっかけは、1 日に報告される 50 万件のクラッシュが 1 つのビデオ ドライバーによって引き起こされていることが判明し、複雑なデバイス ドライバーの使用に伴う大きな脆弱性に対する懸念が高まったことでした。詳細については、Bill Gates のスピーチをご覧ください。それ以来、バグの検出と分離のために、多数の静的およびランタイム手法が提案されてきました。
静的解析
静的分析とは、プログラムを分析して、指定された安全性に不可欠なプロパティに準拠しているかどうかを確認することです。たとえば、システム ソフトウェアは、「カーネル データ構造に書き込む前にユーザー権限を確認する」、「確認せずに NULL ポインターを参照しない」、「バッファー サイズのオーバーフローを禁止する」などのルールに準拠する必要があります。このようなチェックは、チェック対象のコードを実際に実行しなくても実行できます。従来のテスト プロセス (動的実行) を使用するには、これらのパスを実行してシステムをエラー状態にするための多くのテスト ケースを作成する必要があります。このプロセスには長い時間と労力がかかる可能性があり、実用的なソリューションではありません。理論的には手動検査も可能な別のアプローチですが、これは何百万行ものコードが関係する最新のシステムでは非現実的であり、ロジックが複雑すぎて人間が分析することはできません。
コンパイラテクニック
ソース コードに簡単にマッピングできるルールは、コンパイラを使用してチェックできます。ルール違反は、ソース操作が意味をなさないかどうかをチェックすることで検出できます。たとえば、「割り込みを無効にした後に有効にする」などのルールは、関数呼び出しの順序を調べることでチェックできます。ただし、ソース コードの型システムがセマンティクスでルールを指定できない場合、コンパイラはその種類のエラーをキャッチできません。多くの型セーフ言語では、安全でない型キャストによって生じるメモリ セーフティ違反をコンパイラで検出できます。
もう一つのアプローチは、メタレベルコンパイル（MC）を使用することです。[3]この目的のために構築されたメタコンパイラは、軽量でシステム固有のチェッカーとオプティマイザーを使用してコンパイラを拡張する場合があります。これらの拡張機能は、システム実装者が高級言語で記述し、厳密な静的分析を行うためにコンパイラに動的にリンクする必要があります。
ソフトウェアモデル検査
ソフトウェアモデル検査は、プログラムのアルゴリズム分析を行い、その実行の特性を証明することです。[4]これにより、与えられた正しい仕様に関するプログラムの動作についての推論が自動化されます。モデル検査とシンボリック実行は、デバイスドライバーの安全性に不可欠な特性を検証するために使用されます。モデルチェッカーへの入力は、プログラムと一時的な安全性特性です。出力は、プログラムが正しいことの証明、または特定の実行パスの形で反例によって仕様違反が存在することのデモンストレーションです。
Microsoft のツール SDV (Static Driver Verifier) [5]は、Windows デバイス ドライバーの静的解析を使用します。バックエンド解析エンジンSLAM は、コンパイル時の静的検証にモデル チェックとシンボリック実行を使用します。各 API のドライバーが遵守すべきルールは、C のような言語 SLIC (インターフェイス チェック用仕様言語) で指定されます。解析エンジンは、API 使用ルールの違反につながる可能性のあるすべてのパスを検出し、ドライバー ソース コードを通じてソース レベルのエラー パスとして提示します。内部的には、C コードをブール プログラムと、このプログラムで遵守すべきルールである述語のセットに抽象化します。次に、シンボリック モデル チェック[6] を使用して、ブール プログラムの述語を検証します。
モデルチェッカーBLAST（Berkeley Lazy Abstraction Software検証ツール）[7]は、Linuxカーネルコードのメモリ安全性と不正なロックエラーを見つけるために使用されます。これは、遅延抽象化[8]と呼ばれる抽象化アルゴリズムを使用して、ドライバーCコードからモデルを構築します。最大50K行のコードを持つCプログラムの一時的な安全性プロパティの検証に成功しています。また、ソースコードの変更が以前のバージョンのプロパティの証明に影響を与えるかどうかを判断するためにも使用され、Windowsデバイスドライバーで実証されています。
Avinux [9] は、 Linuxデバイスドライブの自動解析を容易にする別のツールであり、境界モデルチェッカーCBMCの上に構築されています。[10]これらのモデル検査ツールは長い反例トレースを返すため、正確な障害箇所を見つけるのは困難であり、バグの場所を見つけるための障害特定方法が存在します。[11]
実行時間分析
動的なプログラム分析は、興味深い動作を生成するために十分なテスト入力でプログラムを実行することによって行われます。Safe Drive [12]は、デバイス ドライバーの型安全性違反を検出して回復するためのオーバーヘッドの少ないシステムです。Linux ネットワーク ドライバーのソース コードをわずか 4% 変更するだけで、SafeDrive を実装し、Linux カーネルの保護と回復性を向上させることができました。ハードウェアを使用してデバイス ドライバーをメイン カーネルから分離する同様のプロジェクトは、Nook です。[13]デバイス ドライバーを「nook」と呼ばれる別のハードウェア保護ドメインに配置し、各ページに個別のアクセス許可設定を持たせることで、ドライバーがそのドメインにないページを変更しないようにしますが、同じアドレス空間を共有しているため、すべてのカーネル データを読み取ることができます。
この分野でのもう一つの類似した研究は、ドライバ障害によるオペレーティングシステムの自動回復に関するものである。MINIX 3 [14]は、重大な障害を分離し、欠陥を検出し、故障したコンポーネントを即座に交換できるオペレーティングシステムである。
デバイスドライバ合成
障害の検証と分離の代替案として、デバイス ドライバー開発プロセスに技術を導入して、より堅牢にする方法があります。デバイスの仕様とオペレーティング システムの機能が決まっている場合、そのデバイス用のデバイス ドライバーを合成する方法があります。これにより、人為的なエラーや、システム ソフトウェアの開発にかかるコストと時間が削減されます。合成方法はすべて、ハードウェア デバイスの製造元とオペレーティング システムの機能からの何らかの形式の仕様に依存します。
インターフェース仕様言語
ハードウェア オペレーティング コードは通常、低レベルで、エラーが発生しやすいです。コード開発エンジニアは、通常、不正確または不正確な情報を含むハードウェア ドキュメントに依存しています。ハードウェア機能を表現するインターフェイス定義言語 (IDL) はいくつかあります。最近の OS は、リモート プロシージャ コール IDL のように、これらの IDL を使用してコンポーネントを結合したり、異種性を隠したりします。同じことがハードウェア機能にも当てはまります。このセクションでは、低レベルのコーディングを抽象化し、特定のコンパイラを使用してコードを生成するのに役立つドメイン固有言語でデバイス ドライバーを記述する方法について説明します。
Devil [15]は、デバイスとの通信の高レベル定義を可能にします。ハードウェア コンポーネントは、I/O ポートとメモリ マップ レジスタとして表現されます。これらの仕様は、ドライバー コードから呼び出すことができる C マクロ セットに変換されるため、低レベル関数を記述する際にプログラマが引き起こすエラーが排除されます。NDL [16]は、Devil の拡張機能であり、ドライバーをその操作インターフェイスの観点から記述します。これは、Devil のインターフェイス定義構文を使用し、レジスタ定義のセット、それらのレジスタにアクセスするためのプロトコル、およびデバイス関数のコレクションを含みます。デバイス関数は、そのインターフェイス上の一連の操作に変換されます。デバイス ドライバーを生成するには、まずこれらのインターフェイス仕様言語でドライバー機能を記述し、次に低レベル ドライバー コードを生成するコンパイラを使用する必要があります。
HAIL（ハードウェアアクセスインターフェース言語）[17]は別のドメイン固有のデバイスドライバ仕様言語である。ドライバ開発者は以下を記述する必要がある。
- レジスタ マップの説明。デバイス データ シートのさまざまなデバイス レジスタとビット フィールドについて説明します。
- バスにアクセスするためのアドレス空間の説明。
- 特定のシステムにおけるデバイスのインスタンス化。
- デバイスへのアクセスを制限する不変仕様。
HAIL コンパイラはこれらの入力を受け取り、仕様を C コードに変換します。
ハードウェアソフトウェア共同設計
ハードウェア ソフトウェア共同設計では、設計者は相互に通信する有限ステート マシンを使用してシステムの構造と動作を指定します。次に、一連のテスト、シミュレーション、形式検証がこれらのステート マシンで実行され、どのコンポーネントをハードウェアに組み込み、どのコンポーネントをソフトウェアに組み込むかが決定されます。ハードウェアは通常、フィールド プログラマブル ゲート アレイ (FPGA) または特定用途向け集積回路 (ASIC) で作成され、ソフトウェア部分は低レベルのプログラミング言語に変換されます。このアプローチは主に、センサーを介して環境と継続的に対話するプログラム可能なパーツの集合として定義される組み込みシステムに適用されます。既存の手法[18]は、単純なマイクロ コントローラーとそのドライバーを生成することを目的としています。
スタンドアロンドライバー合成
スタンドアロン合成では、デバイスとシステム ソフトウェアの両方が別々に行われます。デバイスは任意のハードウェア記述言語 (HDL) を使用してモデル化され、ソフトウェア開発者は HDL 仕様にアクセスできません。ハードウェア開発者は、デバイスのデータ シートにデバイス インターフェイスを提示します。ドライバー開発者は、データ シートからデバイスのレジスタとメモリのレイアウト、および有限ステート マシンの形式での動作モデルを抽出します。これは、インターフェイス言語のセクションで説明されているドメイン固有言語で表現されます。最後のステップでは、これらの仕様からコードを生成します。
Termite [19]というツールは、ドライバーを生成するために3つの仕様を取ります。
- デバイス仕様: デバイス データ シートから取得したデバイス レジスタ、メモリ、および割り込みサービスの仕様。
- デバイス クラス仕様: これは、関連するデバイス I/O プロトコル標準から取得できます。たとえば、イーサネットの場合、イーサネット LAN 標準では、これらのコントローラ デバイスの一般的な動作が説明されています。これは通常、パケットの送信、自動ネゴシエーションの完了、リンク ステータスの変更などの一連のイベントとしてエンコードされます。
- OS 仕様: これは、ドライバーとの OS インターフェイスを記述します。具体的には、OS がドライバーに対して実行できる要求、これらの要求の順序、およびこれらの要求に対するドライバーの応答として OS が期待するものについて説明します。これは、各遷移が OS によるドライバーの呼び出し、ドライバーによるコールバック、またはプロトコル指定のイベントに対応する状態マシンを定義します。
これらの仕様に基づいて、Termite は、有効な OS 要求のシーケンスをデバイス コマンドのシーケンスに変換するドライバー実装を生成します。インターフェイスの正式な仕様により、Termite は安全性と活性のプロパティを保持するドライバー コードを生成できます。
RevNIC [20]による非常に興味深いハッキングの取り組みがもう 1 つあります。これは、既存のドライバーをリバース エンジニアリングしてドライバー ステート マシンを生成し、新しいプラットフォーム用の相互移植可能で安全なドライバーを作成するというものです。ドライバーをリバース エンジニアリングするには、シンボリック実行と具体的な実行を使用してドライバーを実行し、ハードウェア I/O 操作を盗聴します。盗聴の出力はシンセサイザーに送られ、シンセサイザーはこれらの複数のトレースと対応するデバイス クラスの定型テンプレートから元のドライバーの制御フロー グラフを再構築します。これらの方法を使用して、研究者はネットワーク インターフェイス用の一部の Windows ドライバーを他の Linux および組み込みオペレーティング システムに移植しました。
批判
静的解析ツールの多くは広く使用されているが、ドライバー合成および検証ツールの多くは実際には広く受け入れられていない。その理由の1つは、ドライバーが複数のデバイスをサポートする傾向があり、ドライバー合成作業では通常、サポートされるデバイスごとに1つのドライバーが生成されるため、ドライバーの数が多くなる可能性があることである。もう1つの理由は、ドライバーも何らかの処理を実行し、ドライバーのステートマシンモデルでは処理を表現できないことである。[21]
結論
この記事で調査したさまざまな検証および合成手法には、それぞれ長所と短所があります。たとえば、実行時の障害分離にはパフォーマンス オーバーヘッドがあり、静的分析ではすべてのクラスのエラーがカバーされるわけではありません。デバイス ドライバー合成の完全な自動化はまだ初期段階にあり、今後の研究の方向性は有望です。現在インターフェイス仕様に使用できる多くの言語が、デバイス ベンダーとオペレーティング システム チームによって普遍的にサポートされる単一の形式に最終的に統合されれば、進歩が促進されます。このような標準化の取り組みの成果は、将来的に信頼性の高いデバイス ドライバーの完全に自動化された合成を実現することです。
参考文献
- ^ Archana Ganapathi、Viji Ganapathi、David Patterson。「Windows XP カーネル クラッシュ分析」。2006 年大規模インストール システム管理カンファレンスの議事録、2006 年。
- ^ A. Chou、J. Yang、B. Chelf、S. Hallem、D. Engler。オペレーティング システム エラーの実証的研究。SOSP、2001 年
- ^ Engler, Dawson、Chef, Benjamin、Chou, Andy、Hallem, Seth。「システム固有のプログラマーが作成したコンパイラー拡張機能を使用したシステムルールのチェック」。2000 年、第 4 回オペレーティング システム設計および実装シンポジウム会議の議事録
- ^ Jhala, Ranjit および Majumdar, Rupak. 「ソフトウェア モデル検査」。ACM Computation Survey。2009 年
- ^ Thomas Ball、Ella Bounimova、Byron Cook、Vladimir Levin、Jakob Lichtenberg、Con McGarvey、Bohus Ondrusek、Sriram Rajamani、および Abdullah Ustuner。「デバイス ドライバーの徹底的な静的分析」、SIGOPS Oper. Syst. Rev、Vol. 40、2006 年。
- ^ McMillan, Kenneth L.「シンボリックモデルチェック」Kluwer Academic Publishers、1993年。
- ^ Thomas A. Henzinger、Ranjit Jhala、Rupak Majumdar、Gregoire Sutre。「BLAST によるソフトウェア検証」。SPIN、2003 年。
- ^ Thomas A. Henzinger、Ranjit Jhala、Rupak Majumdar、Gregoire Sutre。「Lazy Abstraction」、ACM SIGPLAN-SIGACT プログラミング言語の原則に関する会議、2002 年。
- ^ H. Post、W. Küchlin。「Linux デバイス ドライバー検証のための静的解析の統合」。第 6 回統合形式手法国際会議、2007 年。
- ^ Edmund Clarke、Daniel Kroening、Flavio Lerda。「ANSI-C プログラムをチェックするためのツール」。TACAS、2004 年
- ^ Thomas Ball、Mayur Naik、Sriram K. Rajamani。「症状から原因へ: 反例トレースのエラーの特定」ACM SIGPLAN Notices、2003 年。
- ^ Feng Zhou、Jeremy Condit、Zachary Anderson、Ilya Bagrak、Rob Ennals、Matthew Harren、George Necula、Eric Brewer。「SafeDrive: 言語ベースの手法を使用した安全で回復可能な拡張機能」。第 7 回 OSDI、2006 年。
- ^ Michael M. Swift、Steven Martin、Henry M. Levy、および Susan J. Eggers。「Nooks: 信頼性の高いデバイス ドライバーのアーキテクチャ」。第 10 回 ACM SIGOPS、2002 年。
- ^ Jorrit N. Herder、Herbert Bos、Ben Gras、Philip Homburg、Andrew S. Tanenbaum。「MINIX 3: 信頼性が高く、自己修復機能を備えたオペレーティング システム」。SIGOPS Oper. Syst. Rev. 40、2006 年。
- ^ Fabrice Merillon、Laurent Reveillere、Charles Consel、Renaud Marlet、および Gilles Muller。「Devil: ハードウェア プログラミング用の IDL」。第 4 回オペレーティング システムの設計と実装に関するシンポジウム会議の議事録、第 4 巻、2000 年。
- ^ Christopher L. Conway および Stephen A. Edwards. 「NDL: デバイス ドライバー用のドメイン固有言語」。ACM SIGPLAN Notices 39、2004 年。
- ^ J. Sun、W. Yuan、M. Kallahalla、N. Islam。「HAIL: 簡単で正確なデバイス アクセスのための言語」。ACM 組み込みソフトウェア カンファレンスの議事録、2005 年。
- ^ Felice Balarin 他「組み込みシステムのハードウェアとソフトウェアの共同設計。POLIS アプローチ」Kluwer Academic Publishers、1997 年。
- ^ Leonid Ryzhyk、Peter Chubb、Ihor Kuz、Etienne Le Sueur、Gernot Heiser。「Termite によるデバイス ドライバーの自動合成」。2009 年、第 22 回 ACM オペレーティング システム原則シンポジウムの議事録。
- ^ Vitaly Chipounov および George Candea。「RevNIC を使用したバイナリ デバイス ドライバーのリバース エンジニアリング」。第 5 回 ACM SIGOPS/EuroSys、2010 年。
- ^ Asim Kadav と Michael M. Swift「最新のデバイス ドライバーを理解する」プログラミング言語とオペレーティング システムのアーキテクチャ サポートに関する第 17 回 ACM カンファレンスの議事録
外部リンク
- Future Chips: ハードウェアとソフトウェアの共同設計に特化したウェブサイト
- Avinux、Linux デバイス ドライバーの自動検証に向けて
- BLAST: Berkeley Lazy Abstraction ソフトウェア検証ツール
- Microsoft の静的ドライバー検証ツール
- SafeDrive - 言語ベースの技術を使用した安全で回復可能な拡張機能
- Nook : 市販のオペレーティングシステムの信頼性の向上
- BugAssist: 障害箇所特定ツール
- デバイス ドライバーのリバース エンジニアリング 2011-01-08 にWayback Machineでアーカイブされました
- HAIL 簡単で正確なデバイスアクセスのための言語 2010-05-19 にWayback Machineでアーカイブ