October 2023 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 15 Oct '24

15 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

Use C-parser on seL4 based application
by r2ji＠uwaterloo.ca 20 Nov '23

20 Nov '23

Hi, I have been trying to reuse the seL4 verification framework to verify a toy example I built on seL4, and I am currently stuck on the c-parser step. I am trying to use c-parser to parse the example I built, then conduct refinement verification. The toy example is a normal c project, which includes `sel4.h`. From this thread: https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/3QYNFY… I learned that I am supposed to do $ ./isabelle/bin/isabelle jedit -d . -l CParser toy.thy And the toy.thy file is supposed to begin with `install_C_file("toy.c")`. However, since toy.c includes sel4.h, I am not sure how to preprocess it before I put it into toy.thy. I know the standalone c-parser can have a -I flag to include in all the dependency directories, but it cannot open an interactive window. (From my understanding, the standalone c-parser seems to be only a checking tool) I also know that when sel4 is parsed into HOL, it is preprocessed into a single c file `kernel_all.c_pp`, which is later parsed. I am not sure if the preprocessor tool can be reused for other applications as well. My question is summarized as: 1. Is there a way to add an include directory in interactive CParser? 2. If not, can I reuse the preprocessing approach for sel4 to preprocess my application to a singleton file that can be parsed by c-parser? Any help will be appreciated! Thanks, Ru

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 29 Oct '23

29 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Nov 1, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Camkes-vm-linux tutorial
by felicianidaniele＠gmail.com 26 Oct '23

26 Oct '23

Hi, I modified the vm_tutorial.camkes file to obtain two VMs. It works but I would like to see the two virtual machines on two different consoles. Is it possible? Thanks Daniele

1 0

vm-minimal on raspberry pi4
by felicianidaniele＠gmail.com 18 Oct '23

18 Oct '23

Hi everyone, I would like to run vm-minimal and vm-multi (camkes-vm-manifest repo) on raspberry pi 4 4gb RAM. Can someone help me? Thanks Daniele

1 0

Running Sel4 on Rasberry pi 4 4 gb RAM
by felicianidaniele＠gmail.com 18 Oct '23

18 Oct '23

Hello, i'm trying to upload seL4 ( seL4test-driver-image-bcm2711 image) on raspberry pi 4 but i'm encountering two different errors: 1. If I follow the website procedure and upload the sel4test image into the address 0x10000000 the error is : “Reading file would overwrite reserved memory” 2. If I try to upload the image into 0x1000000 I read the following error: “sel4 failed assertion ‘isSchedulable(candidate)’ at /kernel/thread.c can someone help me? Thanks Daniele

2 2

Help with navigating the l4v repository
by Typaldos, Athanasios 17 Oct '23

17 Oct '23

Hello, I am from Lin Zhong’s group at Yale University and I am currently looking at the seL4 specifications and proofs. I am interested in finding the invariants at the abstract level regarding the capability management (CNode and CSpace). I would need some help with navigating the repository, because I am relatively new to interactive theorem proving in general. - I think what I am looking for is in the `l4v/proof/invariant-abstract` directory inside the `{CNode, CSpace}*_AI.thy` files. Is this correct ? - How can I distinguish between helper lemmas and the invariants that you state for example in your paper: SeL4: formal verification of an OS kernel<https://dl.acm.org/doi/10.1145/1629575.1629596> ? - Is there any textual artifact that lists the invariants in prose that could help me ? - Can you clarify me the relationship between the specifications in `l4v/spec/abstract` and the proofs in `l4v/proof/invariant-abstract` ? According to my understanding, the abstract specification defines the system in the abstract level, whereas the proofs use these definitions from the specifications to prove properties and invariants about them. So, the invariants are the statements that the proofs prove. Am I on the right track ? Thank you for your help, Thanasis Typaldos

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 15 Oct '23

15 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Oct 18, 5pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Incorrect dtb in the Microkit tutorial
by Luke Hart 08 Oct '23

08 Oct '23

Hello, It seems that the linux.dtb file supplied with the tutorial code is not correct and does not allocate enough memory for the initrd. The symptoms this issue caused when attempting to run part4 was that the libresolv.so.2 could not be opened and the vmm panic'ed. The linux.dtb supplied in the 'solution' folder in the git repository has 'initrd-end' set to a larger value and this version does work. Thanks, Luke

2 1