seL4

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

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

The project repository includes the entire development history between releases.

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

seL4 uses semantic versioning

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

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

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

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

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

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

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

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).

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

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

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

The project uses CMake

CMake is commonly used.

All build tools needed for seL4 are FLOSS tools.

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

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

The sel4test suite covers most (but not all) of the branches of 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 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

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).

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

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

All compiler warnings are addressed (running on -Werror)

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

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.

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).

seL4 does not use cryptographic mechanisms

seL4 does not use cryptographic mechanisms

seL4 does not use cryptographic mechanisms

seL4 does not use cryptographic mechanisms

seL4 does not use cryptographic mechanisms

seL4 does not use cryptographic mechanisms

seL4 does not use cryptographic mechanisms

seL4 does not use cryptographic mechanisms

seL4 does not use cryptographic mechanisms

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

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).

No such vulnerabilities are known.

No such vulnerabilities are known.

The project contains no private credentials.

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.

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.

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.

The proofs run on every commit.

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.

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.

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

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.