seL4 下载

宋航

2023-12-01

本文译至：http://sel4.systems/Download/

代码

所有的seL4代码和证明都可以在GitHub上找到： https://github.com.au/seL4, 在标准的开放源代码许可证下。

有几个仓库;最有趣的是项目库（后缀名为-manifest）和这两个：

l4v seL4 证明
seL4 seL4 内核

seL4 项目

seL4内核通常是建立作为项目的一部分。每个项目都有一个与之相关的维基条目提供了更多的信息。此页面上的信息是所有项目共通的。

在seL4开发过程中我们仿照了Android开发过程。每个项目包括一个XML文件，它描述使用哪些仓库，以及如何布置它们做一个可构建系统。

发布的项目有：

verification, seL4 证明。
seL4test, 一个seL4的测试套件，包括一个库的操作系统层。
CAmkES, 一个基于seL4的嵌入式系统的组件体系结构。关于更多的文档，查看CAmkES pages 。
VMM ，一个使用英特尔®VT-x和VT-D扩展的IA32平台的组件化虚拟机监视器。

可能以后追加其他项目。

运行证明

有关如何开始使用seL4证明的信息。

支持的目标平台

这是一个支持平台的列表。并不是所有的项目支持所有这些平台。

Intel 平台
- a PC99-style Intel Architecture 32-bit x86 (ia32)
- There is also experimental support for the 64-bit Intel x86_64 architecture.
ARM 平台
- The Arndale dual core A15 ARM development board
- The Beagleboard, Omap 3530
- The Inforce IFC6410 development board, running a Qualcomm Krait processor that is like an A15.
- The KZM-ARM11-01. The kernel for this board is the one that is formally verified.
- The Odroid-X Exynos4412 board
- The Odroid-XU Exynos 5 board
- The Sabre Lite i.mx6 board.

构建面向ARM目标板，你将需要一个跨平台开发工具链。

获取项目

这些命令用于构建Linux。它们假设你已经知道使用命令行，编译器和GNU make的基础知识。

获取 repo

最新的repo可从谷歌的https://storage.googleapis.com/git-repo-downloads/repo下载。下载它，并把它放在你的PATH

mkdir -p ~/bin
export PATH=~/bin:$PATH
curl https://storage.googleapis.com/git-repo-downloads/repo > ~/bin/repo
chmod a+x ~/bin/repo

repo 依赖于git和python，应该在你的发行版的包系统有提供。

在 Debian 或 Ubuntu:

sudo apt-get install git python

在 Fedora, CentOS 或 RedHAT

sudo yum install git python gpg

使用 repo

选择一个项目开始。作为一个例子，我们将使用sel4test。首先创建一个工作目录，并使用repo初始化它：

mkdir seL4test
cd seL4test
repo init -u https://github.com/seL4/sel4test-manifest.git

这将从谷歌下载最新的repo版本，以及seL4test-manifest项目。为了得到实际的源，你需要使用 repo sync：

repo sync

repo将需要通过大约十分钟来获取所有需要的资料库。

工具链和先决条件

要构建seL4项目你需要相应的工具链。 sel4test只需要相应的编译器，链接器和GNU make。用于运行image，qemu的是理想的。

Fedora和CentOS的说明（RHEL应该也一样）
Debian和Ubuntu的说明

构建项目

每个项目都有一个相关的维基，可以通过GitHub的访问，有最新的依赖和说明。这里的一般说明适用于所有项目。

所有项目的顶层布局是相似的。构建后，它看起来像这样：

$ ls -F
Kbuild@   Makefile@  build/    images/   kernel/  projects/  tools/
Kconfig@  apps@      configs@  include/  libs/    stage/

build

包含编译的文件。

apps

是一个到 projects 一个子目录的符号链接，包含应用程序的源代码。

configs

是一个到 projects 一个子目录的符号链接，包含默认配置

images

包含构建后可直接运行的镜像的最终的链接

include

包括库和内核的头文件

kernel

包含seL4内核

libs

包含库的源代码

projects

放置项目特定部分

stage

编译的库放的位置

tools

包含部分的构建系统，以及其他需要构建项目的工具

configs 中的配置文件根据目标机器和它们完成的工作来命名。大多数在名字中带有'release'或'debug'。调试内核编译时是带有调试符号（所以可以使用GDB），启用断言，并提供sel4debug接口允许调试打印输出到串行端口。

有些配置是为了在QEMU运行。因为QEMU不会对硬件做完全忠实的模拟，有时功能必须被禁用或work around。这些配置它们的名字包含‘simulation’。

要开始，选择要构建的一个目标板，并找到相应的配置文件的名字。

例如，让我们为 ia32 构建seL4test在QEMU模拟器上运行：

make ia32_simulation_release_xml_defconfig

这个拷贝configs/ia32_simulation_release_xml_defconfig到./.config，并设置各种头文件。

你可以看一下配置选项使用：

make menuconfig

另外，您可以使用任何文本编辑器来更改./.config; 如果你做了任何改变，你需要使用make oldconfig重新编译头文件。也建议使用 make clean 来清除任何已构建的 - 构建系统不跟踪尽可能多的依赖，虽然它应该这样做。

对于IA32目标板，你应该不需要做任何改变。对于ARM的目标板，你可能需要在menuconfig的toolchain options里改变交叉编译器前缀。

当你已经配置好了系统，你可以通过执行以下命令编译：

make

经过大约五到十分钟之后，这取决于你的机器有多快，最后会在 images 里生成一些文件。

目前并行编译并不工作，所以不要尝试使用 -j 来加速。但是构建系统支持 ccache，如果你已经安装了它。

模拟结果

make simulate-ia32

这里会生成对应的 qemu 上运行的文件。看Makefile中的细节。在Debian上，你将需要一个最近的QEMU - Wheezy版本太旧了，而且不支持KZM或Beagle目标板。Jessie里的OK。

要在表示测试套件已经完成的 All is well in the universe 消息之后退出QEMU后，输入control-a c q

有用的配置选项

交叉编译器前缀

对于交叉编译（以ARM为目标），可以设置交叉编译。这通常是arm-linux-gnueabi- 或arm-none-eabi-。make menuconfig查找 toolchain-options。
一些默认的配置是关于特定的x86编译器的。通常将前缀设成空的是安全的，如果你已经安装了multilib的gcc。
修改大多数的其他配置选项将导致该要么不能编译，或无法运行系统。

注意事项

kzm 模拟器挂起

qemu 不模拟完整的 sel4 测试运行需要的所有的定时器。使用kzm_simulation_ 配置来以避免依赖于未实现的计时器。

arm-none-eabi

如果你使用arm-none-eabi 编译器，不能链接到预编译的库上，消息如下所示：

/usr/lib64/gcc/arm-none-eabi/4.8.1/../../../../arm-none-eabi/bin/ld: warning: /usr/src/seL4test/stage/arm/imx31/lib/libmuslc.a(internal.o) uses 32-bit enums yet the output is to use variable-size enums; use of enum values across objects may fail

要修改这个问题，make menuconfig 在 seL4 Libraries→Build musl C Library 勾掉 libmuslc use precompiled archive，然后执行make clean，并尝试重新编译。

硬浮点编译器

Debian和Ubuntu新版本的编译器的默认配置使用硬件浮点。这些编译器编译的二进制文件都与预编译的MUSL C库不兼容。你可以调整flag（在tools/common/Makefile.flags：添加-mfloat-abi=soft 到 NK_CFLAGS）或与上面的方法一样禁止使用预编译的库。

运行在真正的硬件上

如何在硬件上引导seL4的细节根据不同体系有所变化。

IA32

构建系统生成x86的多引导标准的image; grub2 stanza是在这里，但方便起见，我们平时启动通过PXE。

menuentry "Load seL4 VM"  --class os {
   load_video
   insmod gzio
   insmod part_msdos
   insmod ext2
   set root='(hd0,msdos2)'
   multiboot /boot/sel4kernel
   module /boot/sel4rootserver
}

ARM 平台

从SD卡或闪存加载u-boot，或者使用 fastboot 或 tftp。大多数应用程序有两个部分：将'kernel'部分作为一个内核，将'应用'部分作为一个initrd。如果只有一个部分放到一个image上（例如，一些平台的seL4test）当它为一个内核。

不同开发板的详细命令有所区别。一般命令查看The General Hardware Page;它也有到具体开发板命令的链接。

Debian交叉编译器

不幸的是Debian在旧的“Use Emdebian”和新的MultiArch系统之间变动。这意味着要固定到Jessie;但现在你可以：

使用旧的编译器，bug已经新版本修正
安装来自Mentor Graphics公司（原来的Sourcery）的编译器，或
从源代码编译一个交叉编译器

CAmkES defconfigs需要特定的编译器

大多数CAmkES的x86默认配置使用32位的CodeSourcery的编译器的i686-pc-linux-gnu-。使用任何系统的x86编译器通常是安全的，—只需设置.config文件该字段为空白。