seL4

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

これがあなたのプロジェクトなら、あなたのプロジェクトページにあなたのバッジステータスを表示してください!バッジステータスは次のようになります。 プロジェクト 5003 のバッジ レベルは silver です バッジステータスの埋め込み方法は次のとおりです。

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

        

 基本的情報 13/13

  • 識別情報

    The seL4 microkernel

    どのようなプログラミング言語を使ってプロジェクトを実装していますか?
  • 基本的なプロジェクト ウェブサイトのコンテンツ


    プロジェクトのウェブサイトは、ソフトウェアが何をするのか(何の問題を解決するのか)を簡潔に記述しなければなりません。 [description_good]

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

    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ライセンス

    プロジェクトのライセンスはどのようなものですか?



    プロジェクトによって作成されたソフトウェアは、FLOSSとしてリリースされなければなりません。 [floss_license]

    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]

    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]
  • ドキュメンテーション


    プロジェクトは、プロジェクトによって作成されたソフトウェアに関する基本的なドキュメンテーションを提供しなければなりません。 [documentation_basics]

    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]

    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]

    Given only https: URLs.



    プロジェクトは、議論(提案された変更や問題を含む)のための1つ以上の検索可能なメカニズムを持たなければならず、メッセージやトピックがURLでアドレス指定され、新しい人々がディスカッションのいくつかに参加できるようにしなければならず、クライアント側でプロプライエタリなソフトウェアのインストールを必要としないようにします。 [discussion]

    GitHub supports discussions on issues and pull requests.



    プロジェクトは英語で文書を提供し、英語でコードに関するバグ報告とコメントを受け入れることができるべきです。 [english]

    The main project language is English



    プロジェクトはメンテナンスされている必要があります。 [maintained]

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



(詳細)このバッジエントリを編集する権限を持つユーザーは? 現在:[]



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


    プロジェクトには、公開され、URLを持つ、バージョン管理のソース リポジトリがなければなりません。 [repo_public]

    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]

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


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


    プロジェクトの結果には、ユーザーが使用することを意図されたリリースごとに固有のバージョン識別子が必要です。 [version_unique]

    seL4 uses semantic versioning



    リリースには、Semantic Versioning (SemVer)またはCalendar Versioning (CalVer)のバージョン番号形式を使用することが推奨されます。CalVerを使用する場合は、マイクロレベル値を含めることが推奨されます。 [version_semver]


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

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


  • リリースノート


    プロジェクトは、各リリースにおいて、ユーザーがアップグレードすべきかどうか、また、アップグレードの影響を判断できるよう、そのリリースの主要な変更の要約を説明したリリースノートを提供しなければなりません(MUST)。リリースノートは、バージョン管理ログの生の出力であってはなりません(例えば、 "git log"コマンドの結果はリリースノートではない)。プロジェクトの成果物が複数の場所で再利用されることを意図していないプロジェクト(単独のウェブサイトやサービスのためのソフトウェアなど)で、かつ、継続的・断続的な配布を行う場合は、「該当なし」を選択することができます。 (URLが必要です) [release_notes]

    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]

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


  • バグ報告プロセス


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

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

    このプロジェクトは、過去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]

    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]

    プライベート脆弱性報告がサポートされている場合、プロジェクトは、プライベートに保持された方法で情報を送信する方法を含んでいなくてはなりません。 (URLが必要です) [vulnerability_report_private]

    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]

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


  • 作業ビルドシステム


    プロジェクトによって作成されたソフトウェアを利用するためにビルドが必要な場合、プロジェクトは、ソース コードからソフトウェアを自動的にリビルドできる作業ビルド システムを提供しなければなりません。 [build]

    The project uses CMake



    ソフトウエアをビルドするために、一般的なツールを使用することをお勧めします。 [build_common_tools]

    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]

    テスト スイートは、その言語の標準的な方法で呼び出すことができるべきです。 [test_invocation]

    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]
  • 警告フラグ


    プロジェクトは、選択した言語でこの基準を実装することができる少なくとも1つのFLOSSツールがあれば、1つまたは複数のコンパイラ警告フラグ、「安全」言語モードを使用可能にするか、分離 「リンター」ツールを使用してコード品質エラーまたは共通の単純なミスを検索しなければなりません。 [warnings]

    プロジェクトは警告を出さなければならない。 [warnings_fixed]

    All compiler warnings are addressed (running on -Werror)



    プロジェクトによって作成されたソフトウェアにある警告に、実際的な場合には、最大限に厳格になることを推奨されています。 [warnings_strict]
  • セキュリティに関する開発知識


    プロジェクトには、安全なソフトウェアを設計する方法を知っている少なくとも1人の主要な開発者が必要です。 (正確な要件については、「詳細」を参照してください。) [know_secure_design]

    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]

    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]

    seL4 does not use cryptographic mechanisms



    プロジェクトによって生成されたソフトウェア内のデフォルトのセキュリティメカニズムは、壊れた暗号化アルゴリズム(MD4、MD5、シングルDES、RC4、Dual_EC_DRBGなど)に依存したり、実装する必要がない限り、コンテキストに不適切な暗号化モードを使用したりしてはなりません。相互運用可能なプロトコル(実装されたプロトコルがネットワークエコシステムによって広くサポートされている標準の最新バージョンであり、そのエコシステムではそのようなアルゴリズムまたはモードの使用が必要であり、そのエコシステムはこれ以上安全な代替手段を提供しません)。これらの壊れたアルゴリズムまたはモードが相互運用可能なプロトコルに必要な場合、ドキュメントには、関連するセキュリティリスクと既知の緩和策を記載する必要があります。 [crypto_working]

    seL4 does not use cryptographic mechanisms



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

    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]

    seL4 does not use cryptographic mechanisms



    プロジェクトによって作成されたソフトウェア内のセキュリティ メカニズムは、暗号学的にセキュアな乱数発生器を使用して、すべての暗号鍵とナンスを生成しなければなりません。暗号学的にセキュアでない発生器を使用してはいけません。 [crypto_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]

    No such vulnerabilities are known.



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

    No such vulnerabilities are known.


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


    公開リポジトリは、パブリックアクセスを制限するための有効なプライベートクレデンシャル(たとえば、有効なパスワードやプライベートキー)を漏らしてはなりません。 [no_leaked_credentials]

    The project contains no private credentials.


  • 静的コード解析


    選択した言語でこの基準を実装するFLOSSツールが少なくとも1つある場合、少なくとも1つの静的コード分析ツール(コンパイラの警告と「安全な」言語モード以外)を、ソフトウェアの主要な製品リリースの提案に、リリース前に適用する必要があります。 [static_analysis]

    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]

    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]

    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]

    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]

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



    動的コード分析で発見されたすべての中程度および重大度の悪用可能な脆弱性は、確認された後、適時に修正されなければなりません。 [dynamic_analysis_fixed]

    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にバッジ合格を達成しました。

もどる