June 2021 - Devel - lists.sel4.systems

Re: Tutorial Problem
by Peter Chubb 30 Jun '21

30 Jun '21

>>>>> "Michael" == Michael Neises <neisesmichael(a)gmail.com> writes: Michael> Peter, When I try to remove vme from the -cpu line, I get the Michael> following error at simulation time: OK, so you need nested virtualisation. That's not supported in code-translation mode, only when you're using the KVM kernel module. The message you got was about the simulated CPU, not your host. If you can enable KVM, qemu will pass through your host to the simulation. Looks like you have the kernel packages installed, now you need to make sure that: 1, The version of qemu you're using supports KVM, and 2. you have permissions to use KVM. The first is easy. On Debian-derived systems (debian, ubuntu, mint, etc) sudo apt install qemu-kvm should do the trick. Similarly sudo yum install qemu-kvm on Redhat-derived systems. The second is a little harder. Do ls -l /dev/kvm You'll see something like crw-rw----+ 1 root kvm 10, 232 Jun 30 09:13 /dev/kvm if kvm is installed. The second username (in this case, 'kvm') is the group you need to be in. Do sudo useradd your-login kvm (replacing 'kvm' with the actual group /dev/kvm is in, and 'your-login' with you local login name.) qemu-system-x86_84 -enable-kvm should then work. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

Tutorial Problem
by Michael Neises 30 Jun '21

30 Jun '21

Hello everyone, The tutorials provided here are failing to build for me: https://github.com/seL4/sel4-tutorials Here are the steps to reproduce the errors: git clone git@github.com:seL4/seL4-CAmkES-L4v-dockerfiles.git && git clone git@github.com:seL4/sel4-tutorials.git && make -C ./seL4-CAmkES-L4v-dockerfiles user HOST_DIR=$(pwd)\ followed by cd sel4-tutorials && mkdir build && cd build && ../init.py --plat pc99 --tut camkes-vm-linux Then I am met with the error: ERROR:root:Parent directory is not tutorials root directory which I can fix by changing this line to read "init.py": https://github.com/seL4/sel4-tutorials/blob/d040028999b83c6af2309785f746810… Trying again after this edit, I meet the following errors: loading initial cache file ../projects/sel4-tutorials/settings.cmake CMake Error: Error processing file: ../projects/sel4-tutorials/settings.cmake CMake Error: The source directory "/host/sel4-tutorials/build" does not appear to contain CMakeLists.txt. Specify --help for usage, or press the help button on the CMake GUI. Traceback (most recent call last): File "../init.py", line 90, in <module> sys.exit(main()) File "../init.py", line 78, in main result = common.init_directories(args.plat, args.tut, args.solution, File "/host/sel4-tutorials/common.py", line 101, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/host/sel4-tutorials/common.py", line 69, in _init_build_directory return sh.cmake(args + [tute_directory], _cwd=directory, _out=output, _err=output) File "/usr/local/lib/python3.8/dist-packages/sh.py", line 1520, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python3.8/dist-packages/sh.py", line 784, in __init__ self.wait() File "/usr/local/lib/python3.8/dist-packages/sh.py", line 841, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python3.8/dist-packages/sh.py", line 865, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/bin/cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DFORCE_IOMMU=ON -DTUTORIAL_DIR=build -C ../projects/sel4-tutorials/settings.cmake /host/sel4-tutorials/build STDOUT: STDERR: Either I'm missing something obvious or these instructions have fallen out of date. In any case I would be grateful for any advice. Best, Michael Neises

4 5

How to avoid seL4 passing packets to Linux VM guest
by Hugo V.C. 24 Jun '21

24 Jun '21

Hi, I wonder how to have seL4 host not passing network frames to Linux VM guest. I mean, I would like to have seL4 dealing with TCP/IP and processing packets at the host level but then I want to use a custom communication channel with the Linux guest. So, the very first step would be to stop forwarding network frames to the guest. Any hint where I can start experimenting with this? Cheers,

2 4

Some small details in kernel code and docs
by Mark Jones 24 Jun '21

24 Jun '21

Hi All, Here are a few minor details/questions about the kernel code & documentation. (I've confirmed that these are present in the new seL4-12.1.0 release.) 1) kernel/include/arch/x86/arch/32/mode/machine.h has the following definition (some code elided): static inline word_t FORCE_INLINE x86_read_fs_base_impl(void) { word_t base = 0; base &= ...; base &= ...; base &= ...; return base; } I'm pretty sure that the three &= operators here should be |= or else the result is always going to be zero. The same issue occurs in x86_read_gs_base_impl in the same file. Some follow-up questions: Can anyone say if this would have been detected if the PC99 (32-bit) platform had been verified? More generally, where can I find information about how ia32 segment registers are handled by the kernel? Why aren't they just stored/restored like other user-level registers on kernel entry/exit? Is there something that prevents user-level changes in the ES register, for example, from being observed in other threads? 2) A CNodeRotate will generate a FailedLookup error if the pivot slot either doesn't exist or contains a null capability. But, in the first case the "lookup failed for a source capability" field in the error message is 1, while in the second it is 0. Hardly a serious problem, but this does seem inconsistent. Is this intentional, or a mistake in the specification that has been carried over to the implementation? 3) Section "3.4 Lookup Failure Description" of the manual describes how capability lookup errors are represented in an IPC buffer. But it seems the layout information is incorrect. For example, Section 3.4.2 says that "Offset + 0" will contain seL4_MissingCapability while the number of bits left will be at "Offset + seL4_CapFault_BitsLeft", which is probably supposed to be equivalent to "Offset + 1". But, based on kernel/libsel4/include/sel4/shared_types.h, it would seem that this gives "Offset + 4". Sections 3.4.3 and 3.4.4 have similar problems. 4) On https://docs.sel4.systems/GettingStarted, in the section labeled "Fetching, Configuring and Building seL4test", there are missing line breaks between the commands in the text boxes for Steps 1 and 2, and there are some tags in the text box for Step 4 that probably should not be displayed. Best wishes, and thanks for any feedback! Mark

6 7

CAmkES ARM VM: SATA Passthrough
by Olof Holmberg 21 Jun '21

21 Jun '21

Hi, I ran into the issue of not being able to fit the whole rootfs in RAM (using a qemu-arm-virt device). Therefore I opted for booting the initramfs instead and from there switch root to the proper file system. The booting of the initramfs works fine but the /dev/sda device is not visible to the guest. For x86 (according to these instructions: https://docs.sel4.systems/projects/camkes-vm/) this seems to be done by passing through access to the SATA controller. But since the x86 device configuration is different to the ARM device configuration it requires a different config than the one shown in the instructions. I was wondering how you achieve this SATA passthrough for a ARM VM or if there are any tutorials, other projects or examples that shows how it is done? Best regards, Olof

2 1

Re: Devel Digest, Vol 104, Issue 8
by jonas.cl＠protonmail.com 14 Jun '21

14 Jun '21

Sent from ProtonMail, Swiss-based encrypted email. ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Monday, June 14, 2021 4:00 AM, <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via email, send a message with subject or > body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > Today's Topics: > > 1. sel4 camkes stability (mrshafiei(a)aut.ac.ir) > 2. sel4 camkes stability mechanisms for crash handling and thread failure > (mrshafiei(a)aut.ac.ir) > > > Message: 1 > Date: Sun, 13 Jun 2021 10:47:43 +0430 > From: mrshafiei(a)aut.ac.ir > Subject: [seL4] sel4 camkes stability > To: Siwei.Zhuang(a)data61.csiro.au, devel(a)sel4.systems > Message-ID: 1623565063345060169(a)aut.ac.ir > > Content-Type: text/plain; charset="utf-8" > > Hi Siwei. > I have some problem with my sel4 project, as you know, I'm work on my master project and develop a project on sel4 (camkes) which provide filesystem interfaces, and use ethernet and lwip network stack. This section is ok but sometimes my project crashed and my threads failed. I think that you should start by getting core files from all the crashes. This will point to why the threads fail. I haven't done that for projects running seL4 on hardware, but it is easy to connect gdb to an image running in qemu. I'm sure someone here can point you in the right direction on how to catch core-dump files from hardware. You can of course also implement a watchdog, but start with solving the crashes. /Jonas Claesson > In another words, I wrote my > components and its work correctly but some times (rarely) my threads > crashes and I couldn't find problem. So i decide to use a service like > watch dog timer for garanty all of threads work and when one of therm > failed or crashed, this mechanism detect it and start another thread or > reset the system. > A simple solution can implement is use some thread controlling > (implement WDT in user mode). But I want to know is there in camkes or > sel4 any mechanism for this need? a mechanism for garanti stability and > system availability? > can any body help me? > Is there anybody which confront with this need? > > -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- > > This email was Anti Virus checked by Security Gateway. > > ------------------------------------------------------- > > Message: 2 > Date: Sun, 13 Jun 2021 10:50:18 +0430 > From: mrshafiei(a)aut.ac.ir > Subject: [seL4] sel4 camkes stability mechanisms for crash handling > and thread failure > To: devel(a)sel4.systems > Message-ID: 1623565218534753237(a)aut.ac.ir > > Content-Type: text/plain; charset="utf-8" > > Hi there. > I have some problem with my sel4 project, as > you know, I'm work on my master project and develop a project on sel4 > (camkes) which provide filesystem interfaces, and use ethernet and lwip > network stack. This section is ok but sometimes my project crashed and > my threads failed. > In another words, I wrote my > components and its work correctly but some times (rarely) my threads > crashes and I couldn't find problem. So i decide to use a service like > watch dog timer for garanty all of threads work and when one of therm > failed or crashed, this mechanism detect it and start another thread or > reset the system. > A simple solution can implement is use some thread controlling > (implement WDT in user mode). But I want to know is there in camkes or > sel4 any mechanism for this need? a mechanism for garanti stability and > system availability? > can any body help me? > Is there anybody which confront with this need? > > -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- > > This email was Anti Virus checked by Security Gateway. > > ------------------------------------------------------- > > Subject: Digest Footer > > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > > > --------------------------------------------------------------------------------------------------- > > End of Devel Digest, Vol 104, Issue 8

1 0

hello_rumprun app not worked
by MOHAMAD REZA SHAFIEI 13 Jun '21

13 Jun '21

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

4 4

MMC wait after second command in intialization with mmc_init
by MOHAMAD REZA SHAFIEI 13 Jun '21

13 Jun '21

hi there . i'm work on mmc storage with sel4. i wrote a simple app that use mmc an here is that : ////////////////////////////////////////////////////////////////////// static int count = 0; ps_io_ops_t io_ops = {0}; struct netif* net_if; mmc_card_t mmc_card = 0; sdio_host_dev_t sdio_host_dev; int mmc_found = 0; void mmc_irq_handle(ps_irq_t* irq) { printf("mmc irq handle .... \n"); if(!mmc_found){ mmc_irq_acknowledge(irq); // printf("mmc not found yet :)\n"); sdio_host_dev.handle_irq(&sdio_host_dev,irq->irq.number); return ; } mmc_irq_acknowledge(irq); mmc_handle_irq(mmc_card,irq->irq.number); } int run(void) { notification = timer_notification(); int err = camkes_io_ops(&io_ops); if (err != 0) { ZF_LOGF("Can not init ops : %d\n", err); }; printf("initialize sdhc1 ...\n"); err = sdio_init(SDHC1, &io_ops, &sdio_host_dev); // while card not present check while(sdio_host_dev.reset(&sdio_host_dev) == -1){ delay(1000); } printf("before mmc_init\n"); mmc_init(&sdio_host_dev, &io_ops, &mmc_card); mmc_found = 1; printf("after mmc_init\n"); if (!err) { printf("SDHC1 inited successfully.\n"); } else { printf("SDHC1 initizatino failed!: %d", err); } while (true) { printf(".\n"); delay(1000); } return 0; //////////////////////////////////////////////// its work but in mmc_init after going to mmc_reset , first command sent but in second command (ie MMC_SEND_EXT_CSD ) wait for ever... can any body help me? best regards -- This email was Anti Virus checked by Security Gateway.

2 1

lighttpd as non root user in sel4webserver demo
by Hugo V.C. 12 Jun '21

12 Jun '21

Hi, I was trying to run lighttpd as non root user in " https://github.com/seL4/sel4webserver" demo and realized it didn't allowed me no matter if I configured /etc/passwd, /etc/group and /etc/shadow and /etc/lighttpd.conf correctly. As I don't have debug tools in this Linux VM to look what's going on I decided to directly modify the lighttpd source code to bypass some native code of the web server and hardcode my own user/group. Looks like it works and I now have lighttpd running with it's own user: # ps -ef PID USER COMMAND 1 root init (...) 60 root /sbin/syslogd -n 64 root /sbin/klogd -n 108 lighttpd lighttpd -f /etc/lighttpd.conf 110 root /sbin/getty -L tty1 0 vt100 (...) I also changed the ownership of the /run/site tree to be owned by root. The changes I did in the source code are basically to bypass "getgrnam()" and "getpwnam()" syscalls as I suspect for some reason (musl libc guilty??) and manually set the setgid value before the chroot. I know this is a very dirty hack... but it works for me. My question is if anyone thinks this can be useful to others I can create a pull request with the changes. I think that even if this is a demo, it is not nice to run lighttpd as root, even for a static website. Of course the "right"/elegant way of solving this would be not to change lighttpd source code... but I was unable to do that way. Let me know your opinions. Cheers,

1 0

Camkes-vm-linux on
by Hugo V.C. 11 Jun '21

11 Jun '21

Hi, I'm trying the camkes-vm-linux tutorial and can't run it in qemu despite having nested guests enabled: hugo@dev:~/seL4/sel4-tutorials-manifest/camkes-vm-linux_build$ cat /sys/module/kvm_intel/parameters/nested Y --------- hugo@dev:~/seL4/sel4-tutorials-manifest/camkes-vm-linux_build$ 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" ./simulate: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 qemu-system-x86_64: warning: host doesn't support requested feature: CPUID.80000001H:EDX.pdpe1gb [bit 26] qemu-system-x86_64: warning: host doesn't support requested feature: MSR(48FH).vmx-exit-load-perf-global-ctrl [bit 12] qemu-system-x86_64: warning: host doesn't support requested feature: MSR(490H).vmx-entry-load-perf-global-ctrl [bit 13] qemu-system-x86_64: Host doesn't support requested features ./simulate: QEMU failed; resetting terminal in 5 seconds--interrupt to abort --------- any tutorial to build/boot it natively on x86_64? Thanks,

2 1