Security is a core value of the seL4 Foundation. If you believe you have found a security vulnerability in seL4, we ask you to work with us to resolve it according to principles of responsible disclosure. This policy outlines what we ask of you, and what you can expect of us.
This policy currently applies to the most recent released versions, and the heads of the default branches of the software in the following seL4 Foundation repositories:
Note that these repositories include various code generation tools, for example the seL4 bitfield generator, the capDL-tool and the camkes-tool. This policy applies to the code these tools ultimately generate, but not to the code generators themselves. In other words, it's the code that ends up running on seL4-based systems that we care about.
- Report any vulnerabilities you discover as soon as you can, using the official channel below.
- Provide enough detail to allow us to understand the vulnerability and its impact.
- Be patient with us if we have questions.
- Allow us reasonable time to fix the vulnerability before you disclose it publicly.
- Be mindful that updating the proofs for a fix might take longer than you imagine.
- Avoid violating the privacy of others, disrupting the normal operation of our systems, or destroying data.
- We will respond to your report within 14 days, and usually sooner.
- We will work with you to understand and reproduce the vulnerability you are reporting.
- We will try to reach agreement on an appropriate timeframe for fixing the vulnerability. We will usually aim for 90 days, but sometimes we will need significantly longer to complete difficult proofs.
- We will work to fix the vulnerability in a timely manner, and will keep you informed of our progress.
- When we have developed a fix, we will publicly acknowledge the vulnerability.
- If you agree, we will publicly acknowledge your role in finding and helping us fix the vulnerability.
- We will protect your privacy, and will not disclose your personally identifying information to third parties without your explicit permission.
Unfortunately, we are not currently able to offer bug bounties.
Please send vulnerability reports by email to [email protected], optionally encrypted using our security officer's OpenPGP key.
seL4 supports many configurations, and only some of these are verified. For unverified configurations, we want to know about vulnerabilities, so we can provide the level of support that you would expect from any well-engineered software.
Even verified configurations contain some code that is assumed to do the right thing, including boot code, assembly stubs, and cache management. If that code does the wrong thing, there might be a security vulnerability in a verified configuration, and we want to know about that.
The proofs also make a number of assumptions about the way hardware works. If our assumptions are not valid for real hardware, there might be a security vulnerability, and we want to know so we can try to fix our assumptions. Some assumptions might not be possible to fix. For example, the assumption that memory is incorruptible may be violated by Rowhammer, but it is quite fundamental to the proofs.
For more information about what the proofs mean, see the seL4 FAQ.