1<!-- 2 Copyright 2021, Data61, CSIRO (ABN 41 687 119 230) 3 4 SPDX-License-Identifier: CC-BY-SA-4.0 5--> 6 7# Vulnerability disclosure policy 8 9Security is a core value of the seL4 Foundation. If you believe you have 10found a security vulnerability in seL4, we ask you to work with us to 11resolve it according to principles of responsible disclosure. This 12policy outlines what we ask of you, and what you can expect of us. 13 14## Scope 15 16This policy currently applies to the most recent released versions, and 17the heads of the default branches of the software in the following seL4 18Foundation repositories: 19- https://github.com/seL4/seL4 20- https://github.com/seL4/capdl 21- https://github.com/seL4/camkes-tool 22 23Note that these repositories include various code generation tools, for 24example the seL4 [bitfield generator], the [capDL-tool] and the 25[camkes-tool]. This policy applies to the code these tools ultimately 26generate, but not to the code generators themselves. In other words, 27it's the code that ends up running on seL4-based systems that we care 28about. 29 30[bitfield generator]: https://github.com/seL4/seL4/blob/master/tools/bitfield_gen.py 31[capDL-tool]: https://github.com/seL4/capdl/tree/master/capDL-tool 32[camkes-tool]: https://github.com/seL4/camkes-tool 33 34## What we ask of you 35 36- Report any vulnerabilities you discover as soon as you can, using the 37 official channel below. 38- Provide enough detail to allow us to understand the vulnerability and 39 its impact. 40- Be patient with us if we have questions. 41- Allow us reasonable time to fix the vulnerability before you disclose 42 it publicly. 43- Be mindful that updating the proofs for a fix might take longer than 44 you imagine. 45- Avoid violating the privacy of others, disrupting the normal operation 46 of our systems, or destroying data. 47 48## What you can expect of us 49 50- We will respond to your report within 14 days, and usually sooner. 51- We will work with you to understand and reproduce the vulnerability 52 you are reporting. 53- We will try to reach agreement on an appropriate timeframe for fixing 54 the vulnerability. We will usually aim for 90 days, but sometimes we 55 will need significantly longer to complete difficult proofs. 56- We will work to fix the vulnerability in a timely manner, and will 57 keep you informed of our progress. 58- When we have developed a fix, we will publicly acknowledge the 59 vulnerability. 60- If you agree, we will publicly acknowledge your role in finding and 61 helping us fix the vulnerability. 62- We will protect your privacy, and will not disclose your personally 63 identifying information to third parties without your explicit 64 permission. 65 66Unfortunately, we are not currently able to offer bug bounties. 67 68## Official channel 69 70Please send vulnerability reports by email to security@seL4.systems, 71optionally encrypted using our security officer's [OpenPGP key]. 72 73[OpenPGP key]: https://seL4.systems/security.asc 74 75## FAQ 76 77### How can formally verified software contain security vulnerabilities? 78 79seL4 supports many configurations, and only some of these are verified. 80For unverified configurations, we want to know about vulnerabilities, so 81we can provide the level of support that you would expect from any 82well-engineered software. 83 84Even verified configurations contain some code that is assumed to do the 85right thing, including boot code, assembly stubs, and cache management. 86If that code does the wrong thing, there might be a security 87vulnerability in a verified configuration, and we want to know about 88that. 89 90The proofs also make a number of assumptions about the way hardware 91works. If our assumptions are not valid for real hardware, there might 92be a security vulnerability, and we want to know so we can try to fix 93our assumptions. Some assumptions might not be possible to fix. For 94example, the assumption that memory is incorruptible may be violated by 95Rowhammer, but it is quite fundamental to the proofs. 96 97For more information about what the proofs mean, see the [seL4 FAQ]. 98 99[seL4 FAQ]: https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html 100