January 2018 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 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 16 Oct '24

16 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 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

RefOS Building and Execution Error
by ALVI Aslam (MORPHO) 09 Feb '18

09 Feb '18

Hello Team, I was currently understanding the RefOS but the current code which is present in GIT is not Buildable at all. But after doing some workaround by myself I was able to build it successfully. While executing it on simulator for Kzm 1. Bootstrapping Kernel all finished successfully 2. Dropped to user Space successfully 3. RefOS initialize done successfully 4. Running RefOS Process Server failed In the step 4 while running the Process server it failed while proc_config_new() Failed to spawn Process for Console_server. So Far as per my debugging while coping and writing the elf Header it get failed while getting the capabilities. Excat error line vspace_internal.h line number 396. I would be a great support if anybody help me to resolve the issue. Thank You in advance Regards Aslam Alvi

2 1

OS Engineers Wanted!
by Gernot.Heiser＠data61.csiro.au 31 Jan '18

31 Jan '18

Would you like to get paid for making the world more secure with seL4? I'm in charge of directing OS development for the newly-founded company Hensoldt Cyber. We will develop an integrated, highly-secure hardware-software solution, combined with secure production, aimed at changing the game in securing real-world embedded/cyber-physical systems. Needless to say, there will be close collaboration with the Data61 Trustworthy Systems team. We're now hiring engineers who will help us getting there. Specifically, we're looking for strongly-motivated people with practical experience in OS development, although there is flexibility with the degree of experience. Actual experience with seL4 (or even lesser microkernels ;-) would be awesome. Place of work will be Munich (no remote work possible, sorry). You'll have to be prepared to obtain a German government security clearance (German citizenship is not a requirement for this). Interested? Please send me your CV. Gernot

1 0

seL4 as TEE OS in TrustZone
by Daniel (Xiaolong) Wang 30 Jan '18

30 Jan '18

Hi all, I’m exploring for possible ways to run seL4 as a secure TEE kernel in TrustZone. I found an old discussion thread back in 2016 and corresponding from Gernot: I’m very new to TrustZone technology. I wonder has anyone done that before using seL4? Is there any public available resources for reference? Also on which development board did Data61 run seL4 in the secure world? Thanks -Dan FYI Is it possible to run sel4 as a secure world OS in TrustZone? Has anyone successfully done that before? I believe we have done that in the past (with platforms where we could just ignore the secure/normal split and ran everything in secure mode). There is no reason why it wouldn’t work, it just comes down to initialising the platform correctly. https://sel4.systems/pipermail/devel/2016-March/000750.html <https://sel4.systems/pipermail/devel/2016-March/000750.html> Thanks -Dan

4 7

seL4 as a hypervisor running a linux guest and a RToS(or native sel4 applications) on ARM
by Joel Svensson 29 Jan '18

29 Jan '18

Hello, I'm trying to form an understanding of what one can do with seL4 and how much work is involved in doing it. I am currently under the impression that seL4 could act as a hypervisor and run a linux guest. But I have not found easily accessible instructions for how to do this (ARM targets are most interesting, the Raspberry Pi preferably as it is cheap and ubiquitously available). Did anyone here set up such a seL4 as hypervisor for linux guest and document the procedure? I would be very thankful for links. If such a setup is doable, can you still run some native seL4 code on the "hypervisor" then? Thank you very much /JS

2 2

python-capdl sets incorrect permissions on elf setions
by Joseph Takagi 29 Jan '18

29 Jan '18

Hi I believe the capdl python tool does not correctly set permissions on data loaded from component ELF files. I am wondering if this is a known issue with a fix or whether I'm best off diving in and attempting to fix it myself. Im running on a 32-bit ARM platform The camkes generated linker scripts result in several ELF sections (including .rodata .text and .bss) being lumped together in a single ELF segment. The permissions on this segment in the ELF segment header are RWE. This can be seen from the example output below. readelf -l foo_group_bin Elf file type is EXEC (Executable file) Entry point 0x107b64 There are 4 program headers, starting at offset 52 Program Headers: Type Offset VirtAddr PhysAddr FileSiz MemSiz Flg Align EXIDX 0x021ad8 0x00111ad8 0x00111ad8 0x00008 0x00008 R 0x4 LOAD 0x010000 0x00100000 0x00100000 0x12178 0xd9000 RWE 0x10000 <-- .bss .text .rodata etc. are here with RWE permissions LOAD 0x030000 0x00200000 0x00200000 0x00000 0x01000 RW 0x10000 GNU_STACK 0x000000 0x00000000 0x00000000 0x00000 0x00000 RWE 0x10 Section to Segment mapping: Segment Sections... 00 .ARM.exidx 01 .text .init .fini .rodata .eh_frame .ARM.exidx .data .init_array .fini_array .jcr __vsyscall .bss guarded 02 ignore_fooregs 03 The individual sections are given more sensible permissions via their respective section headers, as can be seen below: .text has permissions 'AE' for alloc and execute, .rodata has 'A' and .bss has 'AW', etc. readelf -S ./foo_group_bin There are 28 section headers, starting at offset 0x8524c: Section Headers: [Nr] Name Type Addr Off Size ES Flg Lk Inf Al [ 0] NULL 00000000 000000 000000 00 0 0 0 [ 1] .text PROGBITS 00100000 010000 00eb68 00 AX 0 0 4096 <-- .text can't be written [ 2] .init PROGBITS 0010eb68 01eb68 000014 00 AX 0 0 4 [ 3] .fini PROGBITS 0010eb7c 01eb7c 000014 00 AX 0 0 4 [ 4] .rodata PROGBITS 0010f000 01f000 002ad4 00 A 0 0 4096 <-- .rodata is read-only [ 5] .eh_frame PROGBITS 00111ad4 021ad4 000004 00 A 0 0 4 [ 6] .ARM.exidx ARM_EXIDX 00111ad8 021ad8 000008 00 AL 1 0 4 [ 7] .data PROGBITS 00112000 022000 000168 00 WA 0 0 4096 [ 8] .init_array INIT_ARRAY 00112168 022168 000004 00 WA 0 0 4 [ 9] .fini_array FINI_ARRAY 0011216c 02216c 000004 00 WA 0 0 4 [10] .jcr PROGBITS 00112170 022170 000004 00 WA 0 0 4 [11] __vsyscall PROGBITS 00112174 022174 000004 00 WA 0 0 4 [12] .bss NOBITS 00112178 022178 000b08 00 WA 0 0 8 [13] guarded NOBITS 00113000 022178 0c6000 00 WA 0 0 4096 [14] ignore_fooregs NOBITS 00200000 030000 001000 00 WA 0 0 1048576 [15] .debug_info PROGBITS 00000000 022178 027a60 00 0 0 1 [16] .debug_abbrev PROGBITS 00000000 049bd8 00a4d4 00 0 0 1 [17] .debug_loc PROGBITS 00000000 0540ac 0113f1 00 0 0 1 [18] .debug_aranges PROGBITS 00000000 0654a0 000ef8 00 0 0 8 [19] .debug_line PROGBITS 00000000 066398 00c5ff 00 0 0 1 [20] .debug_str PROGBITS 00000000 072997 0060c1 01 MS 0 0 1 [21] .comment PROGBITS 00000000 078a58 000038 01 MS 0 0 1 [22] .ARM.attributes ARM_ATTRIBUTES 00000000 078a90 000039 00 0 0 1 [23] .debug_frame PROGBITS 00000000 078acc 002638 00 0 0 4 [24] .debug_ranges PROGBITS 00000000 07b108 002238 00 0 0 8 [25] .shstrtab STRTAB 00000000 085137 000114 00 0 0 1 [26] .symtab SYMTAB 00000000 07d340 005230 10 27 1269 4 [27] .strtab STRTAB 00000000 082570 002bc7 00 0 0 1 Key to Flags: W (write), A (alloc), X (execute), M (merge), S (strings) I (info), L (link order), G (group), T (TLS), E (exclude), x (unknown) O (extra OS processing required) o (OS specific), p (processor specific) The ELF.py code from python-capdl applies the segment permissions to the entire segment so disregards the permissions in the ELF section headers. As a result, data which shouldn't be writable or executable are so. I can confirm this through analysis of the capdl output which shows the entire segment being mapped as 64KB pages with RWE permissions set. Any advice on this would be appreciated. Joe Takagi

2 1

Fileserver connection error in RefOS
by ALVI Aslam (MORPHO) 24 Jan '18

24 Jan '18

Hello All, Greetings, I was trying to run RefOs for ia32_defconfig. Found some error while building but after removing all of them I was able to run it. But now I have an error while selfLoader is trying to laod Terminal or Timer_Server. [00.0] SELFLOADER | main(): --- Starting RefOS process selfloader --- [00.1] SELFLOADER | main(): Connect to the server for [/fileserv/terminal] ERROR main(): Error while connecting to file server. [00.84] PROCSERV | proc_exit_handler(): Process PID 2043 exiting with status 0 !!! [00.85] PROCSERV | proc_syscall_postaction(): Releasing process 2043 [/fileserv/terminal]... [00.0] SELFLOADER | main(): --- Starting RefOS process selfloader --- [00.1] SELFLOADER | main(): Connect to the server for [fileserv/timer_server] ERROR main(): Error while connecting to file server. I have also attached the full log of execution. I have also debugged it and found that while resolving the serverPath its get failed. Please help me out to resolve this issue. Thank You in advance Regards, Aslam

1 0

Hyperkernel paper
by Jeff Waugh 23 Jan '18

23 Jan '18

Hi seL4 friends, Any thoughts and/or feelings about the Hyperkernel paper from SOSP'17? This paper describes an approach to designing, implementing, and formally > verifying the functional correctness of an OS kernel, named Hyperkernel, > with a high degree of proof automation and low proof burden. https://homes.cs.washington.edu/~helgi/papers/hyperkernel.pdf Thanks, Jeff

2 1

Userspace Debugging for ia32
by ALVI Aslam (MORPHO) 23 Jan '18

23 Jan '18

Hello Team, I need some help to start a userspace debugging for ia32. Since as per the instruction mention in the link https://wiki.sel4.systems/Debugging%20guide I was able to use GDB for kzm based defconig. But how can I start userspace debugging for ia32 based defconig? Thank You & Regards, Aslam

2 1

seL4 vs. Integrity-178B
by Baconicsynergy 22 Jan '18

22 Jan '18

Hello friends :) First off, congratulations on being the new primary microkernel of choice for the Genode Operating System Framework! I'm very excited. Now to my questions - how does the formal verification of seL4 compare with the Integrity-178B security guarantees? Also, how do two structurally compare with each other in terms of design principles and implementation? Best regards, Joel Desermeau seL4

2 1

seL4 8.0.0 and CAmkES camkes-3.2.0 release
by Kent.Mcleod＠data61.csiro.au 18 Jan '18

18 Jan '18

seL4 8.0.0 and CAmkES camkes-3.2.0 release = seL4 8.0.0 = Note: Meltdown and Spectre patches are not included in this release and will be included in a forthcoming release once they have been verified. Once they are merged they will still be accessible through the master branch of seL4 on github. Release notes: https://wiki.sel4.systems/seL4%208.0.0 CHANGES file in https://github.com/seL4/seL4/tree/8.0.0 = CAmkES camkes-3.2.0 = Release notes: https://wiki.sel4.systems/camkes-3.2.0 CHANGES file in https://github.com/seL4/camkes-tool/tree/camkes-3.2.0 = Miscellaneous updates = == CMake build system == Replacing the current kbuild build system with a new CMake build system is still in progress. The kernel only CMake build is now used by l4v. Initial CMake versions for sel4test, sel4bench and our CAmkES projects are still being developed. We intend to do a release that contains the Kbuild and CMake scripts working side by side, and will then start to remove the Kbuild scripts after that. == Changes to manifests for our projects == Each project that we maintain now has a default.xml and master.xml manifest file. master.xml is used to specify the branch tips of the upstream git repositories that a project uses. default.xml now pins all of the repositories to revisions that last passed our regression tests. For this current release and future releases a release tag will be created on each manifest repo specifying the revision of default.xml that uses the released revisions of all the repositories. The seL4 and camkes-tool repos will still be tagged on each release, and all other repositories will have versioned branches created the same as before. We have only just finished testing this change and the various documentation will be updated over the coming days. == Meltdown and Spectre == As mentioned above, Meltdown and Spectre related patches are not present in this release and will be merged into the kernel once verification is complete. There will likely be a blog post accompanying their release. ?

1 0

Re: [seL4] x86 kernel address space side channels
by Jeroen "Slim" van Gelderen 05 Jan '18

05 Jan '18

Thanks for clarifying that. Do you have any information on whether AMD is wrong claiming that their architecture is not vulnerable? On Thu, Jan 4, 2018 at 11:29 AM, Alex Elsayed <eternaleye(a)gmail.com> wrote: > > On Jan 4, 2018 07:37, "Jeroen "Slim" van Gelderen" <askslim(a)gmail.com> > wrote: > > On Wed, Jan 3, 2018 at 4:37 PM, Alex Elsayed <eternaleye(a)gmail.com> wrote: > >> In addition, Intel has published a press release, claiming that this >> issue (counter to some claims elsewhere) does in fact affect other >> vendors and architectures: >> >> https://newsroom.intel.com/news/intel-responds-to-security-r >> esearch-findings/ > > > Contrary to the PR, Intel CPUs do indeed have a design flaw aka bug which > makes them vulnerable to Meltdown. Meltdown has not been reproduced on ARM > or AMD and AMD thinks Meltdown is not applicable to their chips due to > architectural differences. > > The Spectre attack is the attack that is applicable across the board. > > As far as Linux is concerned only Intel machines will be hit with the > KPI-related slowdown (5%-30%) since KPI will be disabled on AMD CPUs. (And > I assume this goes for Windows too.) This looks bad for Intel, hence the > FUD. > > > It's a bit more nuanced than that. First of all, section 6.4 of the > Meltdown paper is quite clear: non-Intel CPUs _do_ still perform the > problematic access; it's the particular covert channel they use to extract > the information from it that does not port over. Many expect this to > change; the authors themselves see that whether AMD or ARM are affected is > _unknown-_, not that they are unaffected. > > Second, the patch from AMD to disable KPTI has not been accepted AFAIK, > and AArch64 is adding KPTI. > > Third, Meltdown is a _less severe_ attack by far compared to Spectre. > Meltdown can be addressed by KPTI, but some forms of Spectre use little > besides the BTB, which is known[1] to be infeasible to flush in software. > > Fourth, Intel (and I) posted that link _prior_ to the release of the > papers, at a time when all that was known to the public was "very serious > vulnerability in speculative execution" - its claims should be read in that > context. > > [1]: https://arxiv.org/abs/1612.04474 > > > -- Jeroen "Slim" van Gelderen

1 0

x86 kernel address space side channels
by Corey Richardson 05 Jan '18

05 Jan '18

https://lwn.net/Articles/738975/ That's really painful, for Linux ;) I don't think seL4 is really impacted? I'm having a hard time thinking about what sensitive information could be disclosed by probing the kernel window. Maybe which memory regions caps being accessed by other concurrently running threads occupy? You could use that to make a covert channel, if the two threads trying to communicate are running in parallel. It seems really dubious that that could give you anything useful otherwise, and as the literature shows timing side channels are unavoidable on x86. Thought it was interesting and worth sharing! -- cmr http://octayn.net/ +16038524272

6 8

I/O and PCIE on TX1
by Jon Lamb 04 Jan '18

04 Jan '18

Hi seL4 Dev Team, I'm currently working on (mostly learning at this point) how we could add TX1 platform support for a PCIE network card (Intel 82580), using TK1 and others as a reference. I'm fairly new to working with PCI, but after looking around I think I have a general idea on what I need to do. I would appreciate it very much if someone with more experience could tell me if I'm on the wrong path here: * Using the TX1 TRM, I would populate the missing physical device region definitions in 'tx1/plat/machine/devices.h', and update the 'dev_p_regs[]' struct in 'tx1/plat/machine/hardware.h' * Figure out if I need to build up SMMU support (also a newbie here), I'm having doubts on whether I can bang on physical addresses or not without it * Construct a suitable implementation of 'ps_io_port_ops_t' for handling the I/O routines for libpci * Put together a hello world main program to exercise some of libpci's functionality * Once things are looking good there, move up to libethdrivers and port the needed bits for our Ethernet adapter using existing references (and eventually hooking up to lwip hopefully) At this point, I've been avoiding camkes for the sake of learning how everything works and if anyone can recommend a good starting C project for doing I/O on an ARM platform, that would be very helpful. Thanks in advance. -- Jon Lamb Software Engineer | *PolySync* 1020 SE 11th Ave, Portland, OR 97214 *c* 888.810.4284 x701 <888.810.4284%C2%A0x713> | *e* jlamb(a)polysync.io | *w* polysync.io <http://www.polysync.io/>

2 2

iMX6 dvfs registers
by Zippy Maniac 02 Jan '18

02 Jan '18

Hi, Sorry for pestering (again). I am trying to access the DVFS registers from a seL4 component and they seem to be read only. I can read/write them from UBoot and the kernel. So my guess is the registers require privilege even though I have yet to find a definitive statement to this effect in the ARM / NXP documentation. So the question is. Is it possible to give a component the necessary access rights to the DVFS registers via camkes? Or is there some other sort of workaround I could employ to gain access? Cheers, Zippy

2 1