SeL4 and Camkes Tutorials
To get setup, go through the How to Try Out seL4 page.
In the tutorials, cmake will make the build files and ninja will build the tutorials from those build files. There'll be a simulate script that runs the tutorial on qemu emulated hardware. For more information on the cmake software and usage you can check out a tutorial[1] and the documentation.
The official sel4 and camkes tutorials page is at https://docs.sel4.systems/Tutorials/
Before starting with the sel4 tutorials, you can also follow the C tutorial.
Also, you can Read About CMake.
After this you can look at some SeL4 Web Applications such as a webserver or a http web page ui.
I'm also trying to make a Camkes VM Linux links port.
First sel4 hello world test
1. Make a new folder called seL4test and change to that folder
cd ~ mkdir seL4test cd seL4test sudo apt install repo repo init -u https://github.com/seL4/sel4test-manifest.git repo sync
2. Make a build directory and build a sel4 simulation in qemu.
mkdir build-x86 cd build-x86 sudo ../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE sudo ninja ./simulate
3. You should see the output end with: "All is well in the universe"
5. To exit the qemu test, press:
Ctrl+A x
6. To exit the container (without stopping any processes) enter:
exit
sel4 tutorials
1. Go to the home directory and create a new directory called sel4-tutorials-manifest.
cd ~/ mkdir sel4-tutorials-manifest cd sel4-tutorials-manifest
2. Get the repo. If using containers, open a container first with "container".
repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest.git repo sync --no-clone-bundle
3. We'll start with the hello world tutorial. Initialize the hello world[2] build. The --solution part of the command gives you the completed version of the exercise. If going through the exercise, drop the "--solution" part of the init line. To see a walk through of the hello-world tutorial exercise, go to the sel4 hello-world tutorial walk through page.
mkdir hello-world cd hello-world sudo ../init --tut hello-world --solution
4. Navigate to the newly created tutorial_build directory to build it. It will be simulated in qemu.
cd .. cd hello-world_build sudo ninja ./simulate
5. To exit qemu enter:
Ctrl+A x
6. If you decide to go through the exercise, the point is to make you aware of the sources that get initialized for the tutorials. That is, in the hello-world tutorial there will be a CMakeLists.txt, src/main.c, and helloworld.md file. To complete the tutorial, edit src/main.c to say:
#include <stdio.h> int main(int argc, char *argv[]) { printf("Hello, World!\n"); printf("Second hello\n"); return 0; }
8. Then,
cd .. cd hello-world_build ninja ./simulate
The output should end with:
Hello, World! Second hello
To exit QEMU enter: Ctrl+A x
9. To see the other tutorials, navigate to /host/projects/sel4-tutorials/tutorials and you'll see the tutorials stored in this sel4-tutorials-manifest directory.
10. Next is the sel4 capabilities tutorial. Make sure to add --solution to the ../init line if you want the completed tutorial.
cd ~/sel4-tutorials-manifest mkdir capabilities cd capabilities sudo ../init --tut capabilities --solution cd .. cd capabilities_build sudo ninja ./simulate
There is information about the uncompleted exercise at the sel4 capabilities tutorial walk through page.
11.
cd ~/sel4-tutorials-manifest mkdir untyped cd untyped sudo ../init --tut untyped --solution cd .. cd untyped_build sudo ninja ./simulate
There is information about the uncompleted exercise at the sel4 uptyped tutorial walk through page.
12.
cd ~/sel4-tutorials-manifest mkdir mapping cd mapping sudo ../init --tut mapping --solution cd .. cd mapping_build sudo ninja ./simulate
There is information about the uncompleted exercise at the sel4 mapping tutorial walk through page.
13. The threads tutorial and tutorials after this one requires a config.yaml file.[3] Create that first.
mkdir /home/weiqi/.stack cd /home/weiqi/.stack sudo gedit config.yaml
Include this line in the file:
allow-different-user: true
Then continue with
cd ~/sel4-tutorials-manifest mkdir threads cd threads sudo ../init --tut threads --solution cd .. cd threads_build sudo ninja ./simulate
There is information about the uncompleted exercise at the sel4 threads tutorial walk through page.
This tutorial cannot completed because there are file permission errors. More info to be written on the threads sel4 tutorial troubleshooting page.
14.
cd ~/sel4-tutorials-manifest mkdir ipc cd ipc sudo ../init --tut ipc --solution cd .. cd ipc_build sudo ninja ./simulate
There is information about the uncompleted exercise at the sel4 ipc tutorial walk through page.
15.
cd ~/sel4-tutorials-manifest mkdir notifications cd notifications sudo ../init --tut notifications --solution cd .. cd notifications_build sudo ninja ./simulate
There is information about the uncompleted exercise at the sel4 notifications tutorial walk through page.
16.
cd ~/sel4-tutorials-manifest mkdir interrupts cd interrupts sudo ../init --tut interrupts --solution cd .. cd interrupts_build sudo ninja ./simulate
There is information about the uncompleted exercise at the sel4 interrupts tutorial walk through page.
17.
cd ~/sel4-tutorials-manifest mkdir fault-handlers cd fault-handlers sudo ../init --tut fault-handlers --solution cd .. cd fault-handlers_build sudo ninja ./simulate
There is information about the uncompleted exercise at the sel4 fault-handlers tutorial walk through page.
[camkes-vm-crossvm camkes-vm-linux capabilities dynamic-1 dynamic-2 dynamic-3 dynamic-4 fault-handlers hello-camkes-0 hello-camkes-1 hello-camkes-2 hello-camkes-timer hello-world interrupts ipc mapping mcs notifications threads untyped]
camkes tutorials
18. Next will be the Camkes tutorial[4]. It is called the hello-camkes-0 tutorial[5]. To make the build, navigate to the tutorial file. From inside the container at the host directory:
cd ~/sel4-tutorials-manifest mkdir hello-camkes-0 cd hello-camkes-0 sudo ../init --tut hello-camkes-0 --solution cd .. cd hello-camkes-0_build sudo ninja ./simulate
19. After hello-camkes-0 are the hello-camkes-1, hello-camkes-2, and hello-camkes-timer tutorials. So next up is hello-camkes-1[6].
cd ~/sel4-tutorials-manifest mkdir hello-camkes-1 cd hello-camkes-1 sudo ../init --tut hello-camkes-1 --solution cd .. cd hello-camkes-1_build sudo ninja ./simulate
20. Next is hello-camkes-2.
cd ~/sel4-tutorials-manifest mkdir hello-camkes-2 cd hello-camkes-2 sudo ../init --tut hello-camkes-2 --solution cd .. cd hello-camkes-2_build sudo ninja ./simulate
21. Next is hello-camkes-timer
cd ~/sel4-tutorials-manifest mkdir hello-camkes-timer cd hello-camkes-timer sudo ../init --tut hello-camkes-timer --solution cd .. cd hello-camkes-timer_build sudo ninja ./simulate
[Tutorials should work up to this point.]
22. For the Camkes VM Linux tutorial as well as the following Camkes Cross VM tutorial you will need some additional dependencies[7]. If you made an upgrade from Ubuntu 16.04 to 18.04 or some other previous version, you might need to make some adjustments. [Downgrade ubuntu 16.04 clang related packages at the second aptitude option for clang?[8] If there are some interfering problems from ubuntu 16.04. You also might need to get the specific ubuntu 18.04 bionic version as requested with "gdb/bionic"[9].]Then, begin again at sel4-tutorials-manifest.
sudo apt install python3-pip #Already in How to Try Out seL4 pip3 install --user camkes-deps #Already in How to Try Out seL4 sudo apt install haskell-stack #Already in How to Try Out seL4 sudo apt install aptitude sudo aptitude install clang sudo apt install gdb/bionic sudo apt install libssl-dev libclang-dev libcunit1-dev libsqlite3-dev #Already in How to Try Out seL4 sudo apt install qemu-kvm #Already in How to Try Out seL4 cd sel4-tutorials-manifest container
It seems you also need install some other things[10][11]:
sudo apt install gcc-multilib sudo apt install g++-multilib
- The tutorial is called camkes-vm-linux [as opposed to camkes-vm-crossvm[12], the next one]. Before starting it, make sure that VT-x is enabled (see the setup page) and that KVM is installed. Then enable nested virtualisation with KVM guests.[13][14][15][16][17] If it's able to be enabled, Ubuntu turns on nested virtualization by default. For the solution, instead of the ../init line given below, use "../init --tut camkes-vm-linux --solution". For camkes-vm-examples, there's on simulate script[18].
I want to try to port links2 or other terminal web browser here, and use the simulated e1000 NIC to connect to the web. For more info on this, go to the camkes-vm-linux terminal web browser page.
For troubleshooting comments, see the camkes-vm-linux troubleshooting page.
sudo touch /etc/modprobe.d/kvm_intel.conf sudo chmod -R 777 '/etc/modprobe.d/kvm_intel.conf' echo "options kvm-intel nested=Y" >> /etc/modprobe.d/kvm_intel.conf sudo chmod -R 777 /etc/modprobe.d/qemu-system-x86.conf sudo echo 'options kvm_intel nested=1' >> /etc/modprobe.d/qemu-system-x86.conf
Before running the tutorial, also edit the ~/.stack/config.yaml to allow the process to go through file permissions. Note that when copying lines to change files, remove the extra spaces in front (as would be removed for the formatted command lines as well).[19]
sudo gedit ~/.stack/config.yaml
Add this line to the end of it[20]:
allow-different-user: true
To run the tutorial:
cd ~/sel4-tutorials-manifest mkdir camkes-vm-linux cd camkes-vm-linux sudo ../init --tut camkes-vm-linux --solution
Here you need to add some extra steps to the tutorial and edit the ~/sel4-tutorials-manifest/camkes-vm-linux/modules/CMakeLists.txt file.
cd ~/sel4-tutorials-manifest/camkes-vm-linux/modules sudo gedit CMakeLists.txt
Change the "DefineLinuxModule(poke)" line to say:
DefineLinuxModule( ${CMAKE_CURRENT_SOURCE_DIR}/poke poke-module poke-target KERNEL_DIR ${LINUX_KERNEL_DIR} )
You might also want to add a capdl path to the ~/.bashrc file:
sudo gedit ~/.bashrc
Add the following lines:
PATH=$PATH:/usr/local/bin:$HOME/sel4-tutorials-manifest/camkes-vm-linux_build/capDL-tool export SEL4_CACHE_DIR=$HOME
Then go to the camkes-vm-linux_build file and continue:
cd ~/sel4-tutorials-manifest/camkes-vm-linux_build sudo ninja
sudo ip tuntap add tap0 mode tap sudo ip addr add 10.0.120.100/24 dev tap0 sudo ip link set dev tap0 up
sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=split --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="-enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0"
It will ask for a username and password with:
buildroot login: Password:
The login and password and "root" and "root".
After logging typing help in the bash here gives: Built-in commands:
. : [ [[ alias bg break cd chdir command continue echo eval exec exit export false fg getopts hash help history jobs kill let local printf pwd read readonly return set shift source test times trap true type ulimit umask unalias unset wait
Since the machine is simulated with a e1000 NIC, it seems like it's possible to setup a network connection. I haven't yet figured out how to do this. For more info, see camkes-vm-linux troubleshooting.
23. For the Camkes Cross VM tutorial,
cd ~/sel4-tutorials-manifest mkdir camkes-vm-crossvm cd camkes-vm-crossvm sudo ../init --tut camkes-vm-linux --solution cd .. cd camkes-vm-crossvm_build sudo ninja
sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=split --extra-cpu-opts "+vmx" --extra-qemu-args="-enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0"
Troubleshooting[edit | edit source]
More troubleshooting info on the SeL4 and Camkes Tutorials Troubleshooting Page.
References[edit | edit source]
- ↑ https://medium.com/@onur.dundar1/cmake-tutorial-585dd180109b
- ↑ https://docs.sel4.systems/Tutorials/hello-world
- ↑ https://github.com/commercialhaskell/stack/issues/3048
- ↑ https://docs.sel4.systems/Tutorials/hello-camkes-0.html
- ↑ https://docs.sel4.systems/Tutorials/hello-camkes-0.html
- ↑ https://docs.sel4.systems/Tutorials/hello-camkes-1.html
- ↑ https://docs.sel4.systems/HostDependencies#camkes-build-dependencies
- ↑ https://askubuntu.com/questions/223237/unable-to-correct-problems-you-have-held-broken-packages
- ↑ https://askubuntu.com/questions/1061762/ubuntu-18-04-cant-upgrade-because-of-libpython3-6-version-conflicts
- ↑ https://askubuntu.com/questions/182587/build-32-bit-on-64-bit-ubuntu-installing-ia32-libs-does-not-include-libstdc
- ↑ https://stackoverflow.com/questions/2086072/linking-using-g-fails-searching-for-lstdc
- ↑ https://sel4.systems/pipermail/devel/2019-November/002559.html
- ↑ https://www.linux-kvm.org/page/Nested_Guests
- ↑ https://unix.stackexchange.com/questions/119358/create-file-in-folder-permission-denied
- ↑ https://askubuntu.com/questions/21555/command-to-append-line-to-a-text-file-without-opening-an-editor
- ↑ https://www.juniper.net/documentation/en_US/vsrx/topics/task/installation/security-vsrx-kvm-nested-virt-enable.html
- ↑ https://www.server-world.info/en/note?os=Ubuntu_18.04&p=kvm&f=8
- ↑ http://sel4.systems/pipermail/devel/2019-October/002486.html
- ↑ https://github.com/commercialhaskell/stack/issues/3048
- ↑ https://docs.haskellstack.org/en/stable/yaml_configuration/#allow-different-user