seL4

遵循以下最佳实践的项目将能够自愿的自我认证，并显示他们已经实现了核心基础设施计划（OpenSSF）徽章。

如果这是您的项目，请在您的项目页面上显示您的徽章状态！徽章状态如下所示： 项目5003的徽章级别为silver 这里是如何嵌入它：

这些是黄金级别条款。您还可以查看通过或白银级别条款。

        

 基本 5/5 ●

  • 识别

    The seL4 microkernel

  • 先决条件


    足够获得徽章！

    该项目必须拥有银级徽章。 [achieve_silver]

  • 项目监督


    足够获得徽章！

    项目必须具有2个或更多的“公交车因子”。 (需要网址) [bus_factor]

    For each main skill the bus factor in the technical steering committee is at least 3 https://sel4.systems/Foundation/TSC/.


    足够获得徽章！

    该项目必须至少有两个不相关的重要贡献者。 (需要网址) [contributors_unassociated]

    Interpreting this as "unassociated with the Trustworthy Systems group" (who developed the kernel). Of the technical steering committee https://sel4.systems/Foundation/TSC/index.html, currently 5 people are members of other companies or organisations.


  • 其他


    足够获得徽章！

    项目必须在每个源文件中包含许可证声明。这可以通过在每个文件开头附近的注释中加入以下内容来实现： SPDX-License-Identifier: [SPDX license expression for project]。 [license_per_file]

    The project uses SPDX license headers and copyright information. Checked by CI.


  • 公开的版本控制的源代码存储库


    足够获得徽章！

    必须使用通用的分布式版本控制软件（例如，git，mercurial）作为项目的源代码存储库。 [repo_distributed]

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


    足够获得徽章！

    该项目必须清楚地识别新的或临时贡献者可以执行的小型任务。 (需要网址) [small_tasks]

    Uses the issue badges "help wanted" and "good-first-issue" https://github.com/seL4/seL4/labels


    未知的所需信息，不足以用于徽章。

    项目必须要求开发人员使用双因素身份验证（2FA）来更改中央存储库或访问敏感数据（如私密漏洞报告）。这种2FA机制可以使用没有密码学机制的方案，如SMS（短消息），尽管不推荐。 [require_2FA]

    The project uses 2FA on GitHub


    勉强够获得徽章。

    项目的双因素身份认证（2FA）应该使用加密机制来防止仿冒。基于短消息服务（SMS）的2FA本身不符合此标准，因为它不被加密。 [secure_2FA]

    The project uses GitHub which allows SMS verification.


  • 编码标准


    足够获得徽章！

    该项目必须记录其代码检视需求，包括代码检视是如何进行的，必须检查的内容以及哪些是可接纳的内容。 (需要网址) [code_review_standards]

    See https://docs.sel4.systems/processes/code-review.html


    足够获得徽章！

    该项目必须至少有50％的修改（作者之外的人提出的）在发布之前审查，以确定是否是一个有价值的修改，并且没有已知的问题，会反对其包含 [two_person_review]

    All changes require review, see https://docs.sel4.systems/processes/code-review.html


  • 可工作的构建系统


    未知的所需信息，不足以用于徽章。

    该项目必须具有可重复构建。如果没有发生构建（例如，直接使用源代码而不是编译的脚本语言），请选择“不适用”（N/A）。 (需要网址) [build_reproducible]

    The build system produces the same binaries for the same source input. See https://docs.sel4.systems/GettingStarted#running-sel4 for build instructions and https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles for docker images based on Debian snapshot to ensure reproducible tool chain versions.


  • 自动测试套件


    足够获得徽章！

    测试套件必须以该语言的标准方式进行调用。 (需要网址) [test_invocation]

    The test suite uses a standard init, compile, run cycle. See e.g. https://docs.sel4.systems/GettingStarted.html#running-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.


    足够获得徽章！

    如果有至少一个FLOSS工具可以以所选语言度量此条款，该项目的FLOSS自动测试套件必须具有至少90％语句覆盖率。 [test_statement_coverage90]

    The formal proofs subsume test coverage)


    足够获得徽章！

    如果有至少一个FLOSS工具可以以所选语言度量此条款，该项目的FLOSS自动测试套件必须具有至少80％分支覆盖率。 [test_branch_coverage80]

    The formal proofs subsume test coverage


  • 使用基础的良好加密实践

    请注意，某些软件不需要使用加密机制。

    足够获得徽章！

    项目生成的软件必须支持所有网络通信的安全协议，如SSHv2或更高版本，TLS1.2或更高版本（HTTPS），IPsec，SFTP和SNMPv3。默认情况下，FTP，HTTP，Telnet，SSLv3或更早版本以及SSHv1等不安全协议必须被禁用，只有在用户专门配置时才启用。如果项目生成的软件不支持网络通信，请选择“不适用”（N/A）。 [crypto_used_network]

    seL4 does not use cryptographic mechanisms


    足够获得徽章！

    由项目生成的软件必须，如果支持或使用TLS，至少支持TLS版本1.2。请注意，TLS的前身称为SSL。如果软件不使用TLS，请选择“不适用”（N/A）。 [crypto_tls12]

    seL4 does not use cryptographic mechanisms


  • 安全交付防御中间人（MITM）的攻击


    足够获得徽章！

    项目网站，存储库（如果可通过网络访问）和下载站点（如果单独）必须包括具有非允许值的密钥加固头。 (需要网址) [hardened_site]

    https://sel4.systems and https://github.com/seL4/seL4 both have key hardening headers.


  • 其他安全问题


    足够获得徽章！

    该项目必须在过去5年内进行安全审查。此审查必须考虑安全需求和安全边界。 [security_review]

    seL4 has constant security review in the form of full formal, mathematical proofs that are continuously kept in sync with the code


    足够获得徽章！

    加固机制必须用于项目生产的软件，以便软件缺陷不太可能导致安全漏洞。 (需要网址) [hardening]

    The main hardening mechanism in seL4 are the formal proofs, see https://github.com/seL4/l4v, but compiler flags to eliminate undefined behaviour are on by default as well.


  • 动态代码分析


    足够获得徽章！

    必须在发布之前，至少将一个动态分析工具应用于软件任何候选发布的主要生产版本。 [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.


    足够获得徽章！

    项目应该在其生成的软件中包含许多运行时断言，并在动态分析期间检查这些断言。 [dynamic_analysis_enable_assertions]

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



此数据在知识共享署名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 获得通过徽章。

后退