The Linux Foundation has registered seL4® as a trademark in the United States and other countries. Please use ® with the first mention of seL4 in all materials. In addition to the guidelines below, the Linux Foundation Trademark Usage Guidelines, available at www.linuxfoundation.org/trademark-usage, also apply to any use of the seL4 trademarks and logos.
The usage guidelines at www.linuxfoundation.org/trademark-usage apply to the seL4 mark and logos. In addition:
Do not modify the seL4 trademark or logos, e.g., do not add other characters, or change the colors, orientation or any other visual aspect of any logos.
Do not use the seL4 trademark in a misleading way. This includes:
Do not use the seL4 mark to refer to code that is modified in any way from the repository at http://github.com/seL4/seL4.
You may use the seL4 mark to refer to the seL4 microkernel, the seL4 Foundation, or the seL4 proofs if you use them accurately. The seL4 microkernel refers to the code hosted at https://github.com/seL4/seL4. The seL4 proofs refer to the formal mathematical proofs hosted at https://github.com/seL4/l4v.
For any modified versions make clear it is a modification of seL4, not seL4 itself; for academic research modifications you may use the term experimental seL4.
Cloning the repository, working on features, modifications, evaluations, research, etc, and referring to these is fine and encouraged. The purpose of the restriction is to ensure clarity and consistency on what the mark refers to. When referring to modifications and work-in-progress on the seL4 kernel, the name seL4 should refer to the official seL4 code from the foundation repository. Therefore examples of incorrect use are:
company Y’s seL4 with feature X
enhanced seL4 with feature X
Examples of correct use are (where accurate):
feature X by company Y is under review for inclusion into the seL4 kernel
feature X developed by company Y is under review to be included in the next release of the seL4 kernel
feature X by company Y is on the roadmap to be included in the seL4 kernel
company Y has developed a modification X to the seL4 kernel and has evaluated its performance/impact/benefits.
company Y is working on feature X to be included in the seL4 kernel
The important difference between xyz seL4 and a modification to seL4 is that in the former (incorrect) use the mark refers to the modified version, and in the latter (correct) use the mark refers to the code in the foundation repository.
For use in academic research publications only, the foundation allows the use of the forms experimental seL4 and experimental version of seL4 for referring to modifications to the seL4 code that are experimental research code. The form is explicitly meant for modifications that are not ready for commercial use, and not checked or endorsed by the foundation. An example of correct such use in a research paper would be “running on an experimental version of seL4 that supports feature X”.
Do not use the seL4 mark to make misleading claims about the strength and completeness of its formal verification. In particular, do not claim configurations of seL4 to be formally verified when they are not, and do not claim properties to be verified that are not. See the source code repository for which configurations are verified. If unsure, contact email@example.com. We will be happy to review and help phrase formal verification claims.
You may only make use of formal verification claims of seL4 in relation with your product if your product actually uses a verified configuration of seL4.
Do not add your company logo(s) to seL4 Foundation training and marketing materials, such as official presentations, unless expressly permitted to do so by the seL4 Foundation.
Do not create marketing or training materials that look like they come from the seL4 Foundation rather than your company.
Do not present the seL4 logos or marks larger than your own company’s logo(s).
For many libraries and language bindings it makes sense to include the seL4 mark in the name of your project.
You may do so in the following forms. Do use a capital L in seL4:
Do not use e.g. seL4-<project> or seL4-<language>-bindings.
If for some reason a different form is preferable, this can often be accommodated. To use such a different form, obtain written permission from firstname.lastname@example.org.
If your project is a generally useful part of the ecosystem of components, libraries, and frameworks around the seL4 kernel, consider hosting it under the seL4 Foundation GitHub organisation at github.com/seL4. Contact one of the members of the TSC of the foundation if you would like to do so with a description of the project, its current state and plans for the future.
Projects and repositories hosted under the seL4 Foundation GitHub organisation may use the seL4 mark more freely in their name.
We look to our community to help us retain the value of the seL4 trademark and promote the seL4 brand.
If you have questions about these guidelines or would like to report concerns regarding the use or misuse of the seL4 trademark, or to obtain written permission for a proposed use, please contact email@example.com.
The seL4 Foundation and/or Linux Foundation may release new versions of the seL4 trademark guidelines or The Linux Foundation Trademark Usage Guidelines from time to time.