Getting started with seL4, CAmkES, and L4v: Dependencies
We have found in Trustworthy Systems that a big hurdle for new people coming to work on the seL4 ecosystem is setting up the dependencies. Setting up a machine with all that’s required to build seL4, CAmkES, and L4v is no simple task, particularly if you intend to target multiple platforms.
This blog post will take you through how we have setup our software dependencies in Trustworthy Systems, and how we built it to make it much easier and cleaner for anyone to get starting with seL4, CAmkES, and L4v.
Some history
Approximately a year and a half ago, the regression testing setup in Trustworthy Systems was migrated from a bare-metal server to running within a Docker container. This transition was motivated by two main factors:
- Containers allow the regression system to be isolated from the server itself, meaning no unintentional OS upgrades or software changes can affect it,
- Docker uses Dockerfiles (simple text files) to build containers, which means we could use version control to observe, track, and modify the dependencies.
After the initial transition from bare-metal to container was complete and tested, we were able to start organising the Dockerfiles into a hierarchy that reflected the implicit dependency structure more clearly.
By doing this, we get a number of benefits:
- Dependencies: we are able to isolate the important dependencies that are relevant to each part of our software stack
- Regression testing flexibility: the regression software is a leaf, and so can be swapped out or modified easily (no need to rebuild the whole stack). In our current setup, this is used to ensure Bamboo and its Agents share the same environment, but also allows for switching Bamboo to Jenkins or some other CI very easily.
- Reproducibility: the images we share are the literal basis of our regression testing system, so by sharing them, people can reproduce our steps and verify it’s all OK.
- Usability: The most relevant bits can be released externally to users for them to use!
Helping users get started
Making the seL4, CAmkES, and L4v Docker images available was a good first step to helping users, but still represents a potentially off-putting first step into something unknown (“What the hell is Docker, and how do I use it?”). To mitigate this, a small wrapper Makefile is provided with the Dockerfiles, which enables users to get going as smoothly and quickly as possible.
To demonstrate, these are the steps to go from a fresh Mint/Ubuntu/Debian machine to one ready to build seL4/CAmkES:
1) Install Docker (reading https://get.docker.com/ is a good start point), and add yourself to the docker group:
user@my_machine:~/$ sudo usermod -aG docker $USER # you may need to re-login to your machine for this to take effect
2) Install git and make:
user@my_machine:~/$ sudo apt install git make
3) Clone the Dockerfiles:
user@my_machine:~/$ mkdir -p ~/dev user@my_machine:~/$ git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git ~/dev/seL4-CAmkES-L4v-dockerfiles
4) Run the Docker container:
user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user
It may take a little while to go and fetch the images from the internet, but you’ll soon see something similar to:
make: Entering directory '/home/user/dev/seL4-CAmkES-L4v-dockerfiles'
sed -i -e '/FROM/c\FROM trustworthysystems/camkes' extras.dockerfile
docker build --force-rm=true -f extras.dockerfile -t extras .
Sending build context to Docker daemon 18.43kB
Step 1/1 : FROM trustworthysystems/camkes
---> 160c8b18fae0
Successfully built 160c8b18fae0
docker build --force-rm=true \
--build-arg=UNAME=user \
--build-arg=UID=8462 \
-f user.dockerfile \
--no-cache \
-t user_img-8462 .
Sending build context to Docker daemon 18.43kB
Step 1/5 : FROM extras
---> 160c8b18fae0
Step 2/5 : ARG UID
---> Running in ad877301c9be
---> d8ca455183d4
Removing intermediate container ad877301c9be
Step 3/5 : ARG UNAME
---> Running in f659c95cd16c
---> e68b6ca720e8
Removing intermediate container f659c95cd16c
Step 4/5 : RUN useradd -u ${UID} ${UNAME} && mkdir /home/${UNAME} && echo 'echo "___ "' >> /home/${UNAME}/.bashrc && echo 'echo " | _ _ |_ _ _ |_ |_ "' >> /home/${UNAME}/.bashrc && echo 'echo " | | |_| _) |_ \)/ (_) | |_ | ) \/ "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo " __ "' >> /home/${UNAME}/.bashrc && echo 'echo "(_ _ |_ _ _ _ "' >> /home/${UNAME}/.bashrc && echo 'echo "__) \/ _) |_ (- ||| _) "' >> /home/${UNAME}/.bashrc && echo 'echo " / "' >> /home/${UNAME}/.bashrc && echo 'echo "Hello, welcome to the sel4/CAmkES/L4v docker build environment"' >> /home/${UNAME}/.bashrc && echo 'export PATH=/scripts/repo:$PATH' >> /home/${UNAME}/.bashrc && echo 'cd /host' >> /home/${UNAME}/.bashrc && chown -R ${UNAME}:${UNAME} /home/${UNAME} && chmod -R ug+rw /home/${UNAME}
---> Running in 4589d0fc61e0
---> e079b1ac2687
Removing intermediate container 4589d0fc61e0
Step 5/5 : VOLUME /home/${UNAME}
---> Running in 92381df97d70
---> 10d44ec2f426
Removing intermediate container 92381df97d70
Successfully built 10d44ec2f426
docker run \
-it \
--hostname in-container \
--rm \
-u user \
-v /home/user/dev/seL4-CAmkES-L4v-dockerfiles:/host \
-v user-home:/home/user \
user_img-8462 bash
___
| _ _ |_ _ _ |_ |_
| | |_| _) |_ \)/ (_) | |_ | ) \/
/
__
(_ _ |_ _ _ _
__) \/ _) |_ (- ||| _)
/
Hello, welcome to the sel4/CAmkES/L4v docker build environment
user@in-container:/host$
And that’s it, you now have a terminal that is fully equiped to build seL4 and CAmkES!
You can exit the container by typing:
user@in-container:/host$ exit
5) The makefile comes with a bunch of commands:
user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user_sel4 user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user_camkes user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user_l4v user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user # alias for user_camkes
Each user* command specifies which dependencies you require. The most common is seL4 and CAmkES dependencies, so to make things easier you can add an alias to your bash config like this:
user@my_machine:~/$ echo $'alias container=\'make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user HOST_DIR=$(pwd)\'' >> ~/.bashrc # open a new terminal for this to take effect
You will have to open up a new terminal for this command to take effect (or run source ~/.bashrc).
Now you can run:
user@my_machine:~/$ container
in any directory to launch the seL4/CAmkES Docker container in the current directory.
Building seL4test
To demonstrate a good workflow we’ve come up with, let’s show an example of building seL4test.
First, we’ll create a new folder to store the source code. On your host machine, run:
user@my_machine:~/$ mkdir -p ~/dev/sel4test user@my_machine:~/$ cd ~/dev/sel4test
Start up the container:
user@my_machine:~/dev/sel4test$ container # if you didn't setup the bash alias run: make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user HOST_DIR=~/dev/sel4test
Now we can see the Docker container prompt:
user@in-container:/host$
Now let’s get seL4 test:
user@in-container:/host$ repo init -u https://github.com/seL4/sel4test-manifest.git # don't worry if it complains about "Please tell me who you are" user@in-container:/host$ repo sync user@in-container:/host$ ls # let's see all the files kernel projects tools CMakeLists.txt init-build.sh
Compile seL4test for the sabre simulator:
user@in-container:/host$ mkdir build && cd build user@in-container:/host/build$ ../init-build.sh -DPLATFORM=sabre -DBAMBOO=TRUE -DAARCH32=TRUE -DSIMULATION=TRUE user@in-container:/host/build$ ninja
Once it’s done compiling, we can test everything is working by running:
user@in-container:/host/build$ ./simulate # lots of output
This will run the image we generated inside QEMU. When it’s done running, we should see:
202/202 tests passed.
To quit QEMU, press: ctrl+a q
To quit the container, run:
user@in-container:/host/build$ exit
and you will be returned back to your host machine’s terminal, and you can see all that we’ve done:
user@my_machine:~/dev/sel4test$ ls -la build/images/ total 3032 drwxr-xr-x 2 user user 4096 May 10 15:31 . drwxrwxr-x 11 user user 4096 May 10 15:31 .. -rwxr-xr-x 1 user user 3154876 May 10 15:31 sel4test-driver-image-arm-imx6
The image has been generates in the ~/dev/sel4test/images directory on your host machine, and has all the right permissions for you.
If you are ready to start doing some development, we recommend you do that outside the Docker container, since it does not have common tools like vim or emacs – and you probably have your own comfortable environment setup. When you want to compile, use the container alias to boot into Docker and use make, or simply have the Docker container running in another terminal.
Verifying seL4
Formal verification is major part of the appeal of using seL4. To verify it yourself, we need to do a little bit more setup.
First, we should add another bash alias to make things easier:
user@my_machine:~/dev/sel4test$ echo $'alias containerl4v=\'make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user_l4v HOST_DIR=$(pwd)\'' >> ~/.bashrc # open a new terminal for this to take effect
You will have to open up a new terminal for this command to take effect (or run source ~/.bashrc).
Now we can run the command:
user@my_machine:~/dev/sel4test$ containerl4v
It might take a little while to download the new files. Once it’s done, exit the container by running:
user@in-container:/host$ exit
Now we need to get the L4v files:
user@my_machine:~/$ mkdir -p ~/dev/verification user@my_machine:~/$ cd ~/dev/verification user@my_machine:~/dev/verification$ containerl4v # boot up the l4v container in this directory. Alternately, you can run: make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user_l4v HOST_DIR=~/dev/verification user@in-container:/host$ repo init -u https://github.com/seL4/verification-manifest.git user@in-container:/host$ repo sync
Again, this might take a while to download.
Once it’s ready, have a look at the files:
user@in-container:/host$ ls graph-refine HOL4 isabelle l4v seL4
Now we can follow the instructions from the L4v repository (https://github.com/seL4/l4v), starting from the “Running the Proofs” section:
user@in-container:/host$ cd l4v user@in-container:/host/l4v$ ./run_tests Running 45 test(s)... Started isabelle ... Finished isabelle passed ( 0:04:17 real, 0:12:36 cpu, 4.32GB) Started CamkesAdlSpec ... Finished CamkesAdlSpec passed ( 0:00:28 real, 0:01:00 cpu, 3.02GB) # lots of output Started AutoCorresDoc ... Finished AutoCorresDoc passed ( 0:00:14 real, 0:00:36 cpu, 3.27GB) Started AutoCorresTest ... Finished AutoCorresTest passed ( 0:08:19 real, 0:35:51 cpu, 10.84GB) Started AutoCorresSEL4 ... Finished AutoCorresSEL4 passed ( 0:52:32 real, 1:07:54 cpu, 10.53GB) 45/45 tests succeeded. All tests passed.
This can take a lot of time, a lot of RAM, and a fair amount of harddisk space, so make sure you have plenty of all of them (~8 hours, ~32 GB of RAM, and ~20 GB of harddisk space).
If you are running on your normal desktop with an X11 session, you can even open up jEdit from inside the Docker container:
user@in-container:/host/l4v$ ./isabelle/bin/isabelle jedit -d . -l ASpec
And you should see something like this:
Changing the build environment
Since almost anything could potentially be build on top of the seL4 ecosystem, we cannot include all the possible dependencies that may be required. However, we wanted to make it easy to add additional software.
Let’s say we needed the program “Cowsay” as a build dependency. Currently in the build environment:
user@my_machine:~/$ container # boot up the build environment user@in-container:/host$ /usr/games/cowsay bash: /usr/games/cowsay: No such file or directory
To get it, open up the ~/dev/seL4-CAmkES-L4v-dockerfiles/extras.docker file on your host machine, and uncomment the first RUN block, so it looks like this:
RUN apt-get update -q \
&& apt-get install -y --no-install-recommends \
cowsay \
&& apt-get clean autoclean \
&& apt-get autoremove --yes \
&& rm -rf /var/lib/{apt,dpkg,cache,log}/
Save and close the file, and then boot up the build environment in your source directory:
user@my_machine:~/$ cd ~/dev/sel4test && container # or make -C ~/dev/seL4-CAmkES-L4v-dockerfiles user HOST_DIR=~/dev/sel4test
Docker will detect the changes in extras.dockerfile and build them into a local image that sits on top of the container Trustworthy System distributes. Now you can run cowsay inside the build environment:
user@in-container:/host$ /usr/games/cowsay "Thank god I now have cowsay!"
______________________________
< Thank god I now have cowsay! >
------------------------------
\ ^__^
\ (oo)\_______
(__)\ )\/\
||----w |
|| ||
user@in-container:/host$
Any command can be run after a RUN statement (for example: apt, curl, dpkg, ln, etc.), so you should be able to configure it to your needs. See the other Dockerfiles in the repository for a reference.
Cleanup
The Docker images, and running the L4v regression, can end up taking up a bit of room on your hard disk. If you need to clear them out, you can run a few different cleaning commands:
user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles clean_isabelle # Remove the L4v regression heaps (usually quite large) user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles clean_home_dir # Remove the home directory for the container (usually relatively small) user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles clean_data # Do both of the above user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles clean_images # Remove all of the images downloaded and created from trustworthysystems user@my_machine:~/$ make -C ~/dev/seL4-CAmkES-L4v-dockerfiles clean # Do all of the above
“But I don’t want Docker!”
For all the people interested who can’t or don’t want to install Docker, having access to the Dockerfiles provides a good step in figuring out what you’ll need to install on your own machine. However, in the future to make this a bit easier, we’ll be including a basic script to transform the Dockerfiles into a bash script that strips out any of things you wouldn’t want to do to your real machine (like running the && rm -rf /var/lib/{apt,dpkg,cache,log}/ commands!)
Moving forward
We welcome any feedback on our dependency systems, so feel free to give them a try and let us know! Some plans for the near future are:
- Document each dependency more clearly within the Dockerfiles so it’s clear what they’re for and what uses them,
- Getting the dockerfile2bashscript converter working and useful,
- Migrate more commonly used dependencies from our TS_tools.dockerfile to the externally released files,
- Build parallel stacks of Dockerfiles based on other popular distros, such as Ubuntu or CentOS, which can run as build agents in our CI.