seL4

本サイトが提示する下記のベストプラクティスを実行するプロジェクトは、Open Source Security Foundation (OpenSSF) バッジを達成したことを自主的に自己認証し、そのことを外部に示すことができます。

ソフトウェアに欠陥や脆弱性がないことを保証する手立てはありません。形式論的な証明ができたとしても、仕様や前提が間違っていると誤動作の可能性があります。また、プロジェクトが健全で、かつ機能的な開発コミュニティであり続けることを保証する手立てもありません。しかし、ベストプラクティスの採用は、プロジェクトの成果の向上に寄与する可能性があります。たとえば、いくつものベストプラクティスがリリース前の複数人によるレビューを定めていますが、それによりレビュー以外では発見困難な技術的脆弱性を見つけるのを助け、同時に異なる企業の開発者間の信頼を築き、さらに交流を続けることに対する意欲を生んでいます。バッジを獲得するには、すべてのMUSTおよびMUST NOT基準を満たさなければなりません。すべてのSHOULD基準も満たさなければなりませんが、正当な理由がある場合は満たさなくても構いません。そしてすべてのSUGGESTED基準も満たさなければなりませんが、満たさないとしても、少なくとも考慮することが望まれます。フィードバックは、 GitHubサイトのissueまたはpull requestとして提示されれば歓迎します。また、議論のためのメールリストも用意されています。

私たちは多言語で情報を提供していますが、翻訳版に矛盾や意味の不一致がある場合は、英語版を正式な記述とします。
これがあなたのプロジェクトなら、あなたのプロジェクトページにあなたのバッジステータスを表示してください！バッジステータスは次のようになります。 プロジェクト 5003 のバッジ レベルは silver です バッジステータスの埋め込み方法は次のとおりです。
バッジステータスを表示するには、あなたのプロジェクトのマークダウンファイルに以下を埋め込みます
[![OpenSSF Best Practices](https://www.bestpractices.dev/projects/5003/badge)](https://www.bestpractices.dev/projects/5003)
あるいは、以下をHTMLに埋め込みます
<a href="https://www.bestpractices.dev/projects/5003"><img src="https://www.bestpractices.dev/projects/5003/badge"></a>


これらは合格レベルの基準です。シルバーまたはゴールドレベル基準を表示することもできます。



 基本的情報 13/13 ●

  • 識別情報

    他のプロジェクトが同じ名前を使用していないか注意してください。

    The seL4 microkernel

    どのようなプログラミング言語を使ってプロジェクトを実装していますか？
    複数の言語がある場合は、コンマを区切り（スペースを入れてもよい）としてリストし、使用頻度の高いものから順に並べます。使用言語が多くある場合は、少なくとも最初の3つの最も多く使われるものをリストアップしてください。言語がない場合（例：ドキュメントだけ、またはテスト専用のプロジェクトの場合）、1文字 " - "を使用します。言語ごとにある大文字・小文字の慣用を踏襲してください（例：「JavaScript」）。
    Common Platform Enumeration（CPE）は、情報技術（IT）システム、ソフトウェア、およびパッケージのための構造化された命名体系です。脆弱性を報告する際に、多くのシステムやデータベースで使用されています。

  • 基本的なプロジェクト ウェブサイトのコンテンツ


    バッジには十分です！

    プロジェクトのウェブサイトは、ソフトウェアが何をするのか（何の問題を解決するのか）を簡潔に記述しなければなりません。 [description_good]
    これは、潜在的なユーザーが理解できる言語でなければなりません（例えば、それは最小限の専門用語を使用します）。

    https://sel4.systems/About/


    バッジには十分です！

    プロジェクトのウェブサイトは、取得方法、フィードバックの提供方法（バグ報告や拡張機能）、ソフトウェアへの貢献方法に関する情報を提供しなければなりません。 [interact]

    To obtain: see top line of https://docs.sel4.systems To contribute: see https://sel4.systems/Contribute.html For contact: https://sel4.systems/contact.html


    バッジには十分です！

    貢献する方法に関する情報は、貢献プロセス（たとえばプル リクエストが使用されか、など）を説明する必要があります。 (URLが必要です) [contribution]
    別段の記載がない限り、GitHub上のプロジェクトは、（GitHubが提供する）課題管理とプルリクエストを使用することを想定します。この情報は不足しているかもしれません。すなわち、プロジェクトがプルリクエストと課題追跡ツールを使うことか、メーリングリストへの投稿を言及している。（どちら？）

    The main contribution guidelines are in https://docs.sel4.systems/processes/contributing.html, additional guidelines specific to seL4 in https://docs.sel4.systems/projects/sel4/kernel-contribution.html. Both are reachable from the CONTRIBUTION.md file in the repository and the main "Contribute" link on the home page at https://sel4.systems/Contribute.html


    バッジには十分です！

    貢献する方法に関する情報は、貢献を受け入れるための要件（たとえば、必要なコーディング標準への参照）を含むべきです。 (URLが必要です) [contribution_requirements]

    See "Conventions" at the top of https://docs.sel4.systems/processes/contributing.html. The "Pull requests" link from that page also contains required tests, and formal verification.


  • FLOSSライセンス

    プロジェクトのライセンスはどのようなものですか？
    SPDXライセンスの表現形式を使用してください。 例：「Apache-2.0」、「BSD-2-Clause」、「BSD-3-Clause」、「GPL-2.0+」、「LGPL-3.0+」、「MIT」、「(BSD-2-Clause OR Ruby)」。一重引用符または二重引用符を含めないでください。


    バッジには十分です！

    プロジェクトによって作成されたソフトウェアは、FLOSSとしてリリースされなければなりません。 [floss_license]
    FLOSSは、オープンソース定義またはフリーソフトウェア定義を満たす方法でリリースされたソフトウェアです。そのようなライセンスの例としては、CC0、MIT、2項型BSD、 3項型BSD、 Apache 2.0 、Less GNU General Public License（LGPL）、および GNU General Public License（GPL）を参照してください。私たちの目的のためには、これはライセンスが以下のものでなければならないことを意味します： ソフトウェアは他の方法でライセンスされているかもしれません（たとえば、「GPLv2またはプロプライエタリ」は許容されます）。

    Kernel code in the seL4 repository is licensed under GPL-2.0-only. Library code on top of the kernel under BSD-2-Clause. See also https://github.com/seL4/seL4/blob/master/LICENSE.md The GPL-2.0-only license is approved by the Open Source Initiative (OSI).


    バッジには十分です！

    プロジェクトによって作成されたソフトウェアに必要なライセンスは、オープンソース・イニシアチブ（OSI）によって承認されていることが推奨されています。 [floss_license_osi]
    OSIは、厳格な承認プロセスを使用して、どのライセンスがOSSであるかを判断します。

    Both GPL-2.0-only and BSD-2-Clause are OSI approved. See also https://github.com/seL4/seL4/tree/master/LICENSES for the full list of things that are mentioned by any auxiliary tools and files. The GPL-2.0-only license is approved by the Open Source Initiative (OSI).


    バッジには十分です！

    プロジェクトは、結果のライセンスをソースリポジトリの標準的な場所に投稿しなければなりません。 (URLが必要です) [license_location]
    たとえば、LICENSEまたはCOPYINGという名前の最上位ファイルです。ライセンスファイル名の後に ".txt" や ".md" などの拡張子を付けることができます。別の規則は、ライセンスファイルを含むLICENSESという名前のディレクトリを持つことです。これらのファイルは通常、 REUSE仕様で説明されているように、SPDXライセンス識別子とそれに続く適切なファイル拡張子として名前が付けられます。この基準は、ソースリポジトリの要件にすぎないことに注意してください。ソースコード（実行可能ファイル、パッケージ、コンテナなど）から何かを生成するときに、ライセンスファイルを含める必要はありません。たとえば、Comprehensive R Archive Network（CRAN）のRパッケージを生成するときは、標準のCRANプラクティスに従います。ライセンスが標準ライセンスの場合は、標準の短いライセンス仕様を使用して（テキストのコピーをさらにインストールしないようにするため）、リストします。 .Rbuildignoreなどの除外ファイル内のLICENSEファイル。同様に、Debianパッケージを作成する場合、著作権ファイルに /usr/share/common-licenses のライセンス テキストへのリンクを配置し、作成したパッケージからライセンス ファイルを除外できます（たとえば、dh_auto_installを呼び出した後にファイルを削除します ）。可能な場合は、生成された形式で機械可読ライセンス情報を含めることをお勧めします。

    See https://github.com/seL4/seL4/tree/master/LICENSES.


  • ドキュメンテーション


    バッジには十分です！

    プロジェクトは、プロジェクトによって作成されたソフトウェアに関する基本的なドキュメンテーションを提供しなければなりません。 [documentation_basics]
    このドキュメントは、インストール方法、起動方法、使用方法（可能であれば例示したチュートリアル）、および、そのソフトウェアの適切なトピックであれば安全に使用する方法（たとえば何をするべきで、何をすべきでないか）を記述し、メディア（たとえば、テキストやビデオなど）に収められている必要があります。セキュリティの文書は必ずしも長文である必要はありません。プロジェクトは、ドキュメンテーションとしてプロジェクト以外の素材へのハイパーテキストリンクを使用してもよいです。プロジェクトがソフトウェアを作成しない場合は、「該当なし」（N / A）を選択します。

    The sources of the reference manual are kept in https://github.com/seL4/seL4/tree/master/manual. There is an entire separate documentation site for seL4 at https://docs.sel4.systems


    バッジには十分です！

    プロジェクトは、プロジェクトによって作成されたソフトウェアの外部インタフェース（入力と出力の両方）を記述する参照ドキュメントを提供しなければなりません。 [documentation_interface]
    外部インターフェイスのドキュメントは、エンドユーザーまたは開発者に、その使用方法を説明します。ドキュメントには、ソフトウェアにアプリケーション プログラム インターフェイス（API）が含まれている場合、アプリケーション プログラム インターフェイスが含まれます。ライブラリの場合、呼び出すことができる主要なクラス/型とメソッド/関数を文書化します。ウェブ アプリケーションの場合、URLインタフェース（多くの場合、RESTインタフェース）を定義します。コマンドラインインターフェイスの場合は、サポートするパラメータとオプションを文書化します。多くの場合、ドキュメントのほとんどを自動生成すると、ソフトウェアが変更されたときにドキュメントがソフトウェアと同期したままなので、最も良い方法ですが、これは必須ではありません。プロジェクトは、ドキュメンテーションとしてプロジェクト以外の素材へのハイパーテキストリンクを使用してもよいです。ドキュメンテーションは自動的に生成されるかもしれません（実際的に、しばしばこれを行う最良の方法です）。 RESTインタフェースのドキュメントは、Swagger / OpenAPIを使用して生成することができます。コード インタフェースのドキュメントは、 JSDoc （JavaScript）、 ESDoc （JavaScript）、pydoc（Python）、devtools (R)、pkgdown (R)、およびDoxygen（多数）のいずれかです。実装コードにコメントがあるだけでは、この基準を満たすには不十分です。すべてのソースコードを読むことなく情報を見るための簡単な方法が必要です。プロジェクトがソフトウェアを作成しない場合は、「該当なし」（N/A）を選択します。

    The reference manual includes a full API description. See chapter 10 of https://sel4.systems/Info/Docs/seL4-manual-latest.pdf


  • その他


    バッジには十分です！

    プロジェクトサイト（ウェブサイト、リポジトリ、およびダウンロードURL）は、TLSを使用したHTTPSをサポートしなければなりません。 [sites_https]
    これには、プロジェクトのホームページのURLとバージョン管理リポジトリのURLが「http：」ではなく「https：」で始まる必要があります。Let's Encryptからフリーの証明書を入手できます。プロジェクトは、（例えば） GitHubページ、 GitLabページ、またはSourceForgeプロジェクトページを使ってこの基準を実装してもよいです。HTTPをサポートしている場合は、HTTPトラフィックをHTTPSにリダイレクトすることを強くお勧めします。

    Given only https: URLs.


    バッジには十分です！

    プロジェクトは、議論（提案された変更や問題を含む）のための1つ以上の検索可能なメカニズムを持たなければならず、メッセージやトピックがURLでアドレス指定され、新しい人々がディスカッションのいくつかに参加できるようにしなければならず、クライアント側でプロプライエタリなソフトウェアのインストールを必要としないようにします。 [discussion]
    受け入れ可能なメカニズムの例には、アーカイブされたメーリングリスト、GitHubのイシューとプルリクエストの議論、Bugzilla、Mantis、Tracなどがあります。非同期ディスカッション メカニズム（IRCなど）は、これらの基準を満たしていれば許容されます。 URLアドレス可能なアーカイブ機構があることを確認してください。独自のJavaScriptは、推奨されませんが、許可されています。

    GitHub supports discussions on issues and pull requests.


    バッジには十分です！

    プロジェクトは英語で文書を提供し、英語でコードに関するバグ報告とコメントを受け入れることができるべきです。 [english]
    現在、英語はコンピュータ技術のリンガ フランカです。英語をサポートすることで、世界中のさまざまな潜在的な開発者とレビュアーの数を増やします。コア開発者の主要言語が英語でなくても、プロジェクトはこの基準を満たすことができます。

    The main project language is English


    バッジには十分です！

    プロジェクトはメンテナンスされている必要があります。 [maintained]
    少なくとも、プロジェクトは重大な問題と脆弱性の報告に対応するように努める必要があります。バッジを積極的に追求しているプロジェクトは、おそらくメンテナンスされているでしょう。すべてのプロジェクトや人のリソースには限りがあり、提案された変更をプロジェクトが拒否しなければならないこともあるため、リソースに限りがあることや、提案が拒否されることが、メンテナンスされていないプロジェクトを示すわけではありません。

    プロジェクトが今後メンテナンスされなくなることがわかった場合は、この基準を「不適合（Unmet）」に設定し、適切なメカニズムを使用して、メンテナンスされないことを人々に示す必要があります。たとえば、READMEの最初の見出しに「DEPRECATED」（将来のサポートが保証されないので使用すべきでない）を使用し、ホームページの先頭近くに「DEPRECATED」を追加し、コード リポジトリのプロジェクトの説明の先頭に「DEPRECATED」を追加し、そのREADMEおよび/またはホームページにno-maintenance-intendedバッジを追加し、すべてのパッケージ リポジトリでdeprecated（非推奨）としてマークしたり（例： npm deprecate ）、コード リポジトリのマーキングシステムを使用してアーカイブします（例：GitHubの"archive" 設定、GitLabの"archived" マーキング、 Gerritの "readonly" ステータス、またはSourceForgeの"abandoned" プロジェクト ステータス）。詳細な説明については、こちらを参照してください。

    The project is maintained by the seL4 Foundation https://sel4.systems/Foundation.html



（詳細）このバッジエントリを編集する権限を持つユーザーは？ 現在：[]
ほとんどのプロジェクトはこのフィールドを無視するべきです。プロジェクトのバッジエントリは、バッジエントリのオーナー（作成者）、BadgeApp管理者、GitHubリポジトリにコミットできる人（GitHub上にある場合）によっていつでも編集できます。他の人がこのバッジエントリを編集できるようにする必要があり、あなたがこのプロジェクトのバッジ エントリの編集権限をすでに持っている場合は、編集権限を持つ追加のユーザを追加することができます。"+"と入力し、その後にカンマ区切りの整数ユーザーIDのリストを入力します。そうすることで、これらのユーザーも、このプロジェクト エントリを編集できるようになります。あなたがバッジ エントリのオーナーまたはBadgeApp管理者である場合は、"-"と入力した後にカンマで区切られた整数ユーザーIDのリストを入力すれば、このリストからユーザーを削除できます。通常、特定のバッジエントリを一度に編集するのは1人だけであると予想されます。複数のユーザーが同時に編集しようとすると、このアプリケーションはオプティミスティック ロック機能を使用して古いデータを保存しないようにします。複数の編集者がいる場合は、バッジ エントリ データを段階的かつ頻繁に保存することをお勧めします（いずれにしてもこれは賢明な方法です）。



 変更管理 9/9 ●

  • 公開されたバージョン管理ソースリポジトリ


    バッジには十分です！

    プロジェクトには、公開され、URLを持つ、バージョン管理のソース リポジトリがなければなりません。 [repo_public]
    URLはプロジェクトのURLと同じであってもよいです。プロジェクトは、変更が公開されていない間に（例えば、公開前に脆弱性を修正するため）、特定のケースでプライベート（非公開）ブランチを使用することができます。

    Repository on GitHub, which provides public git repositories with URLs.


    バッジには十分です！

    プロジェクトのソース リポジトリは、どのような変更が行われたのか、誰が変更を行ったのか、いつ変更が行われたのかを追跡しなければなりません。 [repo_track]

    Repository on GitHub, which uses git. git can track the changes, who made them, and when they were made.


    バッジには十分です！

    共同レビューを可能にするために、プロジェクトのソースリポジトリには、リリース間のレビューのための中間バージョンが含まれなければなりません。最終リリースのみを含めることはできません。 [repo_interim]
    プロジェクトは、公開ソース リポジトリから特定の暫定版を省略することを選択することができます。（たとえば、特定の非公開のセキュリティ脆弱性を修正するものは、公開されないか、または、合法的に投稿できないか、最終リリースに入らないです）

    The project repository includes the entire development history between releases.


    バッジには十分です！

    プロジェクトのソース リポジトリに共通の分散バージョン管理ソフトウェア（gitなど）を使用することを推奨します。 [repo_distributed]
    Gitが特別に必要とされているわけでなく、プロジェクトでは、集中型バージョン管理ソフトウェア（例：subversion）を正当とする証拠を持って使用できます。

    Repository on GitHub, which uses git. git is distributed.


  • 一意的なバージョン番号


    バッジには十分です！

    プロジェクトの結果には、ユーザーが使用することを意図されたリリースごとに固有のバージョン識別子が必要です。 [version_unique]
    これはコミットID（git commit idやmercurial changeset idなど）やバージョン番号（YYYYMMDDのようなセマンティックバージョニングや日付ベースのスキームを使用するバージョン番号を含む）など、さまざまな方法で対応できます。

    seL4 uses semantic versioning


    バッジには十分です！

    リリースには、Semantic Versioning (SemVer)またはCalendar Versioning (CalVer)のバージョン番号形式を使用することが推奨されます。CalVerを使用する場合は、マイクロレベル値を含めることが推奨されます。 [version_semver]
    プロジェクトは一般的に、エコシステムで使用されている通常のフォーマットなど、ユーザーが期待しているフォーマットを優先するべきです。多くのエコシステムではSemVerが好まれており、一般的にSemVerはアプリケーションプログラマインターフェース（API）やソフトウェア開発キット（SDK）に好まれています。CalVerは、規模が大きく、独自に開発した依存関係が異常に多いプロジェクトや、スコープが常に変化するプロジェクト、時間的な制約があるプロジェクトで使用される傾向があります。CalVerを使用する際には、マイクロレベルの値を含めることが推奨されます。マイクロレベルを含めることで、必要になった場合にはいつでも同時にメンテナンスされるブランチをサポートできるからです。git commit ID や mercurial changeset ID など、バージョンを一意に識別できるものであれば、他のバージョン番号形式をバージョン番号として使用することができます。しかし、(git commit ID のような)いくつかの代替形式は、リリースの識別子として問題を引き起こす可能性があります。すべての受信者が最新バージョンを実行しているだけの場合 （たとえば、継続的な配信を介して常に更新されている単一のWebサイトまたはインターネットサービスのコード）には、バージョン ID の形式はソフトウェアのリリースを識別する上で重要ではないかもしれません。

    バッジには十分です！

    プロジェクトがバージョン管理システム内の各リリースを特定することが推奨されています。たとえば、gitを使用しているユーザーがgitタグを使用して各リリースを特定することが推奨されています。 [version_tags]

    seL4 uses git tags and the GitHub release mechanism to identify releases


  • リリースノート


    バッジには十分です！

    プロジェクトは、各リリースにおいて、ユーザーがアップグレードすべきかどうか、また、アップグレードの影響を判断できるよう、そのリリースの主要な変更の要約を説明したリリースノートを提供しなければなりません（MUST）。リリースノートは、バージョン管理ログの生の出力であってはなりません（例えば、 "git log"コマンドの結果はリリースノートではない）。プロジェクトの成果物が複数の場所で再利用されることを意図していないプロジェクト（単独のウェブサイトやサービスのためのソフトウェアなど）で、かつ、継続的・断続的な配布を行う場合は、「該当なし」を選択することができます。 (URLが必要です) [release_notes]
    リリースノートは様々な方法で実装できます（MAY）。多くのプロジェクトは、 "NEWS"、 "CHANGELOG"、または "ChangeLog"という名前のファイルでそれらを提供し、 ".txt"、 ".md"、 ".html"などの拡張子を付けることもあります。歴史的には、 "change log"という言葉はすべての変更のログを意味していましたが、本基準を満たすために必要なものは、人間が読める要約です。リリースノートは代わりに、 GitHubリリースのワークフローなどのバージョン管理システムのメカニズムによって提供してもよい（MAY）。

    Release notes are posted on the seL4 website, see e.g. https://docs.sel4.systems/releases/sel4/12.1.0


    バッジには十分です！

    リリースノートでは、このリリースで修正された、リリースの作成時にすでにCVE割り当てなどがあった、公に知られているランタイムの脆弱性をすべて特定する必要があります。 ユーザーが通常、ソフトウェアを実際に更新できない場合（たとえば、カーネルの更新によくあることです）、この基準は該当なし（N/A）としてマークされる場合があります。 この基準はプロジェクトの結果にのみ適用され、依存関係には適用されません。 リリースノートがない場合、または公に知られている脆弱性がない場合は、[N/A]を選択します。 [release_notes_vulns]
    この基準は、特定の更新によって一般に知られている脆弱性が修正されるかどうかをユーザーが判断するのに役立ち、ユーザーが情報に基づいて更新について決定できるようにします。ユーザーが通常、コンピューター上でソフトウェア自体を実際に更新することはできず、代わりに1つ以上の仲介者に依存して更新を実行する必要がある場合（カーネルお​​よびカーネルと絡み合っている下位レベルのソフトウェアの場合によくあることです）、この追加情報はそれらのユーザーには役立たないため、プロジェクトは「該当なし」（N/A）を選択する場合があります。同様に、すべての受信者が最新バージョンのみを実行している場合（継続的デリバリーによって絶えず更新される単一のWebサイトまたはインターネットサービスのコードなど）、プロジェクトはN/Aを選択できます。この基準はプロジェクトの結果にのみ適用され、依存関係には適用されません。プロジェクトのすべての推移的な依存関係の脆弱性を一覧表示することは、依存関係が増加および変化するにつれて扱いにくくなるため、不要です。依存関係を調べて追跡するツールがよりスケーラブルな方法でこれを実行できます。

    seL4 has not any CVE assignments or similar yet, but any security improvements are identified in the release notes.


 報告 8/8 ●

  • バグ報告プロセス


    バッジには十分です！

    プロジェクトは、ユーザーが不具合報告を送信するプロセスを提供しなければなりません（たとえば、課題トラッカーやメーリングリストを使用します）。 (URLが必要です) [report_process]

    See https://github.com/seL4/seL4/issues


    バッジには十分です！

    プロジェクトは、個々の課題を追跡するための課題トラッカーを使用するべきです。 [report_tracker]

    See https://github.com/seL4/seL4/issues


    バッジには十分です！

    このプロジェクトは、過去2〜12か月間に提出された多数のバグ報告の受領を認めなければなりません。応答に修正を含める必要はありません。 [report_responses]

    Almost all issues on https://github.com/seL4/seL4/issues have a response (apart from those that we use for internal tracking).


    バッジには十分です！

    プロジェクトは、直近2〜12ヶ月（2ヶ月を含む）に増強要求の多数（> 50％）に対応すべきです。 [enhancement_responses]
    応答は、「いいえ」や、そのメリットについての議論であってもよいです。目標は、単にプロジェクトがまだ生きていることを示している、いくつかの要求に対する応答があることです。この基準のために、プロジェクトは偽のリクエスト（スパマーや自動システムなど）をカウントする必要はありません。プロジェクトで機能強化が行われていない場合は、「満足されない」（unmet）を選択し、この状況をユーザーに明確にするURLを含めてください。プロジェクトが強化要求の数によって圧倒される傾向がある場合は、「満足されない」（unmet）を選択して説明してください。

    Almost all issues on https://github.com/seL4/seL4/issues have a response. Most issues are enhancement requests or questions.


    バッジには十分です！

    プロジェクトは、後で検索するために、レポートとレスポンスのアーカイブを公開する必要があります。 (URLが必要です) [report_archive]

    See https://github.com/seL4/seL4/issues for current and https://sel4.atlassian.net/ for older issues (latter requires account, but account creation is possible for anyone).


  • 脆弱性報告プロセス


    バッジには十分です！

    プロジェクトは、脆弱性を報告するプロセスをプロジェクト サイトに公開しなければなりません。 (URLが必要です) [vulnerability_report_process]
    たとえば、https：// PROJECTSITE / securityの明示的に指定されたメール アドレスで、これはしばしばsecurity@example.orgの形式です。これはバグ報告プロセスと同じかもしれません。脆弱性レポートは常に公開される可能性がありますが、多くのプロジェクトでは、プライベート脆弱性を報告するメカニズムがあります。

    See https://github.com/seL4/seL4/blob/master/SECURITY.md


    バッジには十分です！

    プライベート脆弱性報告がサポートされている場合、プロジェクトは、プライベートに保持された方法で情報を送信する方法を含んでいなくてはなりません。 (URLが必要です) [vulnerability_report_private]
    例としては、HTTPS（TLS）を使用してWeb上に提出されたプライベート不具合報告や、OpenPGPを使用して暗号化された電子メールがあります。脆弱性報告が常に公開されている場合（プライベート脆弱性報告は存在しないため）、「該当なし」（N / A）を選択します。

    The project provides a gpg key for private communication, see "Official channel" in https://github.com/seL4/seL4/blob/master/SECURITY.md


    バッジには十分です！

    過去6ヶ月間に受け取った脆弱性報告に対するプロジェクトの初期応答時間は、14日以下でなければなりません。 [vulnerability_report_response]
    過去6か月間に脆弱性が報告されていない場合は、「該当なし」（N/A）を選択します。

    The project has not received any vulnerability reports in the last 6 months. Vulnerabilities in seL4 are extremely rare.


 品質 13/13 ●

  • 作業ビルドシステム


    バッジには十分です！

    プロジェクトによって作成されたソフトウェアを利用するためにビルドが必要な場合、プロジェクトは、ソース コードからソフトウェアを自動的にリビルドできる作業ビルド システムを提供しなければなりません。 [build]
    ビルドシステムは、ソフトウェアをリビルドするのに必要なアクション（およびその順序）を決定し、それらのステップを実行します。たとえば、ビルドシステムは、ソースコードをコンパイルするためにコンパイラを呼び出すことができます。実行可能ファイルがソースコードから生成される場合、ビルドシステムは、プロジェクトのソースコードを変更でき、その変更を含む更新された実行ファイルを生成できなければなりません。プロジェクトによって生成されたソフトウェアが外部ライブラリに依存する場合、ビルドシステムはそれらの外部ライブラリをビルドする必要はありません。ソースコードが変更されても、ソフトウェアを使用するためにビルドする必要がない場合、「該当なし」（N/A）を選択します。

    The project uses CMake


    バッジには十分です！

    ソフトウエアをビルドするために、一般的なツールを使用することをお勧めします。 [build_common_tools]
    たとえば、Maven、Ant、cmake、autotools、make、rake (Ruby)、 devtools （R）などです。

    CMake is commonly used.


    バッジには十分です！

    プロジェクトは、FLOSSツールだけを使用してビルドができるようにするべきです。 [build_floss_tools]

    All build tools needed for seL4 are FLOSS tools.


  • 自動テスト スイート


    バッジには十分です！

    プロジェクトは、FLOSSとして公開されている自動テストスイートを少なくとも1つ使用する必要があります（このテストスイートは、別個のFLOSSプロジェクトとして維持される場合があります）。 プロジェクトは、テストスイートの実行方法を明確に示すか文書化する必要があります（たとえば、継続的インテグレーション（CI）スクリプトを介して、またはBUILD.md、README.md、CONTRIBUTING.mdなどのファイルの文書を介して）。 [test]
    プロジェクトでは、複数の自動化されたテストスイートを使用することができます（たとえば、迅速に実行するもの、より完全であるが特別な装置が必要なもの）。Selenium (ウェブブラウザの自動化)、Junit (JVM, Java)、RUnit (R)、testthat (R) など、多くのテストフレームワークやテスト支援システムが利用可能です。

    See https://github.com/seL4/sel4test and https://github.com/seL4/sel4test-manifest


    バッジには十分です！

    テスト スイートは、その言語の標準的な方法で呼び出すことができるべきです。 [test_invocation]
    たとえば、「make check」、「mvn test」、「rake test」（Ruby）などです。

    The test suite uses a standard init, compile, run cycle. See e.g. https://docs.sel4.systems/GettingStarted.html#running-sel4


    バッジには十分です！

    テスト スイートは、コードブランチ、入力フィールド、および機能のほとんど（または理想的にはすべて）をカバーすることが推奨されています。 [test_most]

    The sel4test suite covers most (but not all) of the branches of seL4.


    バッジには十分です！

    プロジェクトは、継続的インテグレーション（新しいコードまたは変更されたコードが頻繁に中央コードリポジトリに統合され、その結果に対して自動テストが実行される）を実装することを推奨されています。 [test_continuous_integration]

    The project currently is running CI for both tests and formal verification. See e.g. https://sel4.systems/~bamboo/logs/RELEASE-SEL4TEST-HWTESTSGHSTATUS/1124/ for an example.


  • 新機能テスト


    バッジには十分です！

    プロジェクトは、プロジェクトで作成されたソフトウェアに主要な新機能が追加されたときに、その機能のテストを自動化されたテスト スイートに追加する必要があるという一般的な方針（正式でも、正式でなくても構いません）を持っていなければなりません。 [test_policy]
    開発者はテストを自動テスト スイートに追加して、新しい機能を追加する必要があるというポリシーが、口頭でも（文書化されていなくても）、存在する限り、「満たしている」を選択してください。

    The policy for new feature testing is informal (but implied). The policy for requiring formal verification is explicit. See e.g. section on Tests in https://docs.sel4.systems/processes/code-review.html


    バッジには十分です！

    プロジェクトによって作成されたソフトウェアの最新の大きな変更で、テストを追加するための test_policy が守られているという証拠がプロジェクトに存在しなければなりません。 [tests_are_added]
    主要な機能は、通常、リリースノートに記載されます。完璧は必要ないですが、プロジェクトによって生成されたソフトウェアに新しい主要機能が追加されたときに、自動テスト スイートに実際にテストが追加されているという証拠となります。

    The last releases have not included major API changes (mostly refactoring, performance improvements, build system improvements, and fixes in experimental features), but you can see reviewers requiring tests on pull requests, e.g. https://github.com/seL4/seL4/pull/322#pullrequestreview-686920158 or https://github.com/seL4/seL4/pull/322#issuecomment-865432029 on a pull request for an experimental feature that would be switched off by default (not yet released).


    バッジには十分です！

    テストを追加するこのポリシー（test_policyを参照）を変更提案に関する手順で文書化することを推奨します。 [tests_documented_added]
    しかし、実際にテストが追加されている限り、非公式の規則でも許容されます。

    See section on Tests in https://docs.sel4.systems/processes/code-review.html


  • 警告フラグ


    バッジには十分です！

    プロジェクトは、選択した言語でこの基準を実装することができる少なくとも1つのFLOSSツールがあれば、1つまたは複数のコンパイラ警告フラグ、「安全」言語モードを使用可能にするか、分離 「リンター」ツールを使用してコード品質エラーまたは共通の単純なミスを検索しなければなりません。 [warnings]
    コンパイラ警告フラグの例には、gcc / clang "-Wall"があります。 「安全」言語モードの例には、JavaScript「use strict」とperl5の「use warnings」があります。分離「リンター」ツールは、ソースコードを調べてコード品質のエラーや一般的な単純なミスを探すツールです。これらは、通常、ソースコードまたはビルド命令内で有効になります。

    The project compiles with -Wall and -Werror, see e.g. https://github.com/seL4/seL4/blob/8afebb55a0318f68c182b270757bb29e8100f952/CMakeLists.txt#L175-L176


    バッジには十分です！

    プロジェクトは警告を出さなければならない。 [warnings_fixed]
    これらは、警告基準の実装によって識別される警告です。プロジェクトは、警告を修正するか、ソースコード内で警告を誤検出としてマークするべきです。理想的には警告がないことがいいですが、プロジェクトはある程度の警告（通常は100行あたり1警告未満、または全体で10警告未満）を受け入れることができます。

    All compiler warnings are addressed (running on -Werror)


    バッジには十分です！

    プロジェクトによって作成されたソフトウェアにある警告に、実際的な場合には、最大限に厳格になることを推奨されています。 [warnings_strict]
    一部の警告は、あるプロジェクトでは効果的に有効にすることはできません。必要なのは、プロジェクトが可能な限り警告フラグを有効にするように努力しており、エラーが早期に検出されるという証拠です。

    The project compiles with -Wall and -Werror, see e.g. https://github.com/seL4/seL4/blob/8afebb55a0318f68c182b270757bb29e8100f952/CMakeLists.txt#L175-L176


 セキュリティ 16/16 ●

  • セキュリティに関する開発知識


    バッジには十分です！

    プロジェクトには、安全なソフトウェアを設計する方法を知っている少なくとも1人の主要な開発者が必要です。 （正確な要件については、「詳細」を参照してください。） [know_secure_design]
    これには、Saltzer and Schroeder の8つの原則を含む以下の設計原則を理解する必要があります。
    • メカニズムの経済性（たとえば、スイーピング シンプリフィケーションを採用して、メカニズムを実際的に単純化し小さくする）
    • フェイルセーフのデフォルト（アクセスの決定はデフォルトで拒否されるべきであり、プロジェクトのインストールはデフォルトで安全でなければならない）
    • 完全なメディエーション（制限されたすべてのアクセスは権限がチェックされ、バイパスされない）
    • オープンな設計（セキュリティメカニズムは攻撃者の設計に対する無知に依存するべきではなく、 簡単に保護ができて変更ができる鍵やパスワードのような情報に依存すべきです。
    • 特権の分離（理想的には、重要なオブジェクトへのアクセスは複数の条件に依存すべきで、1つの保護システムを破ることで完全なアクセスが可能にならないようにします。たとえば、パスワードとハードウェア トークンを必要とする多因子認証は単因子認証より強いです。
    • 最低限の権限（プロセスは最低限の権限で動作する必要がある）
    • 最低限の共通メカニズム（設計は、複数のユーザに共通のメカニズムや全てのユーザーに依存するメカニズムを最小限に抑えるべきです。）
    • 心理学的受容性（ヒューマンインタフェースは、使いやすく設計されていなければならない - 「驚きが最小限になる」という設計が助けになる）
    • 限られた攻撃面（攻撃面 - 攻撃者がデータを入力または抽出しようとする部分 - を制限する必要があります）
    • ホワイト リストで入力を検証します（入力は通常、この検証はブラックリスト（既知の不良値をリストする）ではなく、ホワイトリスト（既知の値のみを受け入れる）を使用する必要があります。
    プロジェクトの「主要な開発者」とは、プロジェクトのコードベースに精通していて、容易に変更を加えることができ、プロジェクトの他のほとんどの参加者によって認められている人です。主要な開発者は、通常、過去1年間に（コード、文書、または質問に回答して）多数の貢献を行います。ある開発者が、プロジェクトを開始している（3年以上プロジェクトから離れていない）、プライベート脆弱性報告チャネル（存在する場合）に関する情報を受け取る、プロジェクトを代表してコミットを受け入れる、最終リリースする、などを行う時主要な開発者とみなすことができます。開発者が1人だけの場合、その人物が主要開発者です。より安全なソフトウェアを開発し、設計について議論する方法を理解するのに役立つ多くの本やコースが利用可能です。 たとえば、 Secure Software Development Fundamentals コースは、3つのコースの無料セットです。 より安全なソフトウェアを開発する方法を説明しています。

    The members of the technical steering committee of the seL4 Foundation all satisfy this requirement (see https://sel4.systems/Foundation/TSC/index.html). Multiple of these teach secure operating systems at Universities, and/or have senior positions in companies that build secure software.


    バッジには十分です！

    プロジェクトの主要開発者の少なくとも1人は、この種のソフトウェアの脆弱性につながる一般的な種類のエラーを知っていなければならず、それぞれを対策または緩和する少なくとも1つの方法を知っていなければなりません。 [know_common_errors]
    例（ソフトウェアの種類によって異なります）には、SQLインジェクション、OSインジェクション、従来のバッファオーバーフロー、クロスサイトスクリプティング、認証の欠落、承認の欠落などがあります。一般的に使用されるリストについては、 CWE/SANSトップ25またはOWASPトップ10を参照してください。より安全なソフトウェアを開発する方法を理解し、脆弱性につながる一般的な実装エラーについて説明するのに役立つ多くの書籍やコースが用意されています。たとえば、 Secure Software Development Fundamentalsコースは、より安全なソフトウェアを開発する方法を説明する3つのコースの無料セットです（受講は無料です。追加料金を払うと、学習したことを証明する証明書を入手できます）。

    All members of the seL4 verification team, who produced mathematical code-level proofs (many of which are also developers) satisfy this requirement. All of the members of the technical steering committee of the seL4 Foundation also satisfy this requirement (see https://sel4.systems/Foundation/TSC/index.html).


  • 優良な暗号手法を使用する

    一部のソフトウェアは暗号化メカニズムを使用する必要がないことに注意してください。あなたのプロジェクトが作成するソフトウェアが、(1) 暗号化機能を含む、アクティブ化する、または有効化し、(2) 米国（US）から米国外または米国市民以外にリリースされる可能性がある場合は、法的に義務付けられた追加手順の実行を要求される可能性があります。通常、これにはメールの送信が含まれます。詳細については、 Understanding Open Source Technology & US Export Controls（「オープンソース技術と米国の輸出管理について」）の暗号化のセクションを参照してください。

    バッジには十分です！

    プロジェクトによって作成されたソフトウェアは、デフォルトで、一般に公開され、専門家によってレビューされている暗号プロトコルとアルゴリズムを使用しなければなりません。（暗号プロトコルとアルゴリズムが使用される場合） [crypto_published]
    ソフトウェアによっては暗号機能を直接使用する必要がないため、これらの暗号基準は常に適用されるわけではありません。

    seL4 does not use cryptographic mechanisms


    バッジには十分です！

    プロジェクトによって作成されたソフトウェアがアプリケーションまたはライブラリであり、主な目的が暗号の実装でない場合、暗号機能を実装するために特別に設計されたソフトウェアを呼び出すだけにするべきです。自分用に（暗号機能を）再実装するべきではありません。 [crypto_call]

    seL4 does not use cryptographic mechanisms


    バッジには十分です！

    暗号に依存するプロジェクトによって作成されるソフトウェアのすべての機能は、FLOSSを使用して実装可能でなければなりません。 [crypto_floss]
    オープン ソース イニシアチブによるオープン スタンダード要件を参照して下さい。

    seL4 does not use cryptographic mechanisms


    バッジには十分です！

    プロジェクトによって作成されたソフトウェア内にあるセキュリティ メカニズムは、少なくとも、2030年までのNIST最小要件（2012年）を満たすデフォルト鍵長を使用しなければなりません。より小さな鍵長を完全に無効になるおうに、ソフトウェアを構成できなければなりません。 [crypto_keylength]
    これらの最小ビット長は、対称鍵112、ファクタリング係数2048、離散対数鍵224、離散対数群2048、楕円曲線224、ハッシュ224（パスワードハッシュはこのビット長でカバーされません。パスワードハッシュに関する詳しい情報は crypto_password_storage 基準にあります）です。さまざまな機関が出している推奨鍵長の比較については、https://www.keylength.comを参照してください。ソフトウェアは、 いくつかの構成ではより短い鍵長を許可するかもしれません（これはダウングレード攻撃を許すので、理想的には正しくありません。しかし、短い鍵長は、相互運用性のために時に必要となります）。

    seL4 does not use cryptographic mechanisms


    バッジには十分です！

    プロジェクトによって生成されたソフトウェア内のデフォルトのセキュリティメカニズムは、壊れた暗号化アルゴリズム（MD4、MD5、シングルDES、RC4、Dual_EC_DRBGなど）に依存したり、実装する必要がない限り、コンテキストに不適切な暗号化モードを使用したりしてはなりません。相互運用可能なプロトコル（実装されたプロトコルがネットワークエコシステムによって広くサポートされている標準の最新バージョンであり、そのエコシステムではそのようなアルゴリズムまたはモードの使用が必要であり、そのエコシステムはこれ以上安全な代替手段を提供しません）。これらの壊れたアルゴリズムまたはモードが相互運用可能なプロトコルに必要な場合、ドキュメントには、関連するセキュリティリスクと既知の緩和策を記載する必要があります。 [crypto_working]
    ECBモードは、 ECBペンギンによって示されるように暗号文内の同一のブロックを明らかにするため、ほとんど適切ではありません。また、CTRモードは、認証を実行せず、入力状態が繰り返されると重複を引き起こすため、不適切なことがよくあります。多くの場合、Galois / Counter Mode（GCM）やEAXなど、機密性と認証を組み合わせるように設計されたブロック暗号アルゴリズム モードを選択するのが最善です。プロジェクトは、互換性のために必要な場合、ユーザーが壊れたメカニズムを有効にすることを許可する場合があります（構成中など）が、ユーザーはそれを実行していることを認識します。

    seL4 does not use cryptographic mechanisms


    バッジには十分です！

    プロジェクトによって作成されたソフトウェア内のデフォルトのセキュリティ メカニズムは、既知の重大な脆弱性を持つ暗号アルゴリズムやモード（たとえば、SHA-1暗号ハッシュ アルゴリズムまたはSSHのCBC モード）に依存するべきではありません。 [crypto_weaknesses]
    SSHのCBCモードに関する懸念事項は、 CERT: SSH CBC 脆弱性にて議論されています。.

    seL4 does not use cryptographic mechanisms


    バッジには十分です！

    プロジェクトによって作成されたソフトウェア内のセキュリティ メカニズムは、鍵合意プロトコルのための完全な順方向秘密を実装するべきなので、もし長期鍵が将来侵害された場合でも、長期鍵のセットから導出されるセッション鍵は侵害されません。 [crypto_pfs]

    seL4 does not use cryptographic mechanisms


    バッジには十分です！

    プロジェクトによって作成されたソフトウェアが外部ユーザーの認証用のパスワードの保存を引き起こす場合、パスワードは、キーストレッチ（反復）アルゴリズム（Argon2id、Bcrypt、Scrypt、PBKDF2など）を使用して、ユーザーごとのソルトで反復ハッシュとして保存される必要があります。OWASP Password Storage Cheat Sheetも参照してください）。 [crypto_password_storage]
    この基準は、ソフトウェアがサーバー側Webアプリケーションなどの外部ユーザーのパスワードを使用してユーザーの認証（別名インバウンド認証）を実施している場合にのみ適用されます。ソフトウェアが他のシステムへの認証用のパスワードを保存している場合（別名、アウトバウンド認証、たとえば、ソフトウェアが他のシステムのクライアントを実装している場合）、そのソフトウェアの少なくとも一部がハッシュされていないパスワードにアクセスできる必要があるため、適用されません。

    seL4 does not use cryptographic mechanisms


    バッジには十分です！

    プロジェクトによって作成されたソフトウェア内のセキュリティ メカニズムは、暗号学的にセキュアな乱数発生器を使用して、すべての暗号鍵とナンスを生成しなければなりません。暗号学的にセキュアでない発生器を使用してはいけません。 [crypto_random]
    暗号学的にセキュアな乱数発生器は、ハードウェアの乱数発生器でも、Hash_DRBG、HMAC_DRBG、 CTR_DRBG、Yarrow、Fortunaなどのアルゴリズムを使用する暗号学的にセキュアな疑似乱数発生器（CSPRNG）でもよいです。セキュアでない乱数発生器には、Javaのjava.util.RandomとJavaScriptのMath.randomがあります。

    seL4 does not use cryptographic mechanisms


  • MITM（man-in-the-middle：中間者）攻撃に対応できる安全な配信


    バッジには十分です！

    プロジェクトは、MITM攻撃に対抗する配信メカニズムを使用しなければならない。httpsまたはssh+scpを使用することは許容されます。 [delivery_mitm]
    さらに強力な仕組みは、デジタル署名されたパッケージでソフトウェアをリリースすることです。配布システムへの攻撃を緩和するからです。しかし、これは、署名の公開鍵が正当なものであることをユーザーが確信でき、かつユーザーが実際に署名をチェックする場合にのみ有効です。

    Assuming this is for software releases, the project uses https. Otherwise, N/A.


    バッジには十分です！

    暗号ハッシュ（たとえばSHA1SUM）は、http経由で運んではならず、暗号署名をチェックすることなしに使用してはいけません。 [delivery_unsigned]
    これらのハッシュは、送信中に変更することができます。

    Assuming this is for software releases, the project uses, the project uses GitHub's release mechanism and git hashes (the kernel is usually built from source for use).


  • 広く知られた脆弱性を修正


    バッジには十分です！

    60日を超えて公的に知られている中程度または重大度のパッチが適用されていない脆弱性は存在してはなりません。 [vulnerabilities_fixed_60_days]
    脆弱性は、プロジェクト自体によってパッチされ、リリースされなければなりません（パッチは他の場所で開発される可能性があります）。脆弱性が無料情報と共にCVE（共通脆弱性識別子）を持つとき（例えば、 National Vulnerability Database ）、またはプロジェクトに情報が伝えられ、その情報が（おそらくプロジェクトによって）一般に公開されたとき、脆弱性は一般に知られるようになります。Common Vulnerability Scoring System (CVSS)の定性的スコアが中程度以上であれば、脆弱性は中程度以上の深刻度とみなされます。CVSS のバージョン 2.0 から 3.1 では、これは CVSS のスコア 4.0 以上に相当します。プロジェクトは、広く利用されている脆弱性データベース（国家脆弱性データベースなど）で公開されているCVSSスコアを、そのデータベースで報告されている最新バージョンのCVSSを用いて使用することができます。代わりに、プロジェクトは、脆弱性が公表された時点で計算入力内容が公開されている場合には、脆弱性が公表された時点でのCVSSの最新版を用いて深刻度を計算することができます。注意：これは、ユーザーが最大60日間、世界中のすべての攻撃者に対して脆弱なままになる可能性があることを意味します。この基準は、責任ある開示の再起動でGoogleが推奨しているものよりも、はるかに簡単に満たすことができることが多いです。なぜなら、Googleはレポートが公開されていなくても、プロジェクトが通知された時点で60日間の期間が開始されることを推奨しているためです。また、このバッジの基準は、他の基準と同様に、個々のプロジェクトに適用されることにも注意してください。プロジェクトの中には、より大きな包括組織や大規模プロジェクトの一部であり、複数のレイヤーに分かれている場合もあります。また、多くのプロジェクトでは、複雑なサプライチェーンの一部として、他の組織やプロジェクトに成果を提供しています。個々のプロジェクトは、多くの場合、残りの部分をコントロールできませんが、個々のプロジェクトは、脆弱性パッチをタイムリーにリリースするための作業を行うことができます。そのため、私たちは個々のプロジェクトの対応時間に焦点を当てています。 一旦、個々のプロジェクトからパッチが利用可能になると、他のプロジェクトはそのパッチにどのように対処するかを決定することができます（たとえば、新しいバージョンにアップデートすることもできますし、選別されたソリューションのパッチだけを適用することもできます）。

    No such vulnerabilities are known.


    バッジには十分です！

    プロジェクトは、すべての重要な脆弱性を、報告された後迅速に修正するべきです。 [vulnerabilities_critical_fixed]

    No such vulnerabilities are known.


  • その他のセキュリティ上の課題


    バッジには十分です！

    公開リポジトリは、パブリックアクセスを制限するための有効なプライベートクレデンシャル（たとえば、有効なパスワードやプライベートキー）を漏らしてはなりません。 [no_leaked_credentials]
    プロジェクトは、パブリック アクセスを制限する意図がない限り、テスト用や重要でないデータベース用の「サンプル」資格情報を漏らす可能性があります。

    The project contains no private credentials.


 分析 8/8 ●

  • 静的コード解析


    バッジには十分です！

    選択した言語でこの基準を実装するFLOSSツールが少なくとも1つある場合、少なくとも1つの静的コード分析ツール（コンパイラの警告と「安全な」言語モード以外）を、ソフトウェアの主要な製品リリースの提案に、リリース前に適用する必要があります。 [static_analysis]
    静的コード解析ツールは、ソフトウェアコードを実行せずに特定の入力を用いて（ソースコード、中間コード、または実行可能ファイルとして）調べます。この基準のために、コンパイラの警告と「安全な」言語モードは、静的コード解析ツールとしてカウントされません（これらは通常、速度が重要なため深い解析を行いません）。このような静的コード解析ツールの例には、cppcheck (C, C++)、clang静的解析 (C, C++)、SpotBugs (Java)、FindBugs (Java) (FindSecurityBugsを含む)、PMD (Java)、Brakeman (Ruby on Rails)、lintr (R)、goodpractice (R), Coverity Quality Analyzer、SonarQube、 Codacyおよび HP Enterprise Fortify Static Code Analyzer.大きなツールのリストは、静的コード解析のためのWikipediaツール一覧, 静的コード解析に関するOWASP情報、 NISTソースコードセキュリティアナライザのリスト、およびウィーラーの静的解析ツール一覧などがあります。 使用する実装言語で使用できるFLOSS静的解析ツールがない場合は、「該当なし」（N/A）を選択します。

    The project does use static analysis such as Coverity, but its main static analysis is full machine-checked mathematical, code-level verification of C code base. This is the strongest form of static analysis possible, and subsumes dynamic analysis tools as well for this application. The proof scripts for seL4 are available at https://github.com/seL4/l4v together with instructions on how to check them separately. These proofs are run as part of CI.


    バッジには十分です！

    static_analysis基準に使用される静的解析ツールの少なくとも1つが、分析された言語または環境における共通の脆弱性を探すためのルールまたはアプローチを含むことが、推奨されています。 [static_analysis_common_vulnerabilities]
    一般的な脆弱性を探すために特別に設計された静的解析ツールは、それらを見つける可能性が高いです。つまり、静的ツールを使用すると、通常は問題を見つけるのに役立ちますので、利用を提案しますが、「合格」レベルのバッジには要求しません。

    The formal seL4 proofs cover all known common vulnerabilities such as buffer overflows, null pointer dereferences, etc. They do not (yet) cover timing side channels, but neither does any other common static analysis we are aware of.


    バッジには十分です！

    静的コード解析で発見された中程度および重大度の悪用可能な脆弱性はすべて、それらが確認された後、適時に修正されなくてはなりません。 [static_analysis_fixed]
    Common Vulnerability Scoring System (CVSS)の基本的な定性的なスコアが中程度以上であれば、脆弱性は中程度以上の深刻度とみなされます。CVSS のバージョン 2.0 から 3.1 では、これは CVSS のスコア 4.0 以上に相当します。プロジェクトは、広く利用されている脆弱性データベース（国家脆弱性データベースなど）で公開されているCVSSスコアを、そのデータベースで報告されている最新バージョンのCVSSを用いて使用することができます。また、脆弱性が公開された時点で計算入力が公開されている場合には、脆弱性が公開された時点でのCVSSの最新バージョンを用いて深刻度を計算することもできます。基準 vulnerabilities_fixed_60_days では、公開後 60 日以内にすべての脆弱性を修正することが要求されていることに注意してください。

    The formal proofs are part of CI and must pass before any code change is accepted into the kernel repository. The exception from this are experimental features that are marked as such, and unverified architecture ports, which are also marked as such.


    バッジには十分です！

    静的ソースコード解析は、コミットごと、または少なくとも毎日実行することをお勧めします。 [static_analysis_often]

    The proofs run on every commit.


  • 動的コード分析


    バッジには十分です！

    リリース前に、ソフトウェアの主要な製品リリースに少なくとも1つの動的解析ツールを適用することが示唆されています。 [dynamic_analysis]
    動的解析ツールは、ソフトウェアを特定の入力で実行して検査します。たとえば、プロジェクトは、ファジングツール（アメリカンファジーロップなど）やウェブ アプリケーション スキャナ（例： OWASP ZAP または w3af ）です。場合によっては、 OSS-Fuzz プロジェクトがプロジェクトにファズテストを適用する可能性があります。この基準のために、動的分析ツールは、様々な種類の問題を探すために何らかの方法で入力を変更するかまたは少なくとも80％のブランチ カバレッジを持つ自動テスト スイートである必要があります。 動的解析に関するWikipediaのページと ファジングに関するOWASPページで、いくつかの動的解析ツールを特定しています。解析ツールは、セキュリティの脆弱性を探すことに重点を置くことができますが、これは必須ではありません。

    The formal proofs subsume any errors that dynamic analysis tools can detect. In addition, the afl fuzzer has been run on kernel code that is not formally verified, e.g. experimental features and platform ports that are marked as unverified, but not for every release. Dynamic analysis in the form of runtime assertions for a full test suite (sel4test) is done for every commit (and release), including code that is not formally verified.


    バッジには十分です！

    プロジェクトで作成されたソフトウェアにメモリ安全でない言語（CやC ++など）を使用して作成されたソフトウェアが含まれている場合、少なくとも1つの動的ツール（たとえば、ファジーまたはウェブ アプリケーション スキャナ）を、バッファの上書きなどのメモリの安全性の問題を検出するメカニズムと一緒にいつも使用します。プロジェクトがメモリ安全でない言語で書かれたソフトウェアを作成しない場合は、「該当なし」（N/A）を選択します。 [dynamic_analysis_unsafe]
    メモリの安全性の問題を検出するメカニズムの例としては、アドレスサニタイザー（ASAN）（GCCおよびLLVMで利用可能）、 Memory Sanitizer 、および valgrind が含まれます。他に使用される可能性のあるツールには、スレッドサニタイザと定義されていない動作サニタイザを参照してください。広範なアサーションも機能します。

    The formal seL4 proofs guarantee the absence of any memory safety errors in C. Tests with assertions guard against potential memory safety issues such as object overlap in code that is experimental and/or not formally verified.


    バッジには十分です！

    プロジェクトでは、多くのアサーションを可能にする少なくとも一部の動的分析（テストやファジングなど）の構成を使用することをお勧めします。多くの場合、これらのアサーションは本番ビルドでは有効にしないでください。 [dynamic_analysis_enable_assertions]
    この基準は、本番環境でアサーションを有効にすることを示唆するものではありません。それは完全にプロジェクトとそのユーザーが決定することです。この基準の焦点は、展開前の動的分析中の障害検出を改善することです。プロダクション環境でのアサーションの有効化は、動的分析（テストなど）中にアサーションを有効にすることとはまったく異なります。場合によっては、プロダクション環境でアサーションを有効にすることは非常に賢明ではありません（特に高整合性コンポーネントの場合）。プロダクション環境でアサーションを有効にすることには多くの議論があります。たとえば、ライブラリは呼び出し元をクラッシュさせてはなりません。ライブラリが存在するとアプリストアによる拒否が発生する可能性があります。また、プロダクション環境でアサーションをアクティブにすると、秘密鍵などの秘密データが公開される可能性があります。多くのLinuxディストリビューションではNDEBUGが定義されていないため、これらのディストリビューションのプロダクション環境ではデフォルトで C/C++ assert() が有効になります。これらの環境でのプロダクション環境では、別のアサーションメカニズムを使用するか、 NDEBUGを定義することが重要です。

    Assertions are on for debug builds only and are used in development for new features or refactoring.


    バッジには十分です！

    動的コード分析で発見されたすべての中程度および重大度の悪用可能な脆弱性は、確認された後、適時に修正されなければなりません。 [dynamic_analysis_fixed]
    動的コード分析を実行しておらず、この方法で脆弱性が見つからない場合は、「該当なし」（N/A）を選択してください。 Common Vulnerability Scoring System (CVSS)の基本的な定性的スコアが中以上の場合、脆弱性は中程度以上の重大度と見なされます。 CVSSバージョン2.0から3.1では、これは4.0以上のCVSSスコアに相当します。プロジェクトは、広く使用されている脆弱性データベース（ National Vulnerability Databaseなど）で公開されているCVSSスコアを、そのデータベースで報告されている最新バージョンのCVSSを使用して使用できます。代わりに、脆弱性が公表された後に計算入力が公開された場合、プロジェクトは脆弱性の開示時に最新バージョンのCVSSを使用して重大度を自ら計算することができます。

    All issues detected during the formal proofs are fixed before pull requests are accepted. Any issues (security, correctness, or otherwise) on code that is experimental and/or not formally verified are fixed either before pull request are accepted, or if only discovered later, fixed as soon as possible. seL4 releases typically do not contain any known security issues.



このデータは、Creative Commons Attribution version 3.0以降のライセンス（CC-BY-3.0 +）のもとで利用できます。すべての人がデータを自由に共有および適応できますが、適切にクレジットを入れる必要があります。 Gerwin KleinとOpenSSFベストプラクティス バッジ貢献者のクレジットを入れてください。

プロジェクト バッジ登録の所有者： Gerwin Klein.
エントリの作成日時 2021-06-30 05:53:00 UTC、 最終更新日 2021-07-01 02:50:15 UTC 最後に2021-06-30 07:33:16 UTCにバッジ合格を達成しました。

もどる