seL4

Projects that follow the best practices below can voluntarily self-certify and show that they've achieved an Open Source Security Foundation (OpenSSF) best practices badge.

If this is your project, please show your badge status on your project page! The badge status looks like this:

Badge level for project 5003 is silver

Here is how to embed it:

You can show your badge status by embedding this in your markdown file:

[![OpenSSF Best Practices](https://www.bestpractices.dev/projects/5003/badge)](https://www.bestpractices.dev/projects/5003)

or by embedding this in your HTML:
<a href="https://www.bestpractices.dev/projects/5003"><img src="https://www.bestpractices.dev/projects/5003/badge"></a>

These are the

level criteria. You can also view the

or

level criteria.

Analysis 2/2 ●

Dynamic code analysis

Criterion [dynamic_analysis]
Met

Unmet

N/A

?

The project MUST apply at least one dynamic analysis tool to any proposed major production release of the software produced by the project before its release. ^{[dynamic_analysis]}
A dynamic analysis tool examines the software by executing it with specific inputs. For example, the project MAY use a fuzzing tool (e.g., American Fuzzy Lop) or a web application scanner (e.g., OWASP ZAP or w3af). In some cases the OSS-Fuzz project may be willing to apply fuzz testing to your project. For purposes of this criterion the dynamic analysis tool needs to vary the inputs in some way to look for various kinds of problems or be an automated test suite with at least 80% branch coverage. The Wikipedia page on dynamic analysis and the OWASP page on fuzzing identify some dynamic analysis tools. The analysis tool(s) MAY be focused on looking for security vulnerabilities, but this is not required.

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.

Criterion [dynamic_analysis_enable_assertions]
Met

Unmet

N/A

?

The project SHOULD include many run-time assertions in the software it produces and check those assertions during dynamic analysis. ^{[dynamic_analysis_enable_assertions]}
This criterion does not suggest enabling assertions during production; that is entirely up to the project and its users to decide. This criterion's focus is instead to improve fault detection during dynamic analysis before deployment. Enabling assertions in production use is completely different from enabling assertions during dynamic analysis (such as testing). In some cases enabling assertions in production use is extremely unwise (especially in high-integrity components). There are many arguments against enabling assertions in production, e.g., libraries should not crash callers, their presence may cause rejection by app stores, and/or activating an assertion in production may expose private data such as private keys. Beware that in many Linux distributions NDEBUG is not defined, so C/C++ assert() will by default be enabled for production in those environments. It may be important to use a different assertion mechanism or defining NDEBUG for production in those environments.

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

This data is available under the Creative Commons Attribution version 3.0 or later license (CC-BY-3.0+). All are free to share and adapt the data, but must give appropriate credit. Please credit Gerwin Klein and the OpenSSF Best Practices badge contributors.

Project badge entry owned by: Gerwin Klein.
Entry created on 2021-06-30 05:53:00 UTC, last updated on 2021-07-01 02:50:15 UTC. Last achieved passing badge on 2021-06-30 07:33:16 UTC.