SeL4 and Camkes Tutorials

From Secure OS Wiki
Jump to navigation Jump to search

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
  1. 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]

  1. https://medium.com/@onur.dundar1/cmake-tutorial-585dd180109b
  2. https://docs.sel4.systems/Tutorials/hello-world
  3. https://github.com/commercialhaskell/stack/issues/3048
  4. https://docs.sel4.systems/Tutorials/hello-camkes-0.html
  5. https://docs.sel4.systems/Tutorials/hello-camkes-0.html
  6. https://docs.sel4.systems/Tutorials/hello-camkes-1.html
  7. https://docs.sel4.systems/HostDependencies#camkes-build-dependencies
  8. https://askubuntu.com/questions/223237/unable-to-correct-problems-you-have-held-broken-packages
  9. https://askubuntu.com/questions/1061762/ubuntu-18-04-cant-upgrade-because-of-libpython3-6-version-conflicts
  10. https://askubuntu.com/questions/182587/build-32-bit-on-64-bit-ubuntu-installing-ia32-libs-does-not-include-libstdc
  11. https://stackoverflow.com/questions/2086072/linking-using-g-fails-searching-for-lstdc
  12. https://sel4.systems/pipermail/devel/2019-November/002559.html
  13. https://www.linux-kvm.org/page/Nested_Guests
  14. https://unix.stackexchange.com/questions/119358/create-file-in-folder-permission-denied
  15. https://askubuntu.com/questions/21555/command-to-append-line-to-a-text-file-without-opening-an-editor
  16. https://www.juniper.net/documentation/en_US/vsrx/topics/task/installation/security-vsrx-kvm-nested-virt-enable.html
  17. https://www.server-world.info/en/note?os=Ubuntu_18.04&p=kvm&f=8
  18. http://sel4.systems/pipermail/devel/2019-October/002486.html
  19. https://github.com/commercialhaskell/stack/issues/3048
  20. https://docs.haskellstack.org/en/stable/yaml_configuration/#allow-different-user