Download seL4

Get the Current seL4 Source Release

seL4 is now open source — see the sel4.systems website.

 

Historical seL4 Binary Release

What am I downloading?

You are downloading a binary version of the seL4 microkernel, version 1.2, together with its formal specification, user-level libraries and sample code, and a para-virtualised Linux.

Where can I get help?

You can get help from the bundled reference manual, the abstract specification documents, and release notes.

Things to note

  • The proof applies to the seL4/ARM11 production (non-debug) version only. It proves functional correctness, not necessarily security.
  • The proof applies to the kernel code only, not to any of the provided user-level stubs, libraries, applications, or sample code.
  • Do not use this kernel in a safety critical system without understanding the proof, its assumptions, the specification, and system environment.
  • More information about the proof and its assumptions is available on the L4.verified page and research paper.

Updates

Last update on 2013-03-25 (see release notes or the more detailed changelog)

Please provide the following details

Name:
Email:
Company/Organisation:

End-User Licence Agreements

OPEN KERNEL LABS and National ICT Australia Limited (Licensors) NON-COMMERCIAL LICENSE AGREEMENT

This Non-Commercial License Agreement ("Agreement") is made by and between

Open Kernel Labs Inc ("OK"), and National ICT Australia Limited (ABN 62 102 206 173) ("NICTA") (together, for the purposes of this license and, subject to clause 2, to be known as the "LICENSOR") and you, the Licensee.

WHEREAS OK and NICTA respectively own the intellectual property rights in different components of software and other materials as listed in Schedule 1 to this License Agreement;

AND WHEREAS OK and NICTA have agreed between themselves, for the convenience of licensees, to make their respective components of software and related materials available for license to licensees from the same location and at the same time and together under the terms of this Non-commercial License Agreement.

NOW, THEREFORE, this Non-Commercial License Agreement applies to licensed materials identified in Schedule 1 and the associated documentation, both in the form made available to you hereunder ("Product").

1. Non-Commercial Use Only.

You acknowledge and agree that the Product is being licensed to you without charge in exchange for your agreeing to use the Product and any derivative works thereof ("Derivative Works") for a Non-Commercial Purpose only. "Non-Commercial Purpose" means solely for educational use, academic research, or internal testing and evaluation and excludes any commercial use of the Product or Derivative Works, including but not limited to, use for, as part of, or in connection with, any product (including software) or service that will be sold, offered for sale, licensed, leased, loaned, rented or otherwise made available commercially.

2. Limited License.

The terms of this Non-Commercial License Agreement apply in the following way:

a. OK is the Licensor solely of the OKL Components listed in Schedule 1
b. NICTA is the Licensor solely of the NICTA Components listed in Schedule 1.
c. "LICENSOR" refers to OK in respect of the OKL Components.
d. "LICENSOR" refers to NICTA in respect of the NICTA Components.
e. You obtain a separate and distinct license to the NICTA and OKL Components listed in Schedule from each of OK and NICTA, when you agree to the terms described in this Agreement.

Subject to your compliance with all the terms and conditions of this Agreement, LICENSOR grants you a limited, royalty-free, nonexclusive, nontransferable, non-sublicense-able, revocable license to copy and make derivative works of the Product, solely for a valid Non-Commercial Purpose. The Product is licensed with the following limitations and obligations:

f. No Reverse Engineering. You must comply with any technical limitations in the Product that only allow you to use it in certain ways and you may not decompile, decipher, disassemble, reverse engineer or otherwise attempt to access the source code of any 1 object code version of the Product, except as expressly permitted by applicable law notwithstanding this limitation.

g. No Rental or Transfer. You may not rent, lease, lend, sublicense, transfer, host for, or otherwise provide the Product or Derivative Works to any third party.

h. Proprietary Markings. You will not remove, alter or obscure any trademark, service mark, copyright, patent, trade secret, ownership or any other proprietary or intellectual property notices, legends, warnings, markings, or indications on or within any component of the Product. In addition to the requirements of the preceding sentence you will include the following legend on any Derivative Works: "This program contains a non-commercial version of certain software code or other information proprietary to NICTA and Open Kernel Labs, Inc. ("OK-NICTA Product"). The OK-NICTA Product is provided to you "AS-IS". YOU ASSUME TOTAL RESPONSIBILITY AND RISK FOR USE OF THE OK-NICTA PRODUCT."

i. No Open Source. This Agreement does not include any license, right, power or authority to, and are subject to the condition that you do not, subject LICENSOR's Intellectual Property Rights to any of the terms of an Open Source License. "Open Source License" means a license that requires as a condition of use, modification, or distribution of software subject to the license, that the software or other software combined or distributed with the software be (i) disclosed or distributed in source code form; (ii) licensed for the purpose of making derivative works; or (iii) redistributable at no charge. "Intellectual Property Right" means all intellectual property rights throughout the world, whether existing under intellectual property, unfair competition or trade secret laws, or under statute or at common law or equity, including but not limited to: (i) copyrights, trade secrets, trademarks, trade names, patents, inventions, designs, logos and trade dress, "moral rights," mask works, rights of personality, publicity or privacy, and any other intellectual property and proprietary rights; and (ii) any registration, application or right to apply for any of the rights referred to in this clause; and (iii) any and all renewals, extensions and restorations thereof, now or hereafter in force and effect.

3. Reservation of Rights and Ownership; Feedback.

The Product is protected by copyright and other intellectual property laws and treaties. Except for the limited rights granted to you in Section 2, LICENSOR reserves all right, title, and interest including but not limited to copyright, patent, trade secret, and all other Intellectual Property Rights, in and to the Product and the Derivative Works. You agree that LICENSOR does not, directly or by implication, by estoppel or otherwise, grant any other rights or licenses to you under this Agreement. If you inform LICENSOR of any errors, difficulties or other problems with the Product, or make any suggestions as to changes or modifications to the Product (collectively, "Feedback"), LICENSOR will have the right to use the Feedback for any purpose without compensation to you. All Feedback, including any and all patents, copyrights, trade secrets and any and all other proprietary rights in or derived from the Feedback, will be the sole property of LICENSOR.

4. Support of Product.

LICENSOR has no obligation to provide maintenance, technical or other support, or updates to you for the Product.

5. Confidentiality.

Other than provided for in Section 6 of this Agreement, you will not distribute or disclose the Product, Derivative Works, or any information obtained from use of the Product or Derivative Works (collectively, "Confidential Information") to any third party and will protect the Confidential Information from use by and disclosure to others using the same degree of care used to protect your own confidential or proprietary information, but in any case using no less than a reasonable degree of care. If you (i) are required by law to disclose Confidential Information per the advice of counsel, (ii) give LICENSOR notice of such requirement, and (iii) cooperate with LICENSOR in seeking arrangements with the party requiring such disclosure to protect the confidentiality of the Confidential Information, you may furnish only that minimal portion of the Confidential Information that is legally required. Confidential Information does not include any information that is generally known to the public without breach of this Agreement by you.

6. Limited Publication Rights.

You may not publish the Product or Derivative Works for others to copy. You will not publish any data, results or information obtained from use of the Product or Derivative Works without the prior written consent of LICENSOR. Such consent will not be unreasonably withheld.

7. Termination; Return of Product; Survival.

a. Termination. LICENSOR may terminate this agreement if you fail to comply with its terms and conditions, or for any reason by providing written notice to you at the address provided. In such event, any and all licenses granted to you under this Agreement immediately cease.

b. Return of Product. As soon as practicable following any termination or expiration of this Agreement (and in no event more than ten (10) business days thereafter), you agree, as may be requested by LICENSOR, to either return to LICENSOR or delete all copies of the Product and Derivative Works in your possession, custody, or control, including the original copy of the Product provided to you by LICENSOR, and including any copies of the Product or Derivative Works on magnetic media or computer systems or any written materials. Upon request by LICENSOR, you will certify your compliance with this Section 7(b) in writing.

c. Survival of Terms. The provisions of Sections 1, 3, 5, 6, 7(b), 7(c), and 8 through 14 will survive any termination or expiration of this Agreement.

8. DISCLAIMER OF WARRANTIES.

YOU ACKNOWLEDGE AND AGREE THAT, TO THE MAXIMUM EXTENT PERMITTED BY APPLICABLE LAW, THE PRODUCT IS PROVIDED AS IS, AND LICENSOR AND ITS SUPPLIERS HEREBY DISCLAIM ALL WARRANTIES AND CONDITIONS, WHETHER EXPRESS, IMPLIED OR STATUTORY, INCLUDING ANY IMPLIED WARRANTIES, DUTIES OR CONDITIONS OF MERCHANTABILITY, OR FITNESS FOR A PARTICULAR PURPOSE. ALSO THERE IS NO WARRANTY OR CONDITION OF TITLE, QUIET ENJOYMENT, QUIET POSSESSION, CORRESPONDENCE TO DESCRIPTION OR NON-INFRINGEMENT WITH REGARD TO THE PRODUCT, LACK OF VIRUSES OR BUGS, OR ACCURACY OR COMPLETENESS OF RESPONSES OR RESULTS. THE ENTIRE RISK ARISING OUT OF THE USE, PERFORMANCE, OR QUALITY OF THE PRODUCT REMAINS WITH YOU.

9.LIMITATION OF LIABILITY.

IN NO EVENT WILL LICENSOR BE LIABLE FOR ANY DAMAGES, WHETHER IN CONTRACT OR TORT (INCLUDING NEGLIGENCE), INCLUDING BUT NOT LIMITED TO DIRECT, CONSEQUENTIAL, SPECIAL, EXEMPLARY, INCIDENTAL, AND INDIRECT DAMAGES, ARISING OUT OF OR IN CONNECTION WITH THIS AGREEMENT OR THE USE, THE RESULTS OF USE, OR THE INABILITY TO USE THE PRODUCT, EVEN IF LICENSOR HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES. YOU AGREE THAT YOU HAVE THE SOLE RESPONSIBILITY FOR PROTECTING YOUR DATA, INCLUDING BY PERIODIC BACKUP OR OTHERWISE, USED IN CONNECTION WITH THE PRODUCT.

10. Indemnification.

You will indemnify and hold harmless LICENSOR, its subsidiary and parent entities, successors, affiliates, and assigns, and all of their respective officers, directors, members, shareholders, agents, and employees against any action, cause of action, suit, proceeding, claim, or demand of any third party (and all resulting judgments, bona fide settlements, penalties, damages, losses, liabilities, costs, and expenses (including without limitation reasonable attorneys' fees and costs) arising out of, or relating to, your use of the Product, except for use expressly permitted in this Agreement.

11. Export Law Assurances.

You will comply with all applicable international and national laws that apply to the Product, including the U.S. Export Administration Regulations, as well as end-user, end-use, and destination restrictions issued by U.S. or other governments.

12. Assignment.

You may not assign or otherwise transfer this Agreement or any rights or obligations hereunder, in whole or in part, whether by operation of law or otherwise, to any third party.

13. Applicable Law; Jurisdiction and Venue; Attorneys' Fees.

This Agreement will be governed by the laws of the State of Illinois, without regard to its conflict of laws principles. You hereby consent to the exclusive jurisdiction and venue of the state and federal courts located in Cook County, Illinois with respect to any claim arising under or by reason of this Agreement. If either party employs attorneys to enforce any rights arising out of or relating to this Agreement, the prevailing party will be entitled to recover its reasonable attorneys' fees, costs and other expenses.

14. Entire Agreement; No Waiver.

This Agreement constitutes the entire agreement between the parties and expressly supersedes any prior agreement, written or oral, between the parties on the subject matter hereof. No waiver of any provision of this Agreement will be effective unless it is in a signed writing, and no waiver will constitute a waiver of any other provision or of the same provision on another occasion. If a court of competent jurisdiction holds any term, covenant or restriction of this Agreement to be illegal, invalid, or unenforceable, in whole or in part, the remaining terms, covenants, and provisions will remain in full force and effect and will in no way be affected, impaired or invalidated.

SCHEDULE 1 to the Non-Commercial License Agreement.

The Product is:

OKL Components

seL4/ARM binary
seL4manual
seL4 abstract specification (in pdf and Isabelle)
seL4/x86 binary
In-kernel debugging stubs

NICTA Components

Linux booter and time server
user libraries (ARM and x86)
user examples (ARM and x86)

********************************************

Open Source Components

The Components are listed here for convenience, but they are not licensed to you under the terms of this Agreement. These Components are available under separate license terms, as indicated)
1. Elfloader (ARM bootloader) (OZPLB License)
2. Linux on seL4/x86 (paravirtualised Linux) (GPL License)

********************************************

99.65MiB, gzipped tarball

Served by Apache on Linux on seL4