secc
/
seL4-docs
mirror of https://github.com/seL4/docs.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
seL4-docs/GettingStarted.md

6.0 KiB
Raw Permalink Blame History

toc layout SPDX-License-Identifier SPDX-FileCopyrightText
true api CC-BY-SA-4.0 2020 seL4 Project a Series of LF Projects, LLC.

Getting Started

This page is a quick start for working with seL4 and its ecosystem.

Background and terminology

Sources

Code and proofs are available on GitHub, under standard open-source licenses.

There are many repositories. Of the most significant are:

  • l4v the seL4 proofs
  • seL4 the seL4 kernel

Projects

The seL4 kernel is built as part of project. Each project has a README.md associated with it which provides further information.

While the kernel is normally built as part of a project it is also possible create a standalone build.

Projects are a collection of git repositories, with versions managed by Android's Repo tool. Each project consists of an XML manifest file which specifies the source dependencies, and directory structure of a project. See the RepoCheatsheet page for a quick explanation of how we use Repo and some common commands.

A subset of available projects are described below, for a full list see the list of released projects:

  • verification, the seL4 proofs.
  • seL4test, a test suite for seL4, including a Library OS layer.
  • seL4bench, a microbenchmarking suite for seL4.
  • CAmkES, a component architecture for embedded systems based on seL4. See the CAmkES pages for more documentation about CAmkES.
  • x86 Camkes VMM a component-based virtual machine monitor for ia32 platforms using Intel VT-X and VT-D extensions.

Hardware and Target Platforms

Read the Hardware pages to see a list of supported platforms, and special instructions for particular hardware platforms.

Verification Targets and Claims

The seL4 kernel has a number of verified properties on a selection of configured hardware platforms. These configurations are also referred to as verification platforms (e.g. ARM_HYP). Read Verified Configurations to see which proofs are available for which platform and how to make use of these configurations.

Note: verification claims are limited to specific properties of seL4 on specifically configured platforms. These claims do not automatically transfer to other platforms, other seL4 configurations, or custom seL4 versions. Please consult Frequently Asked Questions, as well as the proof and assumptions page for a better understanding of the intersection of verification and seL4.

Setting up your machine

Read the Host Dependencies page to find instructions on how to set up your host machine.

Build system

We use a CMake-based build system to manage dependencies.

Running seL4

This section presents a case study, by the end of which you can run seL4test on a simulator.

Fetching, Configuring and Building seL4test

To build a project, you need to:

  • check out the sources using Repo,
  • configure a target build using CMake,
  • build the project using Ninja.
  1. Use repo to check sel4test out from GitHub. Its manifest is located in the sel4test-manifest repository.
mkdir seL4test
cd seL4test
repo init -u https://github.com/seL4/sel4test-manifest.git
repo sync
  1. Configure an x86_64 build directory, with a simulation target to be run by Qemu. QEMU is a generic and open source machine emulator and virtualizer, and can emulate different architectures on different systems.
mkdir build-x86
cd build-x86
../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE
ninja

The target configurations available for each project are potentially different depending on what the project supports. Building/Using describes how projects can generally be configured. 3. The build images are available in build-x86/images, and a script build-x86/simulation that will run Qemu with the correct arguments to run seL4test.

./simulate

  1. On success, you should see:

    Test VSPACE0002 passed

        </testcase>

        <testcase classname="sel4test" name="Test all tests ran">

        </testcase>

</testsuite>

All is well in the universe

For more information on seL4test see its project page.

Using real hardware

See Hardware for supported hardware and how to set it up.

Learn more

seL4 Tutorials

The seL4 and CAmkES Tutorials are an introduction to the design of seL4, and also to preparing to develop for seL4, and they are also used internally to train new seL4 engineers. You are strongly encouraged to complete the tutorials if you are new to seL4: they will quickly bring you up to speed and ready to practically contribute.

Publications

You can find a long list of seL4 publications here:

The seL4 project page at Trustworthy Systems.

Youtube

Get Help

Mailing lists

If you have ideas or questions, please use the developer mailing list:

There is also a low-bandwidth list for general announcements: