Devel November 2018

devel@sel4.systems

24 participants
21 discussions

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

19 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 21 Jan '19

21 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

Network lwip for imx6
by wong xuguo 11 Dec '18

11 Dec '18

Hi, I am a student fron Nanjing university, a fresh man of microkernel, specially, know very little about the seL4. Recently I accept a chellange about porting the lwip to sel4, on arch of imx6, does any one could give me a clue? I found the source of camkes does have this code, could I do something to port, to make the lwip work? What my aim is make a tcp echo server. Thank you for all of you help. Best regards from Xuguo Wang

4 4

sel4 on Raspberry Pi 3b Not Working
by Amit Goyal 06 Dec '18

06 Dec '18

Hi All, I tried running seL4 on Raspberry Pi 3b using the following links: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ https://docs.sel4.systems/Hardware/Rpi3.html https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html#fnref1 I get the following: CACHE: Misaligned operation at range [20000000, 20000014] CACHE: Misaligned operation at range [20008c80, 200092ef] CACHE: Misaligned operation at range [200192f0, 203bb4f0] CACHE: Misaligned operation at range [203bc000, 203c6030] CACHE: Misaligned operation at range [203c6030, 203c8000] ## Starting application at 0x20000000 … and then nothing works and the processor halts. I have tried the pre-built uboot binary, complied uboot versions v2017.1 and v2016.11 as suggested by steve sloloski (on the blog) and uboot version v2016.05 (out of curiosity) but nothing works. Can someone please suggest a possible way out. -- Thanks and Regards, Amit Goyal

2 4

seL4 cache pinning
by 송대영 02 Dec '18

02 Dec '18

Hi, I read "Improving Interrupt Response Time in a Verifiable Protected Microkernel" paper. This paper improved IPC performance by using cache pinning and I want to know how to implement cache pinnng. But this paper doesn't refer how to manipulate cache lines. Would you give me some methods how to read cache lines and write cache lines?

3 2

sel4bench config problem
by 송대영 24 Nov '18

24 Nov '18

Hi, I have a sel4bench config problem. I use 'ccmake ..' command to configure sel4 configuration but system prints error with this message. Build files have been written to: /home/scribnote5/sel4bench_thesis/build CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:18 (include) CMakeLists.txt:21 (include) Please help me!

2 1

seL4 stack overflow
by Anna.Lyons＠data61.csiro.au 22 Nov '18

22 Nov '18

Hi everyone, I've created a proposal for an seL4 stack overflow, which will complement the mailing list. Please support it! https://area51.stackexchange.com/proposals/120611/sel4?referrer=oNjnX5y9POx… Cheers, Anna.

2 1

seL4 on Raspberry 3
by talos 20 Nov '18

20 Nov '18

Hi Did anyone try seL3 on raspberry pi 3? I tried following these links:https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ https://docs.sel4.systems/Hardware/Rpi3.html https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html#fnref1 I set the serial port 115200, 8N1, but I only got some messy codes, I did not get the booting information! Did anyone find this cases? Thanks Sincerely

2 1

Re: [seL4] seL4 10.1.0 and camkes-3.6.0
by jonas.cl＠protonmail.com 16 Nov '18

16 Nov '18

Hi, Today I created a few pull-requests on seL4 repos to build x86-64 with clang: - https://github.com/seL4/seL4/pull/105 - https://github.com/seL4/musllibc/pull/4 - https://github.com/seL4/seL4_tools/pull/19 /Jonas ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Wednesday, November 14, 2018 5:28 PM, <devel-request(a)sel4.systems> wrote: > Message: 3 > Date: Wed, 14 Nov 2018 16:28:17 +0000 > From: Andy Helten andy.helten(a)goctsi.com > To: "Matthew.Brecknell(a)data61.csiro.au" > Matthew.Brecknell(a)data61.csiro.au, "devel(a)sel4.systems" > > <devel(a)sel4.systems> > > > Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0 > Message-ID: > DM6PR17MB2314D1EF141DD6DD6A4779BE92C30(a)DM6PR17MB2314.namprd17.prod.outlook.com > > Content-Type: text/plain; charset="utf-8" > > Disclaimer: I've never compiled sel4 nor executed sel4 and, at this point, am just a follower of this mailing list (with tentative plans to use sel4 "someday") > > Regarding the issue that was fixed here, my first thought was "why did the compiler not complain?". My next thought was "maybe sel4 doesn't enable all warnings in their builds or they ignore the warnings!" But surely a kernel that focuses on security would enable all compiler warnings and fix them immediately as they are introduced. > > Turns out it doesn't matter what sel4 builds are doing, the gcc compiler has a bug that prevents warnings for several of these common "might be used uninitialized" cases. See here: > > https://gcc.gnu.org/bugzilla/show_bug.cgi?id=18501 > > It also appears this bug will not be fixed! An alternative for some projects, though maybe not sel4, is to also compile their code with clang, which does catch these uninitialized cases. If sel4 can use clang to catch these types of mistakes earlier, in a compiler warning, it might save a lengthy validation procedure to catch the error (if it gets caught at all). > > Just thought folks might be interested in this gcc bug -- I certainly wasn't aware of it. > > Andy > > -----Original Message----- > From: Devel devel-bounces(a)sel4.systems On Behalf Of Matthew.Brecknell(a)data61.csiro.au > Sent: Thursday, November 8, 2018 7:22 PM > To: devel(a)sel4.systems > Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0 > > Hi, > > Now that the fix for this issue has made it through our integration pipeline, I can explain what happened, since some of you might be interested. The fix is here: > > https://github.com/seL4/seL4/commit/d12bb374ab47d2b13f438969d2eb5dde1021af84 > > At line 56, the target variable was originally declared uninitialised. > If the loop at lines 57 to 64 executes at least once, then the variable is initialised at line 58. But if the loop does not execute, then the variable would remain uninitialised when it is used at line 65. This would be the case if infer_cpu_gic_id was ever called with nirqs <= 0. > This is not a problem in the released kernel, becuase infer_cpu_gic_id is only ever called once in dist_init, with 32 <= nirqs <= 1024. > > However, the binary translation validation test that failed does not do the inter-procedural analysis that would be necessary to realise this. > When looking at infer_cpu_gic_id, the analysis allows nirqs to take any value. It considers that the loop might not execute, and therefore target might be uninitialised when it is used at line 65. The dataflow model that is produced by the analysis cannot model such undefined behaviour, and so the test fails. With the fix, the variable is never uninitialised, so the analysis does not run into this problem. > > In summary, the fix you see here keeps our proofs happy, but it does not increase the safety of the kernel. This function, as it is actually used, was already safe. > > In terms of our development process, this kind of failure in the binary translation validation is quite rare and difficult to predict. And since our proofs take quite a long time to run, we don't always insist that our kernel developers run the proofs for changes in boot code, which is currently unverified except for binary translation validation. We accept that these failures will occasionally happen, and we deal with them when they do. The functions dist_init and infer_cpu_gic_id are boot-only code, so this was one of those rare failures. > > Of course, we should insist on running all the tests for versions we intend to formally release, and we will for future releases. > > Best regards, > Matt > > From: Brecknell, Matthew (Data61, Kensington NSW) > Sent: Thursday, 8 November 2018 11:25 AM > To: devel(a)sel4.systems > Cc: Mcleod, Kent (Data61, Kensington NSW) > Subject: Re: seL4 10.1.0 and camkes-3.6.0 > > Hi, > > Due to an oversight on my part, seL4 10.1.0 was released without passing the full verification test suite. > > We have no reason to believe that there is any problem in the verified parts of this seL4 version. > > The test that failed is part of the binary translation validation, which produces a dataflow graph from the Isabelle/HOL model of the C code, and then attempts to automatically prove a refinement relation between the C and that dataflow graph. The failure occurred in boot code, which in any case is currently not verified. The failure does not mean that there is any problem with the C code. Most likely, it just means that some new code uses some C idiom which is currently not handled by the automatic translation process. > > All other components of the verification test suite pass, including security proofs and functional correctness proofs for the Isabelle/HOL model of the C code. > > Nevertheless, we intend to rectify this failure as soon as possible, and we'll make further announcements when we understand what happened. > > I want to reiterate that this was entirely my fault, and was not at all Kent's fault. > > Best regards, > Matt > > From: Devel devel-bounces(a)sel4.systems on behalf of Kent.Mcleod(a)data61.csiro.au Kent.Mcleod(a)data61.csiro.au > Sent: Thursday, 8 November 2018 8:44 AM > To: devel(a)sel4.systems > Subject: [seL4] seL4 10.1.0 and camkes-3.6.0 > > See an online copy of the release notes at: > https://docs.sel4.systems/sel4_release/seL4_10.1.0 > https://docs.sel4.systems/camkes_release/Camkes_3.6.0 > > 10.1.0 2018-11-07: SOURCE COMPATIBLE > > Changes > > -------- > > - structures in the boot info are not declared 'packed' > - these were previously packed (in the GCC attribute sense) > - some field lengths are tweaked to avoid padding > - this is a source-compatible change > - ARM platforms can now set the trigger of an IRQ Handler capability > - seL4_IRQControl_GetTrigger allows users to obtain an IRQ Handler capability > and set the trigger (edge or level) in the interrupt controller. > > - Initial support for NVIDIA Jetson TX2 (ARMv8a, Cortex A57) > - AARCH64 support added for raspberry pi 3 platform. > - Code generation now use jinja2 instead of tempita. > - AARCH32 HYP support added for running multiple ARM VMs > - AARCH32 HYP VCPU registers updated. > - A new invocation for setting TLSBase on all platforms. > - seL4_TCB_SetTLSBase > - Kbuild/Kconfig/Makefile build system removed. > > camkes-3.6.0 2018-11-07 > Using seL4 version 10.1.0 > > Changes > > -------- > > - AARCH64 is now supported. > - CakeML components are now supported. > - Added `query` type to Camkes ADL to allow for querying plugins for component configuration values. > - Components can now make dtb queries to parse device information from dts files. > - Component definitions for serial and timer added on exynos5422, exynos5410, pc99. > - Preliminary support for Isabelle verification of generated capDL. > - See cdl-refine-tests/README for more information > - Simplify and refactor the alignment and section linking policy for generated Camkes binaries. > - Dataports are now required to declare their size in the ADL. > - Templates now use seL4_IRQHandler instead of seL4_IRQControl, which is consistent with the seL4 API. > - This change is BREAKING. > - Remove Kbuild based build system. > - Remove caches that optimised the Kbuild build system, which are not required with the new Cmake build system. > - Added virtqueue infrastructure to libsel4camkes, which allows virtio style queues between components. > > > Upgrade Notes > > -------------- > > - Any dataport definitions that did not specify a size must be updated to use a size. > - Any template that used seL4_IRQControl must be updated to use seL4_IRQHandler. > - Projects must now use the new Cmake based build system. > > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > -------------------------------------------------------------------------------- > > Subject: Digest Footer > > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > --------------------------------------------------------------------------------- > > End of Devel Digest, Vol 54, Issue 12

2 1

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel November 2018