December 2018 - 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

Questions about Memory Management in seL4
by Daniel Wang 18 May '23

18 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

TLB issue
by Stefan Kalkowski 15 Nov '19

15 Nov '19

Dear sel4 community, yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems. The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault. To be able to reproduce the problem, you might investigate the simple test case here: https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7… My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you. Best regards Stefan -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

3 3

Poll for Separation Kernel (microkernel) CC Protection Profile
by Holger Blasum 20 Jan '19

20 Jan '19

Hello seL4 devel, microkernel-based systems can be used as separation kernels[*] for security. At the moment there is a poll on input for a Common Criteria for Information Technology Security (CC) separation kernel protection profile draft, organized by a certMILS.eu colleague from Rostock Univ, at https://evasys.uni-rostock.de/evasys/online.php?p=ccuf-sk-wg The idea is to have a base protection profile (PP) that all players can agree with and to specify additional functionality as add-ons to the PP (e.g., in the form of PP modules). The questionnaire is an opportunity to provide early feedback. Note that there are no mandatory questions, i.e. you can freely move around / you can leave any question unanswered - the only condition for your feedback be submitted to the collection system is that you go to the last page and use the submit button there. We invite feedback via that poll by end of this week. If, beyond the questionnaire, you want to join the Common Criteria User's Forum separation kernel working group, or anyone would like to have more time, just let me know by answering to this email. [*] https://en.wikipedia.org/wiki/Multiple_Independent_Levels_of_Security Best, -- Holger Blasum, SYSGO

1 1

An RFC process for seL4
by Curtis.Millar＠data61.csiro.au 01 Jan '19

01 Jan '19

Hi Everyone, We are currently in the process of setting up and moving to a public Jira instance to manage many of our development issues. The first part of this move involves setting up a request for comments (RFC) process which will be implemented using a Jira project. You can find out more about the RFC process in the first RFC: https://sel4kernel.atlassian.net/browse/RFC-1 You are encouraged to leave feedback on the issue, but doing so requires that you are logged in with an Atlassian Cloud account. The introduction of a public issue tracker will allow us to better engage with our community, accept more contribution from outside the seL4 development team, and better communicate the ways in which we are changing and improving the seL4 ecosystem. In the long term, we hope to use this to track all of the major issues currently under development across the ecosystem, accept issues submitted by the public, and open issues up for members of the greater community to work on. The issue tracker will initially be used as the basis of the RFC process, which will allow for the community to get involved with larger changes to the ecosystem. Many of the details of the process can only be clearly resolved as it becomes used more regularly as part of ongoing development, so much of how it works is still to be determined. We are hoping to finalise this process at the beginning of the new year before we use it to present a number of other changes we have been planning so we can get your feedback before their design and implementation is finalised. This new issue tracker and RFC process are just part of greater ongoing changes on which we are working to grow the community and to increase its involvement. We wish you all a happy holiday season and look forward to the start of a new year with seL4. Cheers, Curtis

2 2

seL4 at 35C3 in Leipzig (Chaos Communication Congress)
by Daniel Schäfer 26 Dec '18

26 Dec '18

Hey there, are some of you going to the 35C3 congress in Leipzig, Germany? I'm trying to understand seL4 and get into developing for it. I'd love to talk to someone if anyone's around. Best regards and merry Christmas, Daniel P.S. My "home" is the Selfnet assembly

1 0

Fwd: CAmkES tutorial build system
by Wei Xiang Leow 18 Dec '18

18 Dec '18

Hello Kent, Thanks for the reply :) The moving/copying was to demonstrate the differences between the tutorial and the solution. Creating and completing a new copy of the tutorial doesn't give the expected results either. My understanding is, when we run "./init --tut hello-camkes-1", the build directory is immediately built off the incomplete tutorial, hence it's missing client.instance.bin.dir etc. This isn't fixed when we complete the tutorial and ninja. Hence when someone goes through the tutorial, it doesn't give the expected "Starting the client". If this is the case, could you point me to where I can rectify this? On an separate note, I'm experiencing the same issues as https://sel4.systems/pipermail/devel/2018-October/002221.html. The simulate script exists, but qemu (at least 2.5.0+) seems to only allow "kernel-irqchip=on|off", not split. May I know which version of qemu we should be using? Regards, Leow Wei Xiang On Tue, Dec 18, 2018 at 2:10 PM <Kent.Mcleod(a)data61.csiro.au> wrote: > Hi, > > > Renaming the source directory and the build directories aren't supported > as CMake and Ninja rely on the absolute and relative paths remaining > consistent. You are still able to copy the contents of the source > directory from the solution into the source directory of the non solution > and use the same build directory. The reason why you only see ...Booting all > finished is because when the tutorial starts, there are no components > defined in the camkes assembly, so no components will be loaded by the > initial task. This is why you don't see any output. > > > I don't believe there is an issue, but let me know if I have misunderstood > what you meant. > > > Kind regards, > > Kent. > > > > ------------------------------ > *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Wei Xiang Leow < > leowweixiang1991(a)gmail.com> > *Sent:* Tuesday, December 18, 2018 4:42 PM > *To:* devel(a)sel4.systems > *Subject:* [seL4] CAmkES tutorial build system > > Hello, there seem to be issues with the tutorial build system, at least > for CAmkES tutorial 1. After adding the necessary details and running, I > get "...Booting all finished", no further messages. The solution runs fine, > I get "Starting the client" etc. > > Made fresh copies of the tutorial and solution, and overwrote the > tutorial's files with the solution's. Diff shows that only .tute_config > (--solution) and the .md files differ. Diff on the "_build" folders shows > multiple differences. I assume there is an issue there? > > mkdir tutorial; mkdir solution > ./init --tut hello-camkes-1 > mv hello-camkes-1 tutorial > mv hello-camkes-1_build tutorial > ./init --tut hello-camkes-1 --solution > mv hello-camkes-1 solution > mv hello-camkes-1_build solution > cp solution/hello-camkes-1/hello-1.camkes > tutorial/hello-camkes-1/hello-1.camkes > diff -rq tutorial/hello-camkes-1 solution/hello-camkes-1 > ############################ > Files tutorial/hello-camkes-1/hello-camkes-1.md and > solution/hello-camkes-1/hello-camkes-1.md differ > Files tutorial/hello-camkes-1/.tute_config and > solution/hello-camkes-1/.tute_config differ > ############################ > > diff -rq tutorial/hello-camkes-1_build solution/hello-camkes-1_build > ############################ > Files tutorial/hello-camkes-1_build/build.ninja and > solution/hello-camkes-1_build/build.ninja differ > Files tutorial/hello-camkes-1_build/CMakeFiles/CMakeOutput.log and > solution/hello-camkes-1_build/CMakeFiles/CMakeOutput.log differ > Files tutorial/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt and > solution/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt differ > Files tutorial/hello-camkes-1_build/hello-camkes-1/ast.pickle and > solution/hello-camkes-1_build/hello-camkes-1/ast.pickle differ > Files tutorial/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake and > solution/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake differ > Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: > client.instance.bin.dir > Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: > echo.instance.bin.dir > Files > tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes > and > solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes > differ > Files > tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md > and > solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md > differ > Files tutorial/hello-camkes-1_build/rules.ninja and > solution/hello-camkes-1_build/rules.ninja differ > ############################ > > cp -r tutorial/hello-camkes-1 hello-camkes-1 > cp -r tutorial/hello-camkes-1_build hello-camkes-1_build > cd hello-camkes-1_build > ninja > ./simulate > ############################ > ... > Booting all finished, dropped to user space > ############################ > > <another terminal> > rm -r hello-camkes-1 > rm -r hello-camkes-1_build > cp -r solution/hello-camkes-1 hello-camkes-1 > cp -r solution/hello-camkes-1_build hello-camkes-1_build > cd hello-camkes-1_build > ninja > ./simulate > ############################ > ... > Booting all finished, dropped to user space > Starting the client > ------------------- > Component echo saying: hello world > After the client > ############################ > > Regards, > Leow Wei Xiang >

1 0

CAmkES tutorial build system
by Wei Xiang Leow 18 Dec '18

18 Dec '18

Hello, there seem to be issues with the tutorial build system, at least for CAmkES tutorial 1. After adding the necessary details and running, I get "...Booting all finished", no further messages. The solution runs fine, I get "Starting the client" etc. Made fresh copies of the tutorial and solution, and overwrote the tutorial's files with the solution's. Diff shows that only .tute_config (--solution) and the .md files differ. Diff on the "_build" folders shows multiple differences. I assume there is an issue there? mkdir tutorial; mkdir solution ./init --tut hello-camkes-1 mv hello-camkes-1 tutorial mv hello-camkes-1_build tutorial ./init --tut hello-camkes-1 --solution mv hello-camkes-1 solution mv hello-camkes-1_build solution cp solution/hello-camkes-1/hello-1.camkes tutorial/hello-camkes-1/hello-1.camkes diff -rq tutorial/hello-camkes-1 solution/hello-camkes-1 ############################ Files tutorial/hello-camkes-1/hello-camkes-1.md and solution/hello-camkes-1/hello-camkes-1.md differ Files tutorial/hello-camkes-1/.tute_config and solution/hello-camkes-1/.tute_config differ ############################ diff -rq tutorial/hello-camkes-1_build solution/hello-camkes-1_build ############################ Files tutorial/hello-camkes-1_build/build.ninja and solution/hello-camkes-1_build/build.ninja differ Files tutorial/hello-camkes-1_build/CMakeFiles/CMakeOutput.log and solution/hello-camkes-1_build/CMakeFiles/CMakeOutput.log differ Files tutorial/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt and solution/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt differ Files tutorial/hello-camkes-1_build/hello-camkes-1/ast.pickle and solution/hello-camkes-1_build/hello-camkes-1/ast.pickle differ Files tutorial/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake and solution/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake differ Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: client.instance.bin.dir Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: echo.instance.bin.dir Files tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes and solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes differ Files tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md and solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md differ Files tutorial/hello-camkes-1_build/rules.ninja and solution/hello-camkes-1_build/rules.ninja differ ############################ cp -r tutorial/hello-camkes-1 hello-camkes-1 cp -r tutorial/hello-camkes-1_build hello-camkes-1_build cd hello-camkes-1_build ninja ./simulate ############################ ... Booting all finished, dropped to user space ############################ <another terminal> rm -r hello-camkes-1 rm -r hello-camkes-1_build cp -r solution/hello-camkes-1 hello-camkes-1 cp -r solution/hello-camkes-1_build hello-camkes-1_build cd hello-camkes-1_build ninja ./simulate ############################ ... Booting all finished, dropped to user space Starting the client ------------------- Component echo saying: hello world After the client ############################ Regards, Leow Wei Xiang

2 1

Multiboot and extra modules
by Dave Richards 17 Dec '18

17 Dec '18

Is it (or would it be) possible to specify more than the single root server module and have seL4 create virtual addresses, cap. Spaces, threads (leaving them suspended) and pass the information about these modules to the root server? In this way it would be possible to have GRUB load a multi-server seL4 environment. Thanks, Dave

6 11