遵循以下最佳实践的项目将能够自愿的自我认证,并显示他们已经实现了核心基础设施计划(OpenSSF)徽章。 显示详细资料
[](https://www.bestpractices.dev/projects/5003)
<a href="https://www.bestpractices.dev/projects/5003"><img src="https://www.bestpractices.dev/projects/5003/badge"></a>
The seL4 microkernel
For each main skill the bus factor in the technical steering committee is at least 3 https://sel4.systems/Foundation/TSC/.
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.
The project uses SPDX license headers and copyright information. Checked by CI.
Repository on GitHub, which uses git. git is distributed.
Uses the issue badges "help wanted" and "good-first-issue" https://github.com/seL4/seL4/labels
The project uses 2FA on GitHub
The project uses GitHub which allows SMS verification.
See https://docs.sel4.systems/processes/code-review.html
All changes require review, see https://docs.sel4.systems/processes/code-review.html
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.
The test suite uses a standard init, compile, run cycle. See e.g. https://docs.sel4.systems/GettingStarted.html#running-sel4
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.
The formal proofs subsume test coverage)
The formal proofs subsume test coverage
seL4 does not use cryptographic mechanisms
https://sel4.systems and https://github.com/seL4/seL4 both have key hardening headers.
seL4 has constant security review in the form of full formal, mathematical proofs that are continuously kept in sync with the code
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.
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.
Assertions are on for debug builds only and are used in development for new features or refactoring.
后退