- Devel - lists.sel4.systems

3 open positions for Proof Engineers at Data61
by Gerwin.Klein＠data61.csiro.au 20 Mar '18

20 Mar '18

Data61 Seeking Proof Engineers ============================== We are are hiring again! If only there were a place where I could prove theorems for money, change the world, and have fun while doing it... Sounds too good to exist? In the Trustworthy Systems team at Data61 that's what we do for a living. We are the creators of seL4, the world's first fully formally verified operating system kernel with extreme performance and strong security & correctness proofs. Our highly international team is located on the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia, one of the world's most liveable cities. We are looking for 3 motivated proof engineers who want to join our team in Sydney, move things forward, and have global impact. We are expanding our team, because seL4 is going places. There are active projects around the world in - Automotive - because cars have been hacked enough - Aviation - for more security and safety for autonomous vehicles - Defence - protecting confidential information - Connected consumer devices - with security built in from the start - Spaceflight - because awesome To make these projects successful, we need to scale formal verification. You would - work on industrial-scale formal proofs in Isabelle/HOL - develop formally verified infrastructure for building secure systems on top of seL4 - contribute to improved proof automation and better reasoning techniques - apply formal proof to real-world systems and tools To apply for this position, you should possess a significant subset of the following skills. - functional programming in a language like Haskell, ML, or OCaml - first-order or higher-order formal logic - basic experience in C - ability and desire to quickly learn new techniques - undergraduate degree in Computer Science, Mathematics, or similar - ability and desire to work in a larger team We are hiring at two levels, so if you are more qualified or experienced than the above would suggest, you can come in as a senior proof engineer. If you additionally have experience - in software verification with an interactive theorem prover such as Isabelle/HOL, HOL4, or Coq, and/or - with operating systems and microkernels you should definitely apply! If you have the right skills and background, we can provide training on the job. Continual learning is a central component of everything we do. You will work with a unique world-leading combination of OS and formal methods experts, students at undergraduate and PhD level, engineers, and researchers from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun, creative, and welcoming workplace with flexible hours & work arrangements. We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See https://ts.data61.csiro.au/diversity/ for more information. Salary ranges for this position, in AUD (plus superannuation): - Junior: 80-91K - Senior: 95-103K depending on experience and qualifications. Apply online at the following links: - https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/464792900/ - https://jobs.csiro.au/job/Sydney%2C-NSW-Senior-Proof-Engineer/464792300/ Your application should include a cover letter, CV, undergraduate transcript (if applicable), and contact information for two references. This round of applications closes 15 April 2018. The seL4 code and proof are open source. Check them out at https://seL4.systems More information about Data61's Trustworthy Systems team at https://ts.data61.csiro.au Still studying? We also have internship opportunities! https://ts.data61.csiro.au/students/

1 0

Unable to Compile Tutorial 2 Exercises
by Amit Goyal 20 Mar '18

20 Mar '18

Hi, I am new to sel4 and was thus practising the tutorials given at: https://wiki.sel4.systems/Tutorials While compiling tutorial 2 exercises, I got the attached error (I have also attached the main.c file). Can someone please help me in resolving it. -- Thanks and Regards, Amit Goyal

2 1

Ethernet driver for TK-1
by Michal Podhradsky 19 Mar '18

19 Mar '18

Hello, I would like to use a similar Ethernet driver component as for x86 platforms here: https://github.com/seL4/camkes-vm/tree/master/components/Ethdriver But in the camkes-vm-arm repository I don't see an equivalent component: https://github.com/SEL4PROJ/camkes-arm-vm/tree/master/apps/vm/components Is the ethernet currently just passed to Linux? And if so, what would entail making a new driver etc similar to x86 platforms? Regards Michal

2 1

VM and VMM Communication for ARM
by Daniel Wang 16 Mar '18

16 Mar '18

Hi all, I have a couple questions about VM an VMM communication for CAMKES-ARM-VM. Please correct me if I’m wrong. I found when VMM load Linux device it installs a vgic (install_linux_devices() -> vm_install_vgic()) But how exactly a interrupt caused by VM is distributed from GIC to VGIC (kernel to VMM)? I saw that we can register a virq to the VGIC (vm_virq_new()), but I’m not sure when a interrupt is generated how it is passed to the VGIC. Second, I found that we can install virtual devices to VM (e.g. for Vchan communication). Seems like when Linux tries to access the mapped virtual device, a page_fault will generated. Does it create a interrupt? How does it processed by VMM code exactly? I found post_main() in the generated camkes.c file has 3 threads, case 3 runs the control thread -> run(), case 5 runs vevent interface vevent__run(), and case 7 runs fault hander. Does it triggers vevent? I’m not sure the control flow. Thank you in advance! Best Regards -Daniel Wang

1 0

irq_server example? Interrupt handlers?
by Richard Clark 14 Mar '18

14 Mar '18

Hi all! I have an Ethernet driver underneath an lwip implementation that I've gotten to run threaded tcpip. It happily passes messages back and forth and all around between half a dozen threads over a dozen ports all on localhost. Every once in a while though, it wants to send a packet to the outside world... this of course invokes the Ethernet driver, which rather annoyingly, is polled. I am looking for the proper way to convert my polled Ethernet driver to be interrupt-driven.... however the sel4 interrupt-handling/dispatching seems to escape my grasp and I could use a little help... It would appear that there is a mechanism to register a request to receive a message whenever an interrupt occurs? irq_server.c? Are there some nice simple examples out there? Is there an easier way perhaps? Thanks! Richard H. Clark ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

Questions about Vchan
by Daniel Wang 14 Mar '18

14 Mar '18

Hi all, I’m trying to figure out how to use the Vchan library to setup communication between guest OS and native components. I got couple questions how you can give me some advices. 1. I saw the camkes_vchan_con_t structure in the helloworld components (camkes-arm-vm), but I could not find the implementation for vchan_con_new_connection(), vchan_con_rem_connection(), etc. Are those autogenerated by camkes? If so how it is generated? static camkes_vchan_con_t con = { .connect = &vchan_con_new_connection, .disconnect = &vchan_con_rem_connection, .get_buf = &vchan_con_get_buf, .status = &vchan_con_status, .alert = &vchan_con_ping, .wait = &vevent_wait, .poll = &vevent_poll, .dest_dom_number = 0, .source_dom_number = 50, }; 2. I tried to compile the Vchan support and demo helloworld components for odroid-xu. But the compile shows error due to the VM.h file (camkes-arm-vm/projects/vm/components/VM/src/cmks_vchan_vm.c:23) cannot be found. How can I generate the VM.h file? Thanks a lot! Best Regards -Daniel Wang

4 5

seL4 developer review of RISC-V privileged ISA spec?
by Kelly Dean 14 Mar '18

14 Mar '18

The RISC-V privileged ISA is not yet finalized. Have the seL4 developers reviewed the draft [1], in case they might have any recommendations for improvement? For example, just last year a blunder (H-mode) was removed from the draft per a proposal [2] on the mailing list. Finalization is planned for this year. Speak now or forever hold your peace. The first public draft of the memory consistency model [3] was also released just last December. And platform standardization, especially the IOMMU, is in progress. [1] https://content.riscv.org/wp-content/uploads/2017/05/riscv-privileged-v1.10… [2] https://groups.google.com/a/groups.riscv.org/forum/#!msg/isa-dev/SfEDPLU0NU… [3] https://groups.google.com/a/groups.riscv.org/forum/#!topic/isa-dev/hKywNHBk…

6 5

Questions about Allocman
by Daniel Wang 12 Mar '18

12 Mar '18

Hi all, I’m trying to understand the code a little bit more. This is kind of a random question. I’m wondering that in a case where we call to allocate a frame using allocman library, where is the physical address of a certain region is stored? In allocman_t there are multiple fields: size_t num_utspace_chunks; struct allocman_utspace_chunk *utspace_chunk; size_t *utspace_chunk_count; struct allocman_utspace_allocation **utspace_chunks; struct allocman_utspace_chunk { size_t size_bits; seL4_Word type; size_t count; }; struct allocman_utspace_allocation { seL4_Word cookie; cspacepath_t slot; }; I didn’t find struct that hold the paddr, also after we create a frame where is that paddr stored? It is stored in slot.capPtr? Also What does the field cookie for? Best Regards -Daniel Wang

3 3

Share UART with Guest Linux
by Daniel Wang 09 Mar '18

09 Mar '18

Hi all, For experiment, I created a simple app along with the vmm using CamKES-ARM-VM repository. Currently the simple app only prints strings periodically using printf(). However as soon as the guest Linux starting running. I cannot print anything and also receives error as following: I assumes it is due to the iommu capability got assigned to Linux by VMM. Is there a way to allow native app also prints information on the screen using printf()? ------------------ libsel4muslcsys: Error attempting syscall 162 FAULT HANDLER: data fault from hello.control (ID 0x1) on address 0xffffff80, pc = 0x135ac, fsr = 0x3840046 FAULT HANDLER: pc = 0x135ac FAULT HANDLER: sp = 0x142d20 FAULT HANDLER: lr = 0x135ac FAULT HANDLER: r0 = 0xffffff80 FAULT HANDLER: r1 = 0 FAULT HANDLER: r2 = 0 FAULT HANDLER: r3 = 0 FAULT HANDLER: r4 = 0x26 FAULT HANDLER: r5 = 0 FAULT HANDLER: r6 = 0 FAULT HANDLER: r7 = 0xfffffff2 FAULT HANDLER: r8 = 0x1 FAULT HANDLER: r9 = 0 FAULT HANDLER: r10 = 0 FAULT HANDLER: r12 = 0x142caa FAULT HANDLER: r14 = 0x135ac FAULT HANDLER: cpsr = 0x20000050 FAULT HANDLER: memory map: FAULT HANDLER: +-- 0x00143fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00143000 -- FAULT HANDLER: | stack FAULT HANDLER: +-- 0x0013f000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0013e000 -- FAULT HANDLER: | <undescribed> FAULT HANDLER: +-- 0x00137fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00137000 -- FAULT HANDLER: | IPC buffer FAULT HANDLER: +-- 0x00136000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00135000 -- FAULT HANDLER: | <undescribed> FAULT HANDLER: +-- 0x00131fff -- FAULT HANDLER: | code and data FAULT HANDLER: +-- 0x00010000 -- CPIO: 2 files found. 0) linux 0x00059c70, 16302080 bytes 1) linux-dtb 0x00fe5ce8, 29415 bytes Best Regards -Daniel Wang

1 1

Compilation Error with version
by Thad Seeberger 08 Mar '18

08 Mar '18

Good day. I am getting hung up compiling the CAmkES compiles. I'm getting following error which I believe is because the version.h.d does not exist. Where is the version set? thx [camkes-accelerator] building... -- Configuring done -- Generating done -- Build files have been written to: /home/xxxx/seL4_camkes_x86_64/stage/x86/pc99/accelerator ninja: error: '/home/xxxx/seL4_camkes_x86_64/tools/camkes/tools/accelerator/DEPFILE', needed by '.', missing and no known rule to make it make: *** [/home/xxxx/seL4_camkes_x86_64/stage/x86/pc99/accelerator/camkes-accelerator] Error 1 ive traced it down I think to this block in the Cmakeadd_custom_command( OUTPUT ${CMAKE_CURRENT_BINARY_DIR} OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/include/version.h OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/version.h.d # Build a valid dependency file from the print-deps script, this is a little awkward COMMAND echo "include/version.h: " > "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/print-deps.py" >> "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND sed -i "s/$$/\\/" "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/mkversion.py" >"${CMAKE_CURRENT_BINARY_DIR}/include/version.h" DEPENDS mkversion.py DEPENDS print-deps.py DEPFILE ${CMAKE_CURRENT_BINARY_DIR}/version.h.d )

4 8

CapDL spec for Camkes-ARM-VM
by Daniel Wang 08 Mar '18

08 Mar '18

Hi all, I’m trying build a PoC system based on the camkes-arm-vm repository. I saw the init process is created using CapDL, but I’m having trouble to find the the CapDL spec file. Could you please point it out for me? Also for the first step, I’m trying to build another app side-by-side with the VMM and guest Linux. I assume I need to modify the CapDL. I’m not exactly the work flow with CapDL can you give me a hint? Thanks. Best Regards -Daniel Wang

2 2

ARM-VM with Linux Distribution
by Daniel Wang 06 Mar '18

06 Mar '18

Hi all, I was able to compile the camkes-arm-vm and run it on a TK1-SOM board. I wonder if it is possible to run a Linux distribution as the guest OS, such as Ubuntu, Fedora, etc.? If so how can we do that? Best Regards -Daniel Wang

2 1

Re: [seL4] seL4 VMM Hangs during loading time
by Daniel Wang 02 Mar '18

02 Mar '18

Hi Kent and Peter, Thank you so much for your response. I do not know what exactly caused the issue. But I upgraded my toolchain and recompiled the image again and it loaded this time. The GCC version is version 7.2.1 (before it was 4.6). Although I still see the misaligned information like this: CACHE: Misaligned operation at range [90000000, 90000014] CACHE: Misaligned operation at range [90001000, 900091c4] CACHE: Misaligned operation at range [900091c4, 900098d8] CACHE: Misaligned operation at range [900198d8, 900198e0] CACHE: Misaligned operation at range [900198e0, 91392ae0] CACHE: Misaligned operation at range [91394000, 913a4820] CACHE: Misaligned operation at range [913a4820, 913a8000] Another thing I found is that U-boot for TK1-SOM cannot detect ethernet, but I was able to copy the image into MMC and load from there. There are two things I want to do with the seL4 ARM VMM platform. First, I want to incorporate the secure boot from U-boot to seL4 and then using seL4 to verified signed Linux. Second, I want to build a PoC native application and allow the communication between the native app to communication with App running in Linux. I’m wondering if anyone did those two things before that can give me some advice? I implemented the the second scenario before using L4re with a paravirtualized L4Linux. But I’m exactly sure how to do it with seL4 yet. Best Regards -Daniel Wang > On Mar 1, 2018, at 8:00 PM, <Kent.Mcleod(a)data61.csiro.au> <Kent.Mcleod(a)data61.csiro.au> wrote: > > Hi Daniel, > > Two things to try: > > First is to confirm that CONFIG_PRINTING is enabled to distinguish if the kernel is successfully starting its init process. > > Second is to check what ${loadaddr} is set to. Yours seems correct, ours seems to be 0x81000000, but that is for the tk1 jetson dev board. > > You could also try editing the elfloader to print out the contents of the kernel entrypoint before it jumps there to confirm that it is the correct instructions in the stage/arm/tk1/kernel.elf binary. > > Below is what I see when I boot the project on our devboard. > > Kind regards, > Kent. > > ---- > U-Boot SPL 2015.10-rc5-00002-gf861f51-dirty (Oct 13 2015 - 13:44:41) > > > U-Boot 2015.10-rc5-00002-gf861f51-dirty (Oct 13 2015 - 13:44:41 +1100) > > TEGRA124 > Model: NVIDIA Jetson TK1 > Board: NVIDIA Jetson TK1 > DRAM: 2 GiB > MMC: Tegra SD/MMC: 0, Tegra SD/MMC: 1 > tegra-pcie: PCI regions: > tegra-pcie: I/O: 0x12000000-0x12010000 > tegra-pcie: non-prefetchable memory: 0x13000000-0x20000000 > tegra-pcie: prefetchable memory: 0x20000000-0x40000000 > tegra-pcie: 2x1, 1x1 configur��K��Ʌ�pcie: probing port 0, using 2 lanes > tegra-pcie: link 0 down, retrying > tegra-pcie: link 0 down, retrying > tegra-pcie: link 0 down, retrying > tegra-pcie: link 0 down, ignoring > tegra-pcie: probing port 1, using 1 lanes > In: serial > Out: serial > Err: serial > Net: RTL8169#0 > Hit any key to stop autoboot: 2 > 0 > Tegra124 (Jetson TK1) # setenv autoload no && dhcp && tftpboot 0x81000000 jetson1/sel4-image > setenv autoload no && dhcp && tftpboot 0x81000000 jetson1/sel4-image > BOOTP broadcast 1 > BOOTP broadcast 2 > BOOTP broadcast 3 > BOOTP broadcast 4 > DHCP client bound to address 10.13.1.172 (2929 ms) > Using RTL8169#0 device > TFTP from server 10.13.0.130; our IP address is 10.13.1.172 > Filename 'jetson1/sel4-image'. > Load address: 0x81000000 > Loading: ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################ > 3.8 MiB/s > done > Bytes transferred = 20493516 (138b4cc hex) > Tegra124 (Jetson TK1) # bootelf 0x81000000 > bootelf 0x81000000 > ## Starting application at 0x90000000 ... > ELF loader: monitor mode init done > Copy monitor mode vector from 90001000 to a7f00000 size 50 > Number of IRQs: 192 > Load seL4 in nonsecure HYP mode 600001da > ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 > paddr=[90000000..9139ffff] > ELF-loading image 'kernel' > paddr=[80000000..8003cfff] > vaddr=[e0000000..e003cfff] > virt_entry=e0000000 > ELF-loading image 'capdl-loader-experimental' > paddr=[8003d000..8158dfff] > vaddr=[10000..1560fff] > virt_entry=18484 > Enabling hypervisor MMU and paging > Jumping to kernel-image entry point... > > Bootstrapping kernel > Total 28 IOASID set up > Region [c to 28) for SMMU caps > Booting all finished, dropped to user space > > > > From: Devel <devel-bounces(a)sel4.systems> on behalf of Daniel Wang <danielwang.ksu(a)gmail.com> > Sent: Friday, March 2, 2018 7:47 AM > To: devel(a)sel4.systems > Subject: [seL4] seL4 VMM Hangs during loading time > > Hi all, > > I’m trying to run seL as a microvisor following the CAMKES-ARM-VM. My development board is TK1-SOM from ColoradoEngineering. I was able to flash the U-boot to to load seL4 HYP mode. However when I try to load the kernel. The system just hangs. I got stuck here any help would be appreciated thank you! > > I built the capdl-loader-experimental-image-arm-tk1 > and can copied it to the TK1 MMC storage, then I followed the wiki to setup env bootm_boot_mode to nonsec. Attachment is the printout: > > ------------------------------------------------------------------------------------------- > U-Boot 2018.03-rc3-00090-g3990c9d (Mar 01 2018 - 14:33:40 -0500) > > TEGRA124 > Model: Colorado Engineering TK1-SOM > Board: CEI tk1-som > DRAM: 2 GiB > MMC: sdhci@700b0400: 1, sdhci@700b0600: 0 > Loading Environment from MMC... OK > In: > serial > Out: serial > Err: serial > Net: No ethernet found. > Hit any key to stop autoboot: 0 > Tegra124 (TK1-SOM) # setenv bootm_boot_mode nonsec > Tegra124 (TK1-SOM) # saveenv > Saving Environment to MMC... Writing to MMC(0)... OK > Tegra124 (TK1-SOM) # ext2ls mmc 0 > <DIR> > 4096 . > <DIR> > 4096 .. > <DIR> > 16384 lost+found > <DIR> > 4096 boot > <DIR> > 4096 bin > <DIR> > 4096 dev > <DIR> > 12288 etc > <DIR> > 4096 home > <DIR> > 4096 lib > <DIR> > 4096 media > <DIR> > 4096 mnt > <DIR> > 4096 opt > <DIR> > 4096 proc > > 62 README.txt > <DIR> > 4096 root > <DIR> > 4096 run > <DIR> > 12288 sbin > <DIR> > 4096 srv > <DIR> > 4096 sys > <DIR> > 4096 tmp > <DIR> > 4096 usr > <DIR> > 4096 var > > 150994944 testfile > > 20524388 capdl-loader-experimental-image-arm-tk1 > Tegra124 (TK1-SOM) # ext2load mmc 0 ${loadaddr} capdl-loader-experimental-image-arm-tk1 > 20524388 bytes read in 593 ms (33 MiB/s) > Tegra124 (TK1-SOM) # bootelf ${loadaddr} > CACHE: Misaligned operation at range [90000000, 90000014] > CACHE: Misaligned operation at range [90001000, 900091c4] > CACHE: Misaligned operation at range [900091c4, 900098d8] > CACHE: Misaligned operation at range [900198d8, 900198e0] > CACHE: Misaligned operation at range [900198e0, 91392ae0] > CACHE: Misaligned operation at range [91394000, 913a4820] > CACHE: Misaligned operation at range [913a4820, 913a8000] > ## Starting application at 0x90000000 ... > ELF loader: monitor mode init done > Copy monitor mode vector from 90001000 to a7f00000 size 50 > Number of IRQs: 192 > Load seL4 in nonsecure HYP mode 600001da > ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 > paddr=[90000000..913a7fff] > ELF-loading image 'kernel' > paddr=[60000000..6003cfff] > vaddr=[e0000000..e003cfff] > virt_entry=e0000000 > > ------------------------------------------------------------------------------------------- > > Best Regards > -Daniel Wang > > > >

1 0

seL4 VMM Hangs during loading time
by Daniel Wang 02 Mar '18

02 Mar '18

Hi all, I’m trying to run seL as a microvisor following the CAMKES-ARM-VM. My development board is TK1-SOM from ColoradoEngineering. I was able to flash the U-boot to to load seL4 HYP mode. However when I try to load the kernel. The system just hangs. I got stuck here any help would be appreciated thank you! I built the capdl-loader-experimental-image-arm-tk1 and can copied it to the TK1 MMC storage, then I followed the wiki to setup env bootm_boot_mode to nonsec. Attachment is the printout: ------------------------------------------------------------------------------------------- U-Boot 2018.03-rc3-00090-g3990c9d (Mar 01 2018 - 14:33:40 -0500) TEGRA124 Model: Colorado Engineering TK1-SOM Board: CEI tk1-som DRAM: 2 GiB MMC: sdhci@700b0400: 1, sdhci@700b0600: 0 Loading Environment from MMC... OK In: serial Out: serial Err: serial Net: No ethernet found. Hit any key to stop autoboot: 0 Tegra124 (TK1-SOM) # setenv bootm_boot_mode nonsec Tegra124 (TK1-SOM) # saveenv Saving Environment to MMC... Writing to MMC(0)... OK Tegra124 (TK1-SOM) # ext2ls mmc 0 <DIR> 4096 . <DIR> 4096 .. <DIR> 16384 lost+found <DIR> 4096 boot <DIR> 4096 bin <DIR> 4096 dev <DIR> 12288 etc <DIR> 4096 home <DIR> 4096 lib <DIR> 4096 media <DIR> 4096 mnt <DIR> 4096 opt <DIR> 4096 proc 62 README.txt <DIR> 4096 root <DIR> 4096 run <DIR> 12288 sbin <DIR> 4096 srv <DIR> 4096 sys <DIR> 4096 tmp <DIR> 4096 usr <DIR> 4096 var 150994944 testfile 20524388 capdl-loader-experimental-image-arm-tk1 Tegra124 (TK1-SOM) # ext2load mmc 0 ${loadaddr} capdl-loader-experimental-image-arm-tk1 20524388 bytes read in 593 ms (33 MiB/s) Tegra124 (TK1-SOM) # bootelf ${loadaddr} CACHE: Misaligned operation at range [90000000, 90000014] CACHE: Misaligned operation at range [90001000, 900091c4] CACHE: Misaligned operation at range [900091c4, 900098d8] CACHE: Misaligned operation at range [900198d8, 900198e0] CACHE: Misaligned operation at range [900198e0, 91392ae0] CACHE: Misaligned operation at range [91394000, 913a4820] CACHE: Misaligned operation at range [913a4820, 913a8000] ## Starting application at 0x90000000 ... ELF loader: monitor mode init done Copy monitor mode vector from 90001000 to a7f00000 size 50 Number of IRQs: 192 Load seL4 in nonsecure HYP mode 600001da ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 paddr=[90000000..913a7fff] ELF-loading image 'kernel' paddr=[60000000..6003cfff] vaddr=[e0000000..e003cfff] virt_entry=e0000000 ------------------------------------------------------------------------------------------- Best Regards -Daniel Wang

3 2

How to avoid timeout exceptions in non-buggy server code
by Kelly Dean 02 Mar '18

02 Mar '18

The article “Mixed-criticality support in seL4” at https://lwn.net/Articles/745946/ says seL4's solution to the problem of CPU budget exhaustion while in a non-reentrant shared data-structure server is timeout exceptions. The server might time out by chance, through no fault of its own. A more robust solution is to simply disallow calling any such server that advertises a WCET longer than the client's per-period CPU budget, and when a call is made, have the kernel check whether the client's remaining CPU budget ≥ server's WCET. If it is, then proceed with the call as normal. If it isn't, then verify that the client's per-period CPU budget ≥ server's WCET. If that verification succeeds, then terminate the budget for the client's current period early, and actually enter the server at the beginning of the client's _next_ period. (If the verification fails, then the kernel tells the client that the call is disallowed.) If the server fails to return before exhausting the client's CPU budget, then the server has violated its own WCET, which is a bug. Thus, a non-buggy server will never time out, so timeout exception handlers handle only bugs, not routine system operation. If the server's actual WCET is W, then from the client's point of view, the server's apparent WCET is almost 2W, because the client might make the call with remaining CPU budget X such that X is just barely less than W, in which case the kernel will terminate the client's current budget early (so the client loses X) and enter the server at the beginning of the next period, and the server might then take W to return, making the client wait X+W altogether (plus, of course, the remainder of the period, during which other VMs run). But with seL4's current solution, the server's apparent WCET is even longer than 2W, because the server could run for X, time out, be restarted (taking time R), then run for W, making the client wait X+R+W altogether.

2 5

Camkes limitations
by Sam Chenoweth 01 Mar '18

01 Mar '18

Hi, I like the Camkes (3) tool and believe it is essential for making seL4 accessible for developers. However, I have noticed some unexpected limitations that I believe are either bugs or incomplete features. Issue A: A hierarchical component cannot have a dataport with a custom data type. (However, a non-hierarchical component can have a dataport with a custom data type. Also, a hierarchical component can have a dataport with a built-in data type such as Buf.) Issue B: A dataport provided by a sub-component cannot be exported as a dataport belonging to the hierarchical component that contains it. (However, the export of event notifications from sub-components works just fine.) Attached is the relevant code that demonstrates both issues, which is a contrived example to highlight the issues without other stuff getting in the way. Please note that the code as is compiles just fine, however if you comment and uncomment a few lines of code (as instructed in Duck.camkes, Duckherd.camkes and Duckling.camkes), the issues can be demonstrated (separately) as compile failures. There may be other issues with hierarchical components that I am not yet aware of, as the above issues (unfortunately) have prevented me from experimenting with them further. Could you please acknowledge if these are issues that you are aware of, and if there is likely to be a fix in a future Camkes 4 release? Regards, Dr Samuel Chenoweth Cyber Security Researcher DST Group Note: I would have sent this email from my work email address ( samuel.chenoweth(a)dst.defence.gov.au) however I sent it from my personal address instead because of issues to do with our email gateway. All the contents of this email are UNCLASSIFIED and non-sensitive.

2 1

seL4 in an SGX enclave?
by Corey Richardson 28 Feb '18

28 Feb '18

This is email is me being kinda lazy. Does anyone know how challenging this would actually be to pull off? I'm interested in looking into it, but can't for a while. I feel like it makes sense to bootload some little stub that sets up seL4 as the only enclave in the system. I don't see any reason to have multiple enclaves when using seL4. But, from this, it should be possible to get a good static root of trust remote attestation on Google Cloud. (And also, can finally implement https://www.blackhat.com/docs/us-17/thursday/us-17-Swami-SGX-Remote-Attesta…) -- cmr http://octayn.net/ +16038524272

4 4

Fwd: CamkesVM CMA34CR_centos app
by Michal Podhradsky 21 Feb '18

21 Feb '18

Hi Kent, I did a fresh *repo init -u https://github.com/seL4/camkes-vm-manifest <https://github.com/seL4/camkes-vm-manifest> * so I am using the latest default.xml Now I can get a bit further - although still not all the way - here is the full output: https://gist.github.com/podhrmic/bc86178e60fad64ab870ff1fa19992 e3 and then the system as far as I can tell hangs - no serial or VGA output. What could be the cause? Regards M On Mon, Feb 19, 2018 at 4:07 PM, <Kent.Mcleod(a)data61.csiro.au> wrote: > Hi Michal, > > > Which revision of default.xml are you using? Adrian thinks it could be > potentially related to, and fixed by, this commit[1] if you don't have it > yet. > > > Kent > > > [1] https://github.com/seL4/seL4/commit/3d6f4f9bb7bfe42628df > a555601401fa4efcdf2d > > > > ------------------------------ > *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Michal Podhradsky > <mpodhradsky(a)galois.com> > *Sent:* Tuesday, February 20, 2018 9:37 AM > *To:* devel(a)sel4.systems > *Subject:* [seL4] CamkesVM CMA34CR_centos app > > Hi all, > > I have a CM34CR CPU module <https://wiki.sel4.systems/CMA34DBMC> and I am > trying to run the related camkes app on it. > > I choose the centos app: https://github.com/seL4/camkes > -vm/blob/master/apps/vm/cma34cr_centos.camkes > > I am using default camkes vm manifest from https://github.com/seL4/camkes > -vm-manifest. > > Compile with: > > *make clean * > > *make cma34cr_centos_defcondig * > > *make silentoldconfig * > *make* > > And then I create a bootable USB following instructions here > <https://wiki.sel4.systems/Hardware/IA32>. > > Then after I load the kernel and capdl image, I get the following output > on serial: > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > *Boot config: parsing cmdline 'sel4kernel' Boot config: console_port = > 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false > Detected 1 boot module(s): module #0: start=0xd34000 end=0x3b387e8 > size=0x2e047e8 name='rootserver' Parsing GRUB physical memory map > Physical Memory Region from 0 size 9d400 type 1 Physical Memory Region > from 9d400 size 2c00 type 2 Physical Memory Region from e0000 size > 20000 type 2 Physical Memory Region from 100000 size 1ff00000 type 1 > Adding physical memory region 0x100000-0x20000000 Physical Memory > Region from 20000000 size 200000 type 2 Physical Memory Region from > 20200000 size 1fe04000 type 1 Adding physical memory region > 0x20200000-0x40004000 Physical Memory Region from 40004000 size 1000 > type 2 Physical Memory Region from 40005000 size 64bab000 type 1 Adding > physical memory region 0x40005000-0xa4bb0000 Physical Memory Region > from a4bb0000 size 1400000 type 2 Physical Memory Region from a5fb0000 > size 4a0f000 type 1 Adding physical memory region 0xa5fb0000-0xaa9bf000 > Physical Memory Region from aa9bf000 size 500000 type 2 Physical Memory > Region from aaebf000 size 100000 type 4 Physical Memory Region from > aafbf000 size 40000 type 3 Physical Memory Region from aafff000 size > 1000 type 1 Adding physical memory region 0xaafff000-0xab000000 > Physical Memory Region from ab000000 size 4a00000 type 2 Physical > Memory Region from f0000000 size 4000000 type 2 Physical Memory Region > from feb00000 size 4000 type 2 Physical Memory Region from fec00000 > size 1000 type 2 Physical Memory Region from fed10000 size a000 type 2 > Physical Memory Region from fed1c000 size 4000 type 2 Physical > Memory Region from fee00000 size 1000 type 2 Physical Memory Region > from ffc00000 size 400000 type 2 Physical Memory Region from 100000000 > size 14f600000 type 1 Adding physical memory region 0x100000000-0x24f600000 > Got VBE info in multiboot. Current video mode is 16767 ACPI: RSDP > paddr=0xfe020 ACPI: RSDP vaddr=0xfe020 ACPI: RSDT paddr=0xaafda0c4 ACPI: > RSDT vaddr=0xaafda0c4 Kernel loaded to: start=0x100000 end=0xc17000 > size=0xb17000 entry=0x101269 ACPI: RSDT paddr=0xaafda0c4 ACPI: RSDT > vaddr=0xaafda0c4 ACPI: FADT paddr=0xaaffb000 ACPI: FADT vaddr=0xaaffb000 > ACPI: FADT flags=0x3c6a5 ACPI: DMAR paddr=0xaafde000 ACPI: DMAR > vaddr=0xaafde000 ACPI: IOMMU host address width: 36 ACPI: registering > RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: > registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 > ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x14 > fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 > dev=0x2 fun=0x0 ACPI: 2 IOMMUs detected ACPI: MADT paddr=0xaaff9000 ACPI: > MADT vaddr=0xaaff9000 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 > ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x1 ACPI: MADT_APIC > apic_id=0x2 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC > apic_id=0x3 ACPI: Not recording this APIC, only support 2 ACPI: MADT_IOAPIC > ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 > gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: 2 > CPU(s) detected ELF-loading userland images from boot modules: > size=0x41fc000 v_entry=0x409000 v_start=0x400000 v_end=0x45fc000 > p_start=0x3b39000 p_end=0x7d35000 Moving loaded userland images to final > location: from=0x3b39000 to=0xc17000 size=0x41fc000 Starting node #0 with > APIC ID 0 Mapping kernel window is done ========== KERNEL EXCEPTION > ========== Vector: 0xd ErrCode: 0x0 IP: 0xffffffff80115c04 SP: > 0xffffffff80a0bfa0 FLAGS: 0x10046 CR0: 0x80010013 CR2: 0x0 > (page-fault address) CR3: 0xa12000 (page-directory physical address) > CR4: 0x110668 Stack Dump: *0xffffffff80a0bfa0 == 0x0 > *0xffffffff80a0bfa8 == 0x0 *0xffffffff80a0bfb0 == 0x3b39000 > *0xffffffff80a0bfb8 == 0xffffffff80116b80 *0xffffffff80a0bfc0 == 0x0 > *0xffffffff80a0bfc8 == 0x22a8 *0xffffffff80a0bfd0 == 0x0 > *0xffffffff80a0bfd8 == 0x0 *0xffffffff80a0bfe0 == 0xffffffff80000000 > *0xffffffff80a0bfe8 == 0x7e000 *0xffffffff80a0bff0 == 0xaa24c70c > *0xffffffff80a0bff8 == 0x1f *0xffffffff80a0c000 == 0xfffffffff000ba86 > *0xffffffff80a0c008 == 0xffffffff8081f0c0 *0xffffffff80a0c010 == 0x0 > *0xffffffff80a0c018 == 0x0 *0xffffffff80a0c020 == 0x0 *0xffffffff80a0c028 > == 0x0 *0xffffffff80a0c030 == 0x0 *0xffffffff80a0c038 == 0x0 Halting... > halting... Kernel entry via Interrupt, irq 0 * > > Any pointers at what is the cause of error here? The machien runs normally > with vanilla CentOS so I don't think it is a hardware issue. Also, I am > assuming the CMA34CR is identical to the one you have on your side (at > least checking the lspci output against the camkes description the memory > regions etc seem to match). > > Thanks in advance. > M >

3 3

split.c bootstrap.c failure?
by Richard Clark 21 Feb '18

21 Feb '18

Hi! What is this error and how might I go about tracking down the cause? <<seL4(CPU 0) [decodeUntypedInvocation/167 T0xe0792100 "csm-threads" @3a98c]: Untyped Retype: Slot #15 in destination window non-empty.>> _refill_pool@split.c:177 Failed to retype untyped, error 8 vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1 alloc_and_map@bootstrap.c:103 Failed to allocate bootstrap frame, error: 1 What I've done, is taken over the usual sel4test process and turned it into a little process that starts a few others. This error occurs at near the beginning of the main process, after it has allocated some untyped space for a secondary process, and just started it running. There is tons of memory available everywhere, and I do not understand why this is failing.... clues? Thanks! Richard H. Clark ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

CamkesVM CMA34CR_centos app
by Michal Podhradsky 20 Feb '18

20 Feb '18

Hi all, I have a CM34CR CPU module <https://wiki.sel4.systems/CMA34DBMC> and I am trying to run the related camkes app on it. I choose the centos app: https://github.com/seL4/camkes-vm/blob/master/apps/vm/cma34cr_centos.camkes I am using default camkes vm manifest from https://github.com/seL4/camkes-vm-manifest. Compile with: *make clean* *make cma34cr_centos_defcondig* *make silentoldconfig* *make* And then I create a bootable USB following instructions here <https://wiki.sel4.systems/Hardware/IA32>. Then after I load the kernel and capdl image, I get the following output on serial: *Boot config: parsing cmdline 'sel4kernel'Boot config: console_port = 0x3f8Boot config: debug_port = 0x3f8Boot config: disable_iommu = falseDetected 1 boot module(s): module #0: start=0xd34000 end=0x3b387e8 size=0x2e047e8 name='rootserver'Parsing GRUB physical memory map Physical Memory Region from 0 size 9d400 type 1 Physical Memory Region from 9d400 size 2c00 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size 1ff00000 type 1Adding physical memory region 0x100000-0x20000000 Physical Memory Region from 20000000 size 200000 type 2 Physical Memory Region from 20200000 size 1fe04000 type 1Adding physical memory region 0x20200000-0x40004000 Physical Memory Region from 40004000 size 1000 type 2 Physical Memory Region from 40005000 size 64bab000 type 1Adding physical memory region 0x40005000-0xa4bb0000 Physical Memory Region from a4bb0000 size 1400000 type 2 Physical Memory Region from a5fb0000 size 4a0f000 type 1Adding physical memory region 0xa5fb0000-0xaa9bf000 Physical Memory Region from aa9bf000 size 500000 type 2 Physical Memory Region from aaebf000 size 100000 type 4 Physical Memory Region from aafbf000 size 40000 type 3 Physical Memory Region from aafff000 size 1000 type 1Adding physical memory region 0xaafff000-0xab000000 Physical Memory Region from ab000000 size 4a00000 type 2 Physical Memory Region from f0000000 size 4000000 type 2 Physical Memory Region from feb00000 size 4000 type 2 Physical Memory Region from fec00000 size 1000 type 2 Physical Memory Region from fed10000 size a000 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from ffc00000 size 400000 type 2 Physical Memory Region from 100000000 size 14f600000 type 1Adding physical memory region 0x100000000-0x24f600000Got VBE info in multiboot. Current video mode is 16767ACPI: RSDP paddr=0xfe020ACPI: RSDP vaddr=0xfe020ACPI: RSDT paddr=0xaafda0c4ACPI: RSDT vaddr=0xaafda0c4Kernel loaded to: start=0x100000 end=0xc17000 size=0xb17000 entry=0x101269ACPI: RSDT paddr=0xaafda0c4ACPI: RSDT vaddr=0xaafda0c4ACPI: FADT paddr=0xaaffb000ACPI: FADT vaddr=0xaaffb000ACPI: FADT flags=0x3c6a5ACPI: DMAR paddr=0xaafde000ACPI: DMAR vaddr=0xaafde000ACPI: IOMMU host address width: 36 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x14 fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x2 fun=0x0ACPI: 2 IOMMUs detectedACPI: MADT paddr=0xaaff9000ACPI: MADT vaddr=0xaaff9000ACPI: MADT apic_addr=0xfee00000ACPI: MADT flags=0x1ACPI: MADT_APIC apic_id=0x0ACPI: MADT_APIC apic_id=0x1ACPI: MADT_APIC apic_id=0x2ACPI: Not recording this APIC, only support 2ACPI: MADT_APIC apic_id=0x3ACPI: Not recording this APIC, only support 2ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xdACPI: 2 CPU(s) detectedELF-loading userland images from boot modules:size=0x41fc000 v_entry=0x409000 v_start=0x400000 v_end=0x45fc000 p_start=0x3b39000 p_end=0x7d35000Moving loaded userland images to final location: from=0x3b39000 to=0xc17000 size=0x41fc000Starting node #0 with APIC ID 0Mapping kernel window is done========== KERNEL EXCEPTION ==========Vector: 0xdErrCode: 0x0IP: 0xffffffff80115c04SP: 0xffffffff80a0bfa0FLAGS: 0x10046CR0: 0x80010013CR2: 0x0 (page-fault address)CR3: 0xa12000 (page-directory physical address)CR4: 0x110668Stack Dump:*0xffffffff80a0bfa0 == 0x0*0xffffffff80a0bfa8 == 0x0*0xffffffff80a0bfb0 == 0x3b39000*0xffffffff80a0bfb8 == 0xffffffff80116b80*0xffffffff80a0bfc0 == 0x0*0xffffffff80a0bfc8 == 0x22a8*0xffffffff80a0bfd0 == 0x0*0xffffffff80a0bfd8 == 0x0*0xffffffff80a0bfe0 == 0xffffffff80000000*0xffffffff80a0bfe8 == 0x7e000*0xffffffff80a0bff0 == 0xaa24c70c*0xffffffff80a0bff8 == 0x1f*0xffffffff80a0c000 == 0xfffffffff000ba86*0xffffffff80a0c008 == 0xffffffff8081f0c0*0xffffffff80a0c010 == 0x0*0xffffffff80a0c018 == 0x0*0xffffffff80a0c020 == 0x0*0xffffffff80a0c028 == 0x0*0xffffffff80a0c030 == 0x0*0xffffffff80a0c038 == 0x0Halting...halting...Kernel entry via Interrupt, irq 0* Any pointers at what is the cause of error here? The machien runs normally with vanilla CentOS so I don't think it is a hardware issue. Also, I am assuming the CMA34CR is identical to the one you have on your side (at least checking the lspci output against the camkes description the memory regions etc seem to match). Thanks in advance. M

2 2

CamkesVM: EthDriver and Firewall
by Michal Podhradsky 16 Feb '18

16 Feb '18

Hi all, I have some clarifying questions about the Ethernet driver <https://github.com/seL4/camkes-vm/tree/master/components/Ethdriver> and the Firewall <https://github.com/seL4/camkes-vm/tree/master/components/Firewall> components. 1. Does the ethernet driver return a raw ethernet frame and the consumer of the data has to strip the MAC header etc or does the driver return only payload (IP, ARP etc data)? 2. has the Firewall component been tested and does it work? (I know it is a part of CMA34_centos_defconfig but I don't have a way to test it right now) Thanks for the info. M

2 1

Idris now working on seL4
by jonas.cl＠protonmail.com 13 Feb '18

13 Feb '18

Hi, I am interested in both seL4 and Idris (https://www.idris-lang.org/ a dependently typed pure functional language), so I have written an seL4 project that compiles an "hello world" Idris application. My intention is to eventually write the seL4 tutorials using Idris. Any help, comments or contributions to the repositories is appreciated, especially to the idris-libsel4-ffi repo that currently is very limited. The following repositories are created to accomplish this: The project configuration https://github.com/mokshasoft/sel4-idris-manifest The app itself https://github.com/mokshasoft/sel4-idris-apps The Idris RTS (ported and built for seL4) https://github.com/mokshasoft/libsel4-idris-rts The libsel4 FFI (very limited implementation so far) https://github.com/mokshasoft/idris-libsel4-ffi Regards Jonas Sent from [ProtonMail](https://protonmail.com), Swiss-based encrypted email.

1 0

Re: [seL4] RefOS Building and Execution Error
by ALVI Aslam (MORPHO) 12 Feb '18

12 Feb '18

Hello Peter, Thank you for your support, I will try to run RefOS as per your instructions. I have also updated the RefOS at my local repo to make it runnable with default.xml And it working fine. If you want I can push my changes to you. Thanks & Regards, Aslam

2 1

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

Strange Behevior with cma34cr.
by Dan DaCosta 07 Feb '18

07 Feb '18

To Whom It May Concern: My name is Dan DaCosta and I am working with Rockwell on a smaccms transition project referred to as HTA. The manifest associated with this project can be found here: https://github.com/smaccm/hta This manifest is mostly concerned with targeting the cma34cr board. When building images using a Fedora 26 based OS that relies on gcc 7 the following fault occurs: FAULT HANDLER: data fault from vm.ethdriver.control (ID 0x202) on address > 0x1076878, pc = 0x4070d5, fsr = 0x6 > FAULT HANDLER: rip = 0x4070d5 > FAULT HANDLER: rsp = 0x1076880 > FAULT HANDLER: rax = 0 > FAULT HANDLER: rbx = 0xe68000 > FAULT HANDLER: rcx = 0x8 > FAULT HANDLER: rdx = 0x5 > FAULT HANDLER: rsi = 0xe61000 > FAULT HANDLER: rdi = 0xc > FAULT HANDLER: r8 = 0 > FAULT HANDLER: r9 = 0 > FAULT HANDLER: r10 = 0x16997e000 > FAULT HANDLER: r11 = 0x246 > FAULT HANDLER: r12 = 0 > FAULT HANDLER: r13 = 0x404a70 > FAULT HANDLER: r14 = 0 > FAULT HANDLER: r15 = 0 > FAULT HANDLER: rflags = 0x10246 > FAULT HANDLER: tls_base = 0 > FAULT HANDLER: memory map: > FAULT HANDLER: +-- 0x0000000001081fff -- > FAULT HANDLER: | guard page > FAULT HANDLER: +-- 0x0000000001081000 -- > FAULT HANDLER: | stack > FAULT HANDLER: +-- 0x000000000107d000 -- > FAULT HANDLER: | guard page > FAULT HANDLER: +-- 0x000000000107c000 -- > FAULT HANDLER: | <undescribed> > FAULT HANDLER: +-- 0x0000000001069fff -- > FAULT HANDLER: | guard page > FAULT HANDLER: +-- 0x0000000001069000 -- > FAULT HANDLER: | IPC buffer > FAULT HANDLER: +-- 0x0000000001068000 -- > FAULT HANDLER: | guard page > FAULT HANDLER: +-- 0x0000000001067000 -- > FAULT HANDLER: | <undescribed> > FAULT HANDLER: +-- 0x000000000105dfff -- > FAULT HANDLER: | code and data > FAULT HANDLER: +-- 0x0000000000400000 -- > The config I am primarily interested in is named "cma34cr_centos_defconfig" but I seem to have similar problems for all the cma34cr defconfigs. I was successful at building working images when I switched to building on Ubuntu 16.04 LTS. This distribution version uses gcc 5.4. Thanks! Dan DaCosta

2 1

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

30 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 28 Jan '18

28 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) 23 Jan '18

23 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 04 Jan '18

04 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 04 Jan '18

04 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

Dynamic Loading of application
by PANCHAL Vishalkumar (MORPHO) 18 Dec '17

18 Dec '17

Hello, Can we use ELF-Loader tool functions into the user_space application (here, main_app) to Dynamically load the image of other application (app-1, app-2, app-3) from external device ? [cid:image008.png@01D374F1.2B37E4A0] Regards, Vishal PANCHAL Software Engineer | Noida | R&D P : +91 (120) 4072 549 M. +91 94266 38316 E. vishalkumar.panchal(a)morpho.com<mailto:vishalkumar.panchal@morpho.com> [Idemia]<https://www.idemia.com/> Join us on [Facebook]<https://www.facebook.com/IdemiaGroup/> [Twitter]<https://twitter.com/IdemiaGroup> [LinkedIn]<https://www.linkedin.com/company-beta/3488/> [Youtube]<https://www.youtube.com/user/SafranMorpho/> [www.idemia.com]<https://www.idemia.com/> [OT-MORPHO is now IDEMIA] # " This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, you are notified that any dissemination, copying of this e-mail and any attachments thereto or use of their contents by any means whatsoever is strictly prohibited. If you have received this e-mail in error, please advise the sender immediately and delete this e-mail and all attached documents from your computer system." #

2 1

Questions concerning the capability management system
by Timotej Tomandl 18 Dec '17

18 Dec '17

Hi, while reading about seL4 I have found a presentation "The seL4 capability system" by Matthew P. Grosvenor (https://www.cl.cam.ac.uk/resea rch/security/ctsrd/cheri/workshops/pdfs/20160423-sel4-capabilities.pdf), sadly I was able to track down only the slides, not the talk itself. It mentions the "Aurora project", the constraint solver running in static memory + stack space, concerning itself with the capability allocation. There are these questions which popped into my mind: 1. Is the source code of the Aurora project available anywhere? Is there any more information than the presentation available? 2. Is the constraint solver still necessary with the current version of the API? 3. If it is still necessary, then - what is the necessary strength of the constraint solver? - is a design, in which either the root process or the microkernel itself has to include such a constraint solver in static memory + stack space necessary for a microkernel with the guarantees of seL4 or is it a side-effect of the design decisions? Regards, Timotej Tomandl

2 1

Questions about Tx1 Physical Memory usage
by Muneeswaran Rajendran 14 Dec '17

14 Dec '17

Hi all, I’m trying to understand the implementation details and physical memory usage of seL4 for Tx1 we have available physical memory in Tx1 is 6GB. DRAM (4GB) - available address range 8000_0000 - FFFF_FFFF DRAM2 (4GB to 6GB) - available address range - 1_0000_0000 - 2_7FFF_FFFF In the hardware.h file (/kernel/include/plat/tx1/plat/machine/hardware.h),the avail_p_regs[] ={.start = 0x80000000, .end = 0xa7f00000 } '1MiB starting from 0xa7f00000 is reserved by the elfloader for monitor mode hooks'.I understand from the code its required only for Tk1. (/projects/tools/elfloader-tool/src/plat/tk1/monitor.S). As per my understanding is not not applicable for Tx1 so we can use contiguous region of physical ram 2GB to 4GB. Also it's allow to use higher physical memory for seL4 kernel ie > 4GB ? Thanks in advance. Regards, Munees

2 1

Re: [seL4] UEFI support for x86
by Alexander Boettcher 12 Dec '17

12 Dec '17

Hello, On 04.12.2017 18:15, Edward Sandberg wrote: > I modified the demo.run file to use fb_boot_drv and built the uefi > image. I tested it on an UP board, a Minnowboard Turbot, a Dell M3800 > laptop, and a Dell Precision 5810 desktop. I was unable to get > graphical output on any of them. I have pasted the logs for all (except > the laptop which has no serial port) below. > * UP BOARD ******************************** > WARNING: no console will be available to OS > Bender: Hello World. > framebuffer at [80000000+808ca000) 1920x1200@32 > framebuffer at [80000000+808ca000) 1920x1200@32 good > [init -> fb_boot_drv] Framebuffer with 1920x1200x32 @ 0x80000000 type=1 pitch=7680 > [init] child "report_rom" announces service "Report" > [init -> fb_boot_drv] resource_request: ram_quota=4612096 If you see such a message, the driver or component in general will not continue. The specified memory for the driver seems to be too low, try to increase it. It should be something above 9.2M (7680 Byte * 1200 = 9.2 M + some memory for the driver). Maybe 10-11M should suffice. > * MinnowBoard *********************************** > framebuffer at [80000000+808ca000) 1920x1200@32 > framebuffer at [80000000+808ca000) 1920x1200@32 good > [init -> fb_boot_drv] Framebuffer with 1920x1200x32 @ 0x80000000 type=1 pitch=7680 > [init -> fb_boot_drv] resource_request: ram_quota=4612096 Same here, try increase the memory for the framebuffer. > * Dell Precision 5810 ************************************** > Bender: Hello World. > framebuffer at [f1000000+f1300000) 1024x768@32 > framebuffer at [f1000000+f1300000) 1024x768@32 good > > Boot config: parsing cmdline 'sel4 disable_iommu' > Boot config: console_port = 0x3f8 > Boot config: debug_port = 0x3f8 > Boot config: disable_iommu = true > module #0: start=0xf9b8000 end=0xffff228 size=0x647228 name='image.elf' > Physical Memory Region from 0 size a0000 type 1 > Physical Memory Region from 100000 size 997ae000 type 1 > Adding physical memory region 0x100000-0x1f800000 > Physical Memory Region from 998ae000 size 9ac000 type 2 > Physical Memory Region from 9a25a000 size 49000 type 3 > Physical Memory Region from 9a2a3000 size c71000 type 4 > Physical Memory Region from 9af14000 size 492000 type 2 > Physical Memory Region from 9b3a6000 size 65000 type 20 > Physical Memory Region from 9b40b000 size 1000 type 1 > Physical Memory Region from 9b40c000 size e000 type 2 > Physical Memory Region from 9b41a000 size 1be6000 type 1 > Physical Memory Region from a0000000 size 10000000 type 2 > Physical Memory Region from fed1c000 size 4000 type 2 > Physical Memory Region from ff000000 size 1000000 type 2 > Physical Memory Region from 1000000000 size 1760000000 type 1 > Physical memory region not addressable > Adding physical memory region 0x0-0x1f800000 > seL4 failed assertion '!p_region_overlaps(reg)' at /home/esandberg/projects/embedded/genode-17.11/genode-17.11/contrib/sel4-097171f475bff21223783e130445b9be6b3d1bb4/src/kernel/sel4/src/arn > halting... This is a assertion in the seL4 kernel. Probably it complains about that region overlap due to following lines > Adding physical memory region 0x100000-0x1f800000 > Adding physical memory region 0x0-0x1f800000 I'm not sure, whether here the Multiboot 2 information is incorrect or the parsing by the kernel is too strict. Here one would require some more investigation in the Multiboot 2 spec (overlapping regions are valid or not?) and on the target machine in grub2/uefi, potentially bender and the sel4 kernel. Thanks for testing and the infos. -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 4

seL4 bring up on inmate cell of jailhouse.
by Muneeswaran Rajendran 12 Dec '17

12 Dec '17

Hi, I would like to bring up seL4 on inmate cell of Tx1. The jailhouse is running successfully on Tx1 board. I have created root cell and not root cell configuration on jailhouse. I able to load seL4 image successfully on inmate cell then during execution its stuck in the while extracting the program header. I checked with jailhouse forum they suggested some one might have ported seL4 or L4 kernel on jailhouse.also informed that seL4 kernel need to rebuild with some patches. Somehow I do not find the patches for seL4 or Fiasco.OC kernel to bring up on jailhouse.Please share links if you any. Also experimented by changing the PHY_ADDR higher then 2G (0x80000000) configuration ie(0x90000000 to 0xF0000000) and (0x100000000 to 0x170000000) while booting from the u-boot I observed KERNEL DATA abort after boot strapping the kernel. It means that this address cannot accessible in the seL4 kernel. Case 1: 0x90000000 to 0xF0000000 sample logs: ------------------- Bootstrapping kernel KERNEL DATA ABORT! Faulting instruction: 0x1ca9c FAR: 0x90000000 ESR (DFSR): 0x96000044 halting... Kernel entry via Interrupt, irq 0 case 2: 0x100000000 to 0x170000000 It's throwing synchronous data abort during program header extraction. sample logs: ------------------ binaries/elf64: elf64_getNumProgramHeaders "Synchronous Abort" handler, esr 0x96000044 ELR: 82002c8c LR: 820031f4 x0 : 0000000100000000 x1 : 0000000000000000 x2 : 000000000022fc10 x3 : 00000000827a5d40 x4 : 0000000000000000 x5 : 00000000000db8ab x6 : 0000000082007948 x7 : 0000000082008578 x8 : 0000000082008570 x9 : 0000000000000008 x10: 000000000000000f x11: 00000000fed87118 x12: 0000000000000047 x13: 0000000000000040 x14: 0000000000000001 x15: 00000000fed33114 x16: 0000000000000000 x17: 0000000000000000 x18: 00000000fc82ede0 x19: 00000000827a5ff0 x20: 0000000000000002 x21: 0000000082000000 x22: 00000000fc832800 x23: 0000000000000002 x24: 00000000fedaa7fc x25: 0000000000000000 x26: 0000000000000000 x27: 00000000fc8322f0 x28: 0000000000000000 x29: 00000000827a5e80 someone can give suggestion or pointers how we can bring seL4 on Jailhouse. Regards, Munees

3 2

Dynamic Loading of application
by ALVI Aslam (MORPHO) 12 Dec '17

12 Dec '17

Hi everyone, Greetings, I'm just started with seL4. Current Progress: - I have built an application on top of seL4 as learning from tutorials, so this is my current design [seL4,My main_APP,App2,App1,App3] Here My main_App is my main application build on seL4 and App1, App2 and App3 are sub components link with My main_App.( Just like in Tutorial 4 of seL4). When i build and run , this is working fine, no issue with it. when i run make command first i build kernel then libraries, then App1 , App2, App3, then My main_app and in the end it generate a single image file to execute. My Question :- Can i dynamic load my sub components(App1, App2, App3) which is required by My_main_App in run time ? Can we do that in seL4 is yes then how ? i dont want my App1, App2 and App3 part of final image, I want to load them and run them separately using My_main _App? Thank you in Advance, Please Help. Regards, Aslam ALVI # " This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, you are notified that any dissemination, copying of this e-mail and any attachments thereto or use of their contents by any means whatsoever is strictly prohibited. If you have received this e-mail in error, please advise the sender immediately and delete this e-mail and all attached documents from your computer system." #

2 1

AARCH64 with CAMKES (Questions)
by Michael DeFrancis 06 Dec '17

06 Dec '17

Can camkes be used with ARM AARCH64? I am attempting to build a linux virtual machine on top of the zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm project as my reference point. When the build system attempts to generate camkes-gen.mk, it fails - displaying an error indicating that aarch64 is not a valid architecture specification for camkes. I see that valid arm options are aarch32 or arm_hyp. Is arm_hyp what I am looking for here? What would I need to do in order to strip the camkes dependencies out of the tk1 vmm project? Thanks, Mike D Computer Security Engineer - Intelligent Automation, Inc. (301)294-5263 ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

3 3

UEFI support for x86
by Edward Sandberg 04 Dec '17

04 Dec '17

Is there a plan to add UEFI support in seL4 for x86 hardware in the near future? Newer x86 boards are frequently UEFI only. It is possible to get around the lack of UEFI support, as I have done with the UP board: https://up-community.org/wiki/Hardware_Specification but I am hitting problems which I will detail below. When I compile using ia32_debug_xml_defconfig and boot using the resulting images the board fails to find the RSDP location. To fix this I had to modify the source code a bit: * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.h + #define UPBOARD_RSDP 0x5B161000 * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.c - acpi->rsdp = acpi_sig_search(acpi, ACPI_SIG_RSDP, strlen(ACPI_SIG_RSDP), - (void *) BIOS_PADDR_START, (void *) BIOS_PADDR_END); + acpi->rsdp = (void *)UPBOARD_RSDP; * seL4test/kernel/src/plat/pc99/machine/acpi.c - for (addr = (char*)BIOS_PADDR_START; addr < (char*)BIOS_PADDR_END; addr += 16) { + for (addr = (char*)0; addr < (char*)PPTR_BASE; addr += 16) { It would be handy to have this as a kernel parameter to cover cases where it is not successfully discovered automatically. With these changes I can boot the board and several tests pass but then I get stuck on INTERRUPT0001 (Test interrupts with timer). I don't get a test failure or an error the board just sits and makes no more progress. Someone had that test fail in this post: https://sel4.systems/pipermail/devel/2017-February/001328.html and the first recommendation was to check if the irq of the timer was correctly found. I booted the board into linux to find the correct irq which was listed as 0 in /proc/interupts. I added a printf to handleInterrupt in the kernel source, recompiled and when I booted seL4 I found that the irq reported to handleInterrupt is 125 (which sel4 reports as the max interrupt value) every time that function is called. Adding this printf also showed me that when the test hangs the board hasn't crashed or locked up as calls to handleInterrupt are made continuously. At this point I noticed that before any tests started to run several ACPI tables are not recognized: Parsing ACPI tables Skipping table FPDTD, unknown Skipping table FIDT<9c>, unknown Skipping table UEFIB, unknown Skipping table TPM24, unknown Skipping table LPIT^D^A, unknown Skipping table BCFG9^A, unknown Skipping table PRAM0, unknown Skipping table CSRTL^A, unknown Skipping table BCFG9^A, unknown Skipping table OEM0<84>, unknown Skipping table OEM1@, unknown Skipping table PIDVÜ, unknown Skipping table RSCI,, unknown Skipping table WDAT^D^A, unknown Warning: skipping table ACPI XSDT Maybe one or more of those tables needs to be loaded to handle interrupts properly. The LPIT table is conspicuous in the case of the timer test but I think other tests are likely to depend on the other tables. Any suggestions about porting this type of hardware? -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

4 10

seL4_Send vs. seL4_Call
by Stefan Wallentowitz 04 Dec '17

04 Dec '17

Hi everyone, I have built a very simple application that loads another process, which is very similar to the tutorials. For testing I wanted to send from the second process to the first one using seL4_Send and observe that the second process never continues after the seL4_Send blocked, despite the receiver called seL4_Recv and got the message. If I call seL4_Call and the receiver does seL4_Recv + seL4_ReplyRecv it works without any other changes to the code. I am wondering if I am understanding something fundamentally wrong and/or what the best strategy to debug this behavior is. Thanks for your help! Cheers, Stefan

2 1

camkes-gen.mk generated prerequisites
by Gordon Clark 01 Dec '17

01 Dec '17

We have a multi component camkes application with each component using a few common services and then having application interfaces to a small number of other components.All these components are imported into a top level system description camkes file. Examining the generated camkes I see that all the generated header and source files have exactly the same make prerequisites meaning a change to logically unrelated components causes them all to be regenerated and recompiled. Now I have discovered the camkes cache this is less of an issue but is there a better way we can structure our application to reduce the edit-compile-go cycle ? Regards Gordon

2 1

seL4SharedData
by Zippy Maniac 29 Nov '17

29 Nov '17

We have a security requirement on our ARM based product using CAmkES 2.2.x to ensure all sensitive data declared in specific seL4SharedData regions are erased on detection of a power failure. We achieve this by overwriting the data with a known pattern that we read back from a separate component before declaring the device as secured. This is working fine. But we need to guarantee that the overwrite data is actually written to DDR and we aren't just using cached values. This means flushing the L1 and L2 data caches specific regions. We could use seL4HardwareMMIO regions and declare our data in the memory map and use these regions as un-cached. Or use the _hardware_cached attribute and call the provided flush method when necessary. Our main issue with doing this, except the fiddle of mapping multiple different sized regions into the memory map, is we could potentially expose the physical locations of the sensitive data rather than having it wrapped in the virtual address space of a component. Having a flush method on seL4SharedData would be the ideal solution. We are not in a position to upgrade our CAmkES version on this product at the moment. Any thoughts? Zippy

4 3

Tx1 UART and GiC distributor PPTR address
by Muneeswaran Rajendran 27 Nov '17

27 Nov '17

Hi, The PPTR address range between UART and GIC distributor was 12k (kernel/include/plat/tx1/plat/machine/device.h). But when refer in TX1 reference sheet the length was specified as 64byte for UART,4k for GIC distributor and 8k for interrupt controller. can you please point out the reference or reason to choose this address for Tx1 board? /* These devices are used by the seL4 kernel. */ #define UARTA_PPTR 0xffffffffffff0000 #define GIC_DISTRIBUTOR_PPTR 0xffffffffffff3000 #define GIC_CONTROLLER_PPTR 0xffffffffffff4000 These addresses are used during kernel device map to access in the userspace map_kernel_devices : kernel_devices[i].paddr :0x50042000 kernel_devices[i].pptr 0xffffffffffff4000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f4 map_kernel_devices : kernel_devices[i].paddr :0x50041000 kernel_devices[i].pptr 0xffffffffffff3000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f3 map_kernel_devices : kernel_devices[i].paddr :0x70006000 kernel_devices[i].pptr 0xffffffffffff0000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f0 Regards, Munees

1 0

Caught cap fault in send phase at address 0x0 @Tx2
by Muneeswaran Rajendran 23 Nov '17

23 Nov '17

Hi seL4 Dev Team, I am bringing up the sel4 kernel on tx2 board with ref of Tx1. I encountered the TLB invalidation hang issue after kernel map window setup. I do not know the exact reason for hang so just disable that piece of code to look further execution of sel4 kernel. After that it dropped into the usersapce and throwing the cap fault or vm fault issue. Does anyone has come across this type of issue and how it debugged?. Please share your thought or pointers to debug this issue. I shared the full log details here. ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3 paddr=[82000000..827abfff] kernel_phys_start: 0xffffffff80000000 kernel_phys_end:0xffffffff8022fcdf load_elf : image_size 0x230000 ELF-loading image 'kernel' paddr=[80000000..8022ffff] vaddr=[ffffff8000000000..ffffff800022ffff] virt_entry=ffffff8000000000 load_elf : image_size 0x5e9000 ELF-loading image 'sel4test-driver' paddr=[80230000..80818fff] vaddr=[400000..9e8fff] virt_entry=41b160 Enabling MMU and paging Jumping to kernel-image entry point... kernel_info.virt_entry : 0x0 user_info.phys_region_start : 0xffffffff80230000 user_info.phys_region_end:0xffffffff80819000 user_info.virt_region_start:0x400000 user_info.virt_region_end:0x9e9000 user_info.phys_virt_offset:0x7fe30000 user_info.virt_entry:0x41b160 Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on code at address 0x41b160 with status 0x82000010 in thread 0xffffff8027ef4200 "rootserver" at address 0x41b160 With stack: halting... Kernel entry via VM Fault, fault type: 4305248 Thanks in advance Muneeswaran R

1 0

Tx1 SMP and Hypervisor support
by Muneeswaran Rajendran 17 Nov '17

17 Nov '17

Hi Sel4 Dev Team, Any update of SMP and Hypervisor feature which fully functional on TX2. If its not available when will get this feature supported . Regards, Munees

3 4

1:1 Mapping of Zynqmp devices
by Chris Guikema 16 Nov '17

16 Nov '17

Hello, I am attempting to port the camkes-arm-vm to the zynqmp platform. For the TK1 and Exynos platforms, the physical address of the hardware devices are well below the kernelBase of 0xe0000000. However, for the zynqmp, these hardware devices are greater than the kernel base. This causes the "map_emulated_device" function call to fail for the GIC and any other passthrough devices. sel4utils_reserve_range_at_no_alloc@vspace.c:589 Range not available at 0xff010000, size 0x1000 Assertion failed: res.res (/home/chrisguikema/seL4/NAMC/camkes-arm-vm/libs/libsel4arm-vmm/src/devices.c: map_device: 160) Is there a way to 1:1 map these devices, even if they are above the kernelBase? Thanks, Chris

2 1

loading and booting seL4 on a tegra Tx2
by Muneeswaran Rajendran 15 Nov '17

15 Nov '17

Hi, I am trying to bring up sel4 on tegra Tx2 platform using tegra Tx1 as reference. I tweaked the important changes of UART,Timer configuration and IRQ number and also GIC controller, GIC distributor configuration w.r.t Tx2 after loading and booting the Tx2 board sel4 enter into init kernel to initialize the kerenl memory map for GIC and UART devices then control transfer to user space. I underdtand from ref manual both Tx1 and Tx2 using the same clock and baud rate for UART configuration. ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3 paddr=[82000000..827abfff] kernel_phys_start: 0xffffffff80000000 kernel_phys_end:0xffffffff8022fcdf load_elf : image_size 0x230000 ELF-loading image 'kernel' paddr=[80000000..8022ffff] vaddr=[ffffff8000000000..ffffff800022ffff] virt_entry=ffffff8000000000 load_elf : image_size 0x5e9000 ELF-loading image 'sel4test-driver' paddr=[80230000..80818fff] vaddr=[400000..9e8fff] virt_entry=41b160 Enabling MMU and paging Jumping to kernel-image entry point... Also try to add debug print in the init kernel thread to understand the virtual memory set-up but its crashed with synchronous exception. It indicates that the UART driver till not available to log the messages this was seen in Tx1 and Tx2. Not able to check/debug further on this issue. Also experimented with various arbitrary address for UARTA_PPTR and GIC_PPTR because Tx1 UARTA has 64byte size in case of Tx2 its 1MB.but still nothing has improved the state remain same. I completely walk through the sel4 boot and arm MMU code.I do not see any board specific changes in this code apart from UART,GIC configuration and IRQ number. The assembly code of MMU mainly setting up TCR ,TTBR , TLB invalidation and pagetable setup for arma-57. Please let me know your thought on this issue and how do debug this kind of issue. Regards, Munees

2 2

loading and booting seL4test on a zynq7000
by Joel Svensson 13 Nov '17

13 Nov '17

Hello, I want to learn about seL4 so I am trying to get is started on the hardware I already have (a zynq 7000). I have generated the image: sel4test-driver-image-arm-zynq7000 Now I try to load that onto the zynq by executing these commands in XMD: connect arm hw rst fpga -f design_1_wrapper.bit source ps7_init.tcl ps7_init ps7_post_config dow sel4test-driver-image-arm-zynq7000 run All of the above seem to be successful. Then, I have a serial link hooked up to the board (uart) and there I get the following output (screen /dev/ttyUSB1 115200) : ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0 paddr=[10000000..103c881f] ELF-loading image 'kernel' paddr=[0..2afff] vaddr=[e0000000..e002afff] virt_entry=e0000000 But then nothing more. I am lost what to do from this position in order to continue exploring seL4. I don't even know if what I see is an indication of a problem or not. If anyone has experience in running seL4 on zynq and if you sit on knowledge you want to share, please fill me in. Thank you

2 6

CAmkES mutex Question
by Brandon, Jeffrey - 0553 - MITLL 06 Nov '17

06 Nov '17

Hi, I've been taking a look at mutex implementations in the camkes-app example and I had a question. In the mutex example here https://github.com/seL4/camkes/tree/master/apps/mutex suppose I wanted to extend to add a third component C I need to add the corresponding camkes, source, Kbuild, and Kconfig files and then I need to add connections to the master mutex.camkes file correct? My first intuition was to add a connector: Assembly { Composition{ . Connection seL4MyConnector connection(from c.lock, to b.lock); . } } But this yields and error saying something to the effect "seL4MyConnector expects one from endpoint and two are specified" To remedy this I added another lock component to B, and made a connection between C and this new lock B provides. The new lock being implemented by the same template. My Questions: In this scenario do A B and C still have access to the same mutex? If A has a lock on the mutex, then C requests a lock, will this cause A to be unable to release the lock? In my mental model I have three threads of control, one each for A B and C, if A has a lock and then C requests a lock, does this block B (when it receives a message from C and is now blocked on requesting the mutex)? Then when A tries to release, B is blocked and cannot release the mutex on A's behalf. To put it another way, does this mutex example rely on B having direct access to the templated code and there only being two components? Secondarily, in the lockserver example https://github.com/seL4/camkes/tree/master/apps/lockserver a situation is presented where three clients access a single mutex through a single server. Would there be an issue if one of the clients also acted as the server? So for instance if A implemented the three pairs of lock unlock functions instead of the server and then B and C used seL4RPCCall connections to A in order to access them, would there be any synchronization issues? I'm relatively new to this and am trying to build a system with the help of camkes and I want to make sure I understand this before I get too far. I don't want to be working under incorrect assumptions. Thanks for taking the time to read this. Sincerely, Jeff Brandon Associate Staff MIT Lincoln Laboratory Secure Resilient Systems and Technology Ph: +1 781.981.9233

3 2

PPTR address computation on Sel4 Kernel
by Muneeswaran Rajendran 05 Nov '17

05 Nov '17

Hi sel4 development team, I understand from the sel4 kernel the paddr and pptr used in the kernel framework to compute the page table entry. I found from ref manual GICD_PADDR defined as (ARM_PERIPHBASE (0x50040000) + 0x1000) 0x50041000 for that GIC_DISTRIBUTOR_PPTR used as 0xffffffffffff3000. This details was not able to see in the ref manual and other sel4 reference. Can someone help to understand the pptr calculation w.r.t sel4? Thanks in advance Munees

2 1

UART initialisation on seL4 @TX1
by Muneeswaran Rajendran 02 Nov '17

02 Nov '17

Hi sel4 development team, I understand from the seL4 kernel the initial printf message are not routed through sel4 platform uart driver. Because the sel4 UART driver initialisation happened later when seL4 Main kernel initialization is finished. till then sel4 kernel uses u-boot UART driver to route the message. This interpretation is correct as per my understanding. Also mentioned in code as well debug output available via serial interface after kernel init thread started. /* debug output via serial port is only available from here */ printf("Bootstrapping kernel\n"); It means that when sel4 kernel comes up with u-boot uart driver and then later using sel4 uart driver. Please correct me if any thing wrong here and throw some input. Regards, Munees

2 2

Re: [seL4] Devel Digest, Vol 41, Issue 33
by ashokk＠spanidea.com 31 Oct '17

31 Oct '17

Hi Kofi, I tried with go command, but it is not working, board is getting hang... U-boot> go 0x10000000## Starting application at 0x10000000 ... after these i am not able to access the board, i need to reset again... Thanks & RegardsAshok From: "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> To: devel(a)sel4.systems Sent: Monday, 30 October 2017 11:54 PM Subject: Devel Digest, Vol 41, Issue 33 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, 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. Re: Devel Digest, Vol 41, Issue 31 (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Sun, 29 Oct 2017 23:56:03 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] Devel Digest, Vol 41, Issue 31 Message-ID: <1509321363766.62194(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Ashokk, I believe if you replace the command, "bootelf 0x10000000" with "go 0x10000000", That should be all that's needed to boot a raw binary image -- lemme know how things go though~ -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

Re: [seL4] Devel Digest, Vol 41, Issue 31
by ashokk＠spanidea.com 30 Oct '17

30 Oct '17

Hi Kofi, Thanks for the steps, i am able to load sel4test-driver-image-arm-bcm2837 on RPI3. but my question is i generated a sel4test-driver-image-arm-bcm2837.bin(binary image) for RPI3 i want to load these image on RPI3, can you help me out to load these image on RPI3... Hardware/Rpi3 - seL4Wiki these steps are used to load elf image on RPI3.... but i want to load binary image on RPI3... | | | Hardware/Rpi3 - seL4Wiki | | | Thanks and Regards Ashokkumar From: "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> To: devel(a)sel4.systems Sent: Thursday, 26 October 2017 8:48 PM Subject: Devel Digest, Vol 41, Issue 31 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, 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. Re: Loading bin image on RPI3(Remainder) (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Thu, 26 Oct 2017 03:23:06 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] Loading bin image on RPI3(Remainder) Message-ID: <1508988186794.61071(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Ashokk, Thanks for pointing this issue out, and sorry I took so long to get back to you -- I've investigated and come up with a workaround until we can fix the underlying caching problem here: could you try following the instructions on this page? https://wiki.sel4.systems/Hardware/Rpi3#preview There should be a pre-built U-Boot binary image there which should successfully load your seL4 kernel image. Please let me know how things go~ -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 1

Re: [seL4] Loading bin image on RPI3(Remainder)
by Kofidoku.Atuah＠data61.csiro.au 26 Oct '17

26 Oct '17

Hi Ashokk, Thanks for pointing this issue out, and sorry I took so long to get back to you -- I've investigated and come up with a workaround until we can fix the underlying caching problem here: could you try following the instructions on this page? https://wiki.sel4.systems/Hardware/Rpi3#preview There should be a pre-built U-Boot binary image there which should successfully load your seL4 kernel image. Please let me know how things go~ -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

Some guidance when using AutoCorres.
by Dan DaCosta 25 Oct '17

25 Oct '17

seL4 Developers: Consider the following c structure declarations: struct foo_struct{ uint16_t subfield; }; struct bar_struct{ struct foo foo; }; I am wondering if anyone has any suggestions on how I might go about proving something like this: s[Ptr &(bar→[''foo_C'']) := subfield_C_update (λ_. b) (heap_MissionCommand_struct_C s (Ptr &(bar→[''foo_C''])))] = s[Ptr &(bar→[''missioncommand_C''])→subfield := b] where s of type lifted_globals, bar is of type foo_struct_C, and b is of type word16. I *think* it should be provable, i.e., "updating all of the foo field with a copy of what was there originally modulo some change to subfield is equivalent to making that change directly to the subfield." I apologize in for taking this "into the weeds" but some of the definitions being used are buried in the AutoCorres translation and I am unsure how to make my question more abstract. Thanks in Advance! Dan DaCosta

3 2

Booting seL4 in bbb (beaglebone black)
by Sathish Kumar Balasubramaniam -ERS, HCL Tech 24 Oct '17

24 Oct '17

I tried booting sel4test in bbb. but i got the following after u-boot. Any idea for this crash ? U-Boot# echo $loadaddr 0x82000000 U-Boot# fatload mmc 0 ${loadaddr} sel4test.bin reading sel4test.bin 4108544 bytes read in 245 ms (16 MiB/s) U-Boot# go ${loadaddr} ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2 paddr=[82000000..823fc81f] ELF-loading image 'kernel' paddr=[80000000..80036fff] vaddr=[f0000000..f0036fff] virt_entry=f0000000 ELF-loading image 'sel4test-driver' paddr=[80037000..80514fff] vaddr=[8000..4e5fff] virt_entry=21c9c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: unknown syscall 0xf0005 in thread 0xf7fec500 "rootserver" at address 0x18b60 With stack: 0x3d88a0: 0x84ac 0x3d88a4: 0x1711c 0x3d88a8: 0x46c0f 0x3d88ac: 0x0 0x3d88b0: 0x84ac 0x3d88b4: 0x172cc 0x3d88b8: 0x3e5224 0x3d88bc: 0x46c0f 0x3d88c0: 0x84ac 0x3d88c4: 0xecfc 0x3d88c8: 0x31 0x3d88cc: 0x0 0x3d88d0: 0x0 0x3d88d4: 0x0 0x3d88d8: 0x0 0x3d88dc: 0x0 ::DISCLAIMER:: ---------------------------------------------------------------------------------------------------------------------------------------------------- The contents of this e-mail and any attachment(s) are confidential and intended for the named recipient(s) only. E-mail transmission is not guaranteed to be secure or error-free as information could be intercepted, corrupted, lost, destroyed, arrive late or incomplete, or may contain viruses in transmission. The e mail and its contents (with or without referred errors) shall therefore not attach any liability on the originator or HCL or its affiliates. Views or opinions, if any, presented in this email are solely those of the author and may not necessarily reflect the views or opinions of HCL or its affiliates. Any form of reproduction, dissemination, copying, disclosure, modification, distribution and / or publication of this message without the prior written consent of authorized representative of HCL is strictly prohibited. If you have received this email in error please delete it and notify the sender immediately. Before opening any email and/or attachments, please check them for viruses and other defects. ----------------------------------------------------------------------------------------------------------------------------------------------------

2 2

Re: [seL4] sel4Test development Tx1 platform
by Kofidoku.Atuah＠data61.csiro.au 24 Oct '17

24 Oct '17

Hi Munees, I went through some methods for how to boot the seL4 kernel on a stock TX1 board yesterday and wrote this guide: https://wiki.sel4.systems/Hardware/jetsontx1 It goes through the steps for getting seL4 booted using an SD Card, the internal 15GiB mass storage on the TX1, or using a USB cable and the DFU protocol.? DFU is probably a lot faster/better for you f you're doing active development. Could you try one of these methods and let me know if any of them works for you? -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 1

Loading bin image on RPI3(Remainder)
by ashokk＠spanidea.com 23 Oct '17

23 Oct '17

Hi all, I built a bin image from sel4test (https://github.com/seL4/sel4test).I am trying to load .bin image on RPI-3, but it's failing. I am following below steps... U-Boot> fatload mmc 0 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 329 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... i got stuck here... Along with this i also tried with two another methods but facing same issue..METHOD-1 :-==========U-Boot> fatload mmc 0 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> loadb 0x00200000 115200## Ready for binary (kermit) download to 0x00200000 at 115200 bps..U-Boot> load mmc 0:1 0x00200000 kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ...METHOD-2:- ===========U-Boot> load mmc 0:1 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... please guide me through this issue, i wanted to load kernel.bin(sel4test-driver-image-arm-bcm2837.bin) file on RPI-3.... RegardsAshok

1 0

Questions on seL4's scheduling
by Norrathep Rattanavipanon 20 Oct '17

20 Oct '17

Hello, I have a few questions about seL4's scheduling model in the main (formally verified) branch. 1) I see the time slice parameter in make menuconfig. Is that where I can change the scheduler's time slice correct? And the unit is in timer tick period I suppose? 2) I kind of remember the discussion we had that if an interrupt handler has lower priority than the currently running task, then the interrupt wouldnt happen. So what if both of them have the same priority, would the kernel schedule the currently running task until it uses up all of its timeslice, then issues the interrupt notification or would the interrupting process get executed right away? Best Regards, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

4 11

64 bit ARM ELF image load in Tx1 platform
by Muneeswaran Rajendran 18 Oct '17

18 Oct '17

Hi All, I have been trying to load 64bit seL4 (kernel+user space) ELF image on Tx1 board but it's failed to start the application and crashed with reason '"Synchronous Abort" handler, esr 0x02000000' always. Just walk through the Tx1 u-boot code and found that 'load_elf_image_phdr(unsigned long addr)' is using 32bit ELF header structure pointer to load the program header. I would like to understand whether 64bit ELF image load handled using 32bit elf header itself or we need to configure u-boot to load 64 bit ELF image ? I have modified the kernel base addr as 0xffffffc000080000 and phyadd as 0x80080000 to boot sel4 app image on TX1 board nothing has worked out. Please share details if someone succeeded to bring sel4 app elf image on Tx1 platform. Regards, Munees

4 5

Loading bin image on RPI3
by ashokk＠spanidea.com 17 Oct '17

17 Oct '17

Hi, I am trying to load .bin image on RPI-3, but i am not able to do that one i am following below steps... U-Boot> fatload mmc 0 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 329 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... i got stuck... Along with this i also tried with two another methods but facing same issue..METHOD-1 U-Boot> fatload mmc 0 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> loadb 0x00200000 115200## Ready for binary (kermit) download to 0x00200000 at 115200 bps..U-Boot> load mmc 0:1 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... METHOD-2 U-Boot> load mmc 0:1 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... please guide me through this issue, i wanted to load sel4test.bin(sel4test-driver-image-arm-bcm2837.bin) file on RPI-3.... RegardsAshok

1 0

sel4Test development Tx1 platform
by Muneeswaran Rajendran 13 Oct '17

13 Oct '17

Hi All I able to build sel4Test driver for TX1 platform. but the final outputimage is not a executable image it shows as data format :~/sel4Test$ file images/sel4test-driver-image-arm-tx1.bin images/sel4test-driver-image-arm-tx1.bin: data used 'aarch64-linux-gnu-' toolchain for cross compilation. but in the kernel obj shows as 64 bit ARM aarch64 format. ~/sel4Test$ file build/kernel/kernel.o build/kernel/kernel.o: ELF 64-bit LSB relocatable, ARM aarch64, version 1 (SYSV), not stripped And cross checked in the tk1 platform the generated output file as exe file format. ~/sel4Test$ file images/sel4test-driver-image-arm-tk1 images/sel4test-driver-image-arm-tk1: ELF 32-bit LSB executable, ARM, EABI5 version 1 (SYSV), statically linked, stripped Can you please someone help me to get final out image as executable format. Also share the procedure to load the sel4Test driver on TX1 board to verify the test. Thanks in advance Munees

3 6

does seL4 support NVIDIA Jetson Tx2 board ?
by ashokk＠spanidea.com 13 Oct '17

13 Oct '17

Hi , I am newbie to sel4 and currently working on one hobby project.I want to bring sel4 kernel on TX2 board. Can you guide me that is there any support available for tx2 for . If yes then provide some docs related to that. Thank you.

5 9

Re: [seL4] Devel Digest, Vol 41, Issue 11
by ashokk＠spanidea.com 11 Oct '17

11 Oct '17

Hi, I am going through the SEL4 userspace code of UART driver for TX1/TK1 board but i have some doubts in the below given link..https://github.com/seL4/util_libs/blob/master/libplatsupport/mach_inc… In serial.h file they are defining IRQ numbers #define UARTA_IRQ 68 #define UARTB_IRQ 69 #define UARTC_IRQ 78 #define UARTD_IRQ 122 I am not able to find the above IRQ numbers in TX1/TK1 datasheet...can you please point out where they are referring these IRQ numbers(68, 69, 78, 122)... RegardsAshok From: "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> To: devel(a)sel4.systems Sent: Tuesday, 10 October 2017 6:31 AM Subject: Devel Digest, Vol 41, Issue 11 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, 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. Re: TX1 user-space drivers (Kofidoku.Atuah(a)data61.csiro.au) 2. Re: sel4Test development Tx1 platform (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Mon, 9 Oct 2017 23:32:17 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] TX1 user-space drivers Message-ID: <1507591937169.95333(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Munees, I'm fairly sure that the TX1 can use the UART driver in there, since we have that driver in regression, being tested almost daily on a TX1 board -- that driver is the one used by seL4test on the TX1 in this test here: https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/… You also asked whether you have to migrate anything to the TX1. To my knowledge, no, because the TX1 is already running in regression internally, and that UART driver I linked you to is used by the TX1 port with no modifications. As for your question about the TX2, I cannot comment on whether or not the TX2 works the same as the TX1 because I have no experience with the TX2, since we do not have this board internally, and because seL4 does not officially support the TX2. If you want to port seL4 to the TX2, it would require some effort in figuring out what the differences between the TX1 and TX2 are, as far as I can tell :) -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 1

TX1 user-space drivers
by ashokk＠spanidea.com 10 Oct '17

10 Oct '17

Hi, I am trying write UART driver in SEL4 user-space driver for TX1 board.Shall i get any reference(docs or ref.code) to write these driver.. Thanks & RegardsAshok

3 3

SMP on Zynq7000 zc702
by Jesse Millwood 04 Oct '17

04 Oct '17

Hello, I realize that the only officially supported SMP platform is the i.mx6 but I did see some code on 6.0 to master for SMP and the zynq7000 so I am trying to test out some SMP functionality on my zc702 board. I am wondering if anyone has this working because my system is failing when compiling from master and the 6.0 and compatible tags. My second core seems to be coming up but the system ultimately fails and prints out: Bo ot nKgE RaNlEl L fDinAiTsAh eAdBO, RdT!r ppFaeud lttio nugs eirn stspraucctei o n: 0xe001d1b0 o FAR: 0xfffffff8 DFSR: 0x807 halting... Kernel entry via Syscall, number: 1, Call Cap type: 1, Invocation tag: 37 Which seems to be "Booting all finished, dropped to user space" from core0 and "KERNEL DATA ABORT!" from core1. The "0xe001d1b0" seems to be the label of the "idle_thread" function. While stepping through via JTAG, I have verified that core1 gets through "init_kernel" and then enters "restore_user_context" at some point in "restore_user_context" the fault registers as shown in the printed output are set. I think it is either in the c_exit_hook in restore_user_context or after the program branches to "0xFFF0010" which is "ldr pc,0xFFFF0030". This branches to the "arm_data_abort_exception" label, which goes to "kernel_data_fault" label and then to "kernel data abort". I'm having trouble exactly pin pointing where the fault occurs but it seems to be close to there. Has anyone had similar issues with SMP? It seems to get fairly far without setting the fault registers. I have tried to step through the execution over JTAG and here are some of my (verbose) notes | CORE0 Address | Core0 Function | Core0 Instruction | CORE1 Address | Core1 Function | Core1 Instruction | DFSR | DFAR | Note | |---------------+-----------------------------+------------------------+---------------+------------------------------------+----------------------+------------+------------+------| | 0x10000000 | label: start | =cpsid aif= | 0xFFFFFF34 | | =mvn r0,#0x0f= | 0x00000000 | 0x00005000 | | | 0x10003A2C | call: platform_init | =bl -x10003DD8= | 0xFFFFFF30 | | =wfe= | 0x00000000 | 0x00005000 | | | 0x10003ACC | call: smp_boot | =bl 0x100039FC= | 0xFFFFFF34 | | =mvn r0,#0x0f= | 0x00000000 | 0x00005000 | | | 0x10003ADO | ret: smp_boot | =bl 0x10005C54= | 0x10000020 | in: non_boot_core | =orr r0,r0,#0x40= | 0x00000000 | 0x00005000 | 2 | | 0x10003ADC | =if(is_hyp_mode())= | =beq 0x10003AF0= | 0x10002200 | label: arm_disable_dcaches | =push {r14}= | 0x00000000 | 0x00005000 | | | 0x10003AFC | call: arm_enable_mmu | =bl 0x10002174= | 0xE0006190 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 | | 0xE0001D70 | label: init_kernel | =push {r11,r14}= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 | | 0xE0001814 | label: try_init_kernel | =push {r11,r14}= | 0xE0001690 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 | | 0xE0001B80 | call: create_initial_thread | =str r0, [r11,#-0x14]= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 | | 0xE0001C48 | call: SMP_COND_STATEMENT | =bl 0xE0003C20= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1, 3 | | 0xE0001C4C | call: SMP_COND_STATEMENT | =bl 0xE00017D8= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1, 4 | | 0xE0001C50 | NODE_LOCK_SYS | =bl 0xE0019280= | 0xE0019288 | in: getCurrentCPUIndex | =sub r13,r13,#0x8= | 0x00000000 | 0x00005000 | 5 | | 0xE0001D1C | call: arch_pause | =bl 0xE0019DB0= | 0xE0019290 | in: getCurrentCPUIndex | =str r0,[r11,#-0x8]= | 0x00000000 | 0x00005000 | 6 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE00037F4 | in: init_core_state | =pop {r4,r11,pc}= | 0x00000000 | 0x00005000 | | | 0xE0001D20 | in: clh_lock_acquire | =mov r2,#0xE800= | 0xE0003754 | in: init_core_state | =movw r2,#0xE8E0= | 0x00000000 | 0x00005000 | 7 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE00017C4 | in: try_init_kernel_secondary | =mov r3,#0x1= | 0x00000000 | 0x00005000 | 8 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE002A06C | in: schedule | =push {r11,r14}= | 0x00000000 | 0x00005000 | 9 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE002979C | in: activateThread | =push {r11, r14}= | 0x00000000 | 0x00005000 | 10 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE001D24C | label: Arch_activateIdleThread | =push {r11}= | 0x00000000 | 0x00005000 | 11 | | 0xE0001D38 | in: clh_lock_acquire | =ldr r3,[r3,#0x4]= | 0xE0000054 | in: start | =b 0xE001CEC8= | 0x00000000 | 0x00005000 | 12 | Notes 1. Core1 is in a =while (!node_boot_lock)= loop 2. In =smp_boot=, CORE1 changes after =init_cpus= (branch location: ZSR:10003A08) - In =smp_boot=, =boot_cpus= is called - This sets the =CPU_JUMP_PTR= =*((volatile uint32_t*)CPU_JUMP_PTR) = (uint32_t)entry;= - calls =dsb= (data synchronization barrier) - After this call, CPU1 goes to =FFFFFF2C: dsb sy= - And then =sev= - After this call, CPU1 goes to the =non_boot_core= label - SEV - SEV causes an event to be signaled to all cores within a multiprocessor system. If SEV is implemented, WFE must also be implemented. - WFE - If the Event Register is not set, WFE suspends execution until one of the following events occurs: - an IRQ interrupt, unless masked by the CPSR I-bit - an FIQ interrupt, unless masked by the CPSR F-bit - an Imprecise Data abort, unless masked by the CPSR A-bit - a Debug Entry request, if Debug is enabled - an Event signaled by another processor using the SEV instruction. - If the Event Register is set, WFE clears it and returns immediately. - If WFE is implemented, SEV must also be implemented. - After CPU0 executes =arm_enable_mmu()= from the =main= function - by the end of =smp_boot= core1 is just starting =non_boot_main= 3. The =SMP_COND_STATEMENT= is calling =clh_lock_init= 4. The =SMP_COND_STATEMENT= is calling =release_secondary_cpus= 5. right after Core0 returned from releasing secondary cpus - First time Core1 has exited the loop - Core1's stack is - =getCurrentCPUINdex= - =init_core_state= - =try_init_kernel_secondary_core= - =init_kernel= 6. Core0 is in a =while(big_kernel_lock.node_owners[cpu].next->value ! = CLHState_Granted)= - Core0 is in a static inline function =clh_lock_acquire= in =try_init_kernel= - Core1 is in =getCurrentCPUIndex= but being called from =tcbDebugAppend= - =tcbDebugAppend= is being called from a =for= loop in =init_core_state= 7. Core0 is still in the previously mentioned while loop - Core1 is in "init_core_state" and has exited the for loop that called =tcbDebugAppend(NODE_STATE_ON_CORE(ksIdleThread, i))= 8. Core0 is still in the previously mentioned while loop - Core1 has returned to =try_init_kernel_secondary_core= from =init_core_state= and is at the end of the function 9. Core0 is still in the previously mentioned while loop - Core1 has entered the =init_kernel= call and then the =schedule= function. 10. Core0 is still in the previously mentioned while loop - Core1 has entered the =activateThread= call after =schedule= in =init_kernel= 11. Core0 is still in the previously mentioned while loop - Core1 seems to have dropped into the =case ThreadState_IdleThreadState:= case when switching on =switch (thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState))= - This was in =activateThread= 12. Core0 is still in the previously mentioned while loop - Core1 has exited =init_kernel= and is now branching to =restore_user_context= To test everything out I am using the "camkes-sols-master" manifest and building the "CAmkES Hello World application with events and dataports". The changes I made are * I edited the top level CAmkES file to set the affinity for two separate cores. * Upped the Max Number of CPU nodes to 2 The rest of the config is pretty standard. I have it attached to this message. The FSBL and ps7_init script I use are the standard ones created for the zc702 from the 2017.2 version of the Xilinx XSDK. I am booting from jtag and first run the ps7_init script and then flash the fsbl and then the "capdl-loader-experimental-image-arm-zynq7000" that was built. I am wondering if anyone is using a modified fsbl or ps7_init that does something else, if there is config value that I missed, or if it is still in development? If it is still in development I'd like to work with whoever is Thanks, Jesse Millwood

3 4

Question about IO ports in CAmKES
by John Backes 04 Oct '17

04 Oct '17

I have a question about the Real-time Clock component (RTC) for the x86 VMM found here: https://github.com/SEL4PROJ/global-components/blob/master/components/RTC/RT… Here is the text of the camkes file: import <RTC.idl4>; import <PutChar.idl4>; component CMOS { hardware; provides IOPort cmos_address; provides IOPort cmos_data; attribute string cmos_address_attributes = "0x70:0x70"; attribute string cmos_data_attributes = "0x71:0x71"; } component RTC { provides RTC rtc; maybe uses PutChar putchar; uses IOPort cmos_address; uses IOPort cmos_data; attribute int heap_size = 0; /* Connect the hardware RTC to the RTC component */ composition { component CMOS cmos; connection seL4HardwareIOPort rtc_cmos_address(from cmos_address, to cmos.cmos_address); connection seL4HardwareIOPort rtc_cmos_data(from cmos_data, to cmos.cmos_data); } configuration { cmos.cmos_address_attributes <- cmos_address_attributes; cmos.cmos_data_attributes <- cmos_data_attributes; } } What is the meaning of the last two statements in the configuration block? what is the scoping rules for the "cmos_address_attributes" and "cmos_data_attributes" variables? It looks like these attributes are already set in the definition of the CMOS component? They seemed to be assigned again in the configuration block? - John

2 2

SEL4 on Rasperry pi 3
by ashokk＠spanidea.com 04 Oct '17

04 Oct '17

Hi, I successfully compiled and run sel4 image for rasperry pi 3. while running it successfully passes all the tests,then it stopped now what? I need to bring sel4 kernel on top of rasperry pi 3... do you guys have any idea or links please share with me.. i am following below link..https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ RegardsAshok

2 1

Re: [seL4] seL4 website down
by Mike Clark 02 Oct '17

02 Oct '17

Yes, it appears to be down. Mike On Oct 2, 2017 12:39 PM, <keith(a)matellio.com> wrote: Is it just me or is everyone having trouble accessing the seL4 website? I’m getting the following: MOD_PYTHON ERROR ProcessId: 29222 Interpreter: 'sel4.systems.keg.ertos.in.nicta.com.au' ServerName: 'sel4.systems.keg.ertos.in.nicta.com.au' DocumentRoot: '/var/www/seL4/content' URI: '/Community/mailman/home.pml' Location: '/Community' Directory: None Filename: '/var/www/seL4/content/Community/mailman/home.pml' PathInfo: None Phase: 'PythonHandler' Handler: 'ertos' Traceback (most recent call last): File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1537, in HandlerDispatch default=default_handler, arg=req, silent=hlist.silent) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1202, in _process_target module = import_module(module_name, path=path) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 304, in import_module return __import__(module_name, {}, {}, ['*']) File "/var/www/seL4/code/ertos.py", line 9, in <module> from bib import html_bib, html_abstract, yearlist, get_bibtex File "/var/www/seL4/code/bib.py", line 11, in <module> rg = cfg.get('core', 'rg') File "/usr/lib/python2.7/ConfigParser.py", line 618, in get raise NoOptionError(option, section) NoOptionError: No option 'rg' in section: 'core' Keith _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel

2 1

seL4 website down
by keith＠matellio.com 02 Oct '17

02 Oct '17

Is it just me or is everyone having trouble accessing the seL4 website? I'm getting the following: MOD_PYTHON ERROR ProcessId: 29222 Interpreter: 'sel4.systems.keg.ertos.in.nicta.com.au' ServerName: 'sel4.systems.keg.ertos.in.nicta.com.au' DocumentRoot: '/var/www/seL4/content' URI: '/Community/mailman/home.pml' Location: '/Community' Directory: None Filename: '/var/www/seL4/content/Community/mailman/home.pml' PathInfo: None Phase: 'PythonHandler' Handler: 'ertos' Traceback (most recent call last): File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1537, in HandlerDispatch default=default_handler, arg=req, silent=hlist.silent) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1202, in _process_target module = import_module(module_name, path=path) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 304, in import_module return __import__(module_name, {}, {}, ['*']) File "/var/www/seL4/code/ertos.py", line 9, in <module> from bib import html_bib, html_abstract, yearlist, get_bibtex File "/var/www/seL4/code/bib.py", line 11, in <module> rg = cfg.get('core', 'rg') File "/usr/lib/python2.7/ConfigParser.py", line 618, in get raise NoOptionError(option, section) NoOptionError: No option 'rg' in section: 'core' Keith

1 0

Integer overflow bug in capdl-loader
by Jeff Kubascik 29 Sep '17

29 Sep '17

Hello, I am working with seL4 7.0.0 on the zynq7000 platform. I have come across a bug that occurs when a device physical memory region includes the highest address, i.e. where the memory region ends at 0xFFFFFFFF on 32 bit systems. When I create a CAmkES component that uses the highest address, I see the following error. ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0 paddr=[10000000..100ac81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'capdl-loader-experimental' paddr=[33000..1aefff] vaddr=[8000..183fff] virt_entry=befc Enabling MMU and paging Bootstrapping kernel Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/210 T0xffdfd100 "rootserver" @8fa8]: Untyped Retype: Insufficient memory (1 * 4096 bytes needed, 0 bytes available).>> Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() [Err seL4_NotEnoughMemory]: I have traced this problem to an integer overflow bug in the capdl-loader. The patch below shows how I have addressed this error. >From 22c9dd76a31713c98710830c2ea865a4e5d8a078 Mon Sep 17 00:00:00 2001 From: Jeff Kubascik <jeff.kubascik(a)dornerworks.com> Date: Wed, 27 Sep 2017 13:52:36 -0400 Subject: [PATCH] Fixed integer overflow bug in capdl-loader that occurs when a device physical memory region ends at 0xFFFFFFFF --- capdl-loader-app/src/main.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index 34eedb0..305da2a 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -554,7 +554,7 @@ static int find_device_object(void *paddr, seL4_Word type, int size_bits, seL4_C /* Assume we are allocating from a device untyped. Do a linear search for it */ for (unsigned int i = 0; i < bootinfo->untyped.end - bootinfo->untyped.start; i++) { if (bootinfo->untypedList[i].paddr <= (uintptr_t)paddr && - bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) >= (uintptr_t)paddr + BIT(size_bits)) { + bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) - 1 >= (uintptr_t)paddr + BIT(size_bits) - 1) { /* just allocate objects until we get the one we want. To do this * correctly we cannot just destroy the cap we allocate, since * if it's the only frame from the untyped this will reset the -- 2.7.4 I have added a -1 to the end address calculations to fix the edge case when bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) is equal to 0x100000000, an integer overflow. The current statement is comparing the address of the next byte past the end of the memory region. My change is comparing the address of the last byte in the memory region. I have tested this fix on the zynq7000 and it works. However, I am not too familiar with the capdl-loader. Are there any problems with this fix that I have not considered? Thanks, Jeff Kubascik

2 2

ARM 64-bit Support in seL4
by keith＠matellio.com 29 Sep '17

29 Sep '17

Not sure if this is the best place to post this question but I noticed on the seL4 roadmap page on the website that 64-bit support for ARM is due out at the end of 3Q2017. Is that correct, and if so, can someone give me some hints of where to look for it in the repository?

4 3

sel4 on QEMU
by ashokk＠spanidea.com 28 Sep '17

28 Sep '17

Hi, I am trying to run sel4 on QEMU, i am following this steps(https://wiki.sel4.systems/Hardware/Qemu) make clean make optiplex9020_defconfig make silentoldconfig make but while doing make i am getting following error.. /home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c: In function ‘get_breakpoint_format’:/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:130:27: error: ‘seL4_InstructionBreakpoint’ undeclared (first use in this function) *break_type = seL4_InstructionBreakpoint; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:130:27: note: each undeclared identifier is reported only once for each function it appears in/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:131:19: error: ‘seL4_BreakOnRead’ undeclared (first use in this function) *rw = seL4_BreakOnRead; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:135:27: error: ‘seL4_DataBreakpoint’ undeclared (first use in this function) *break_type = seL4_DataBreakpoint; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:136:19: error: ‘seL4_BreakOnWrite’ undeclared (first use in this function) *rw = seL4_BreakOnWrite; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:146:19: error: ‘seL4_BreakOnReadWrite’ undeclared (first use in this function) *rw = seL4_BreakOnReadWrite; ^make[1]: *** [src/gdb_server/gdb.o] Error 1make: *** [libsel4camkes] Error 2 can you please give any solution to solve these errors.. RegardsAshok

2 2

Sel4 compilation error for RasperryPi-3
by ashokk＠spanidea.com 27 Sep '17

27 Sep '17

Hi I am trying to cross-compile sel4 for rasperry-pi-3. i am executing following command on sel4 kernel source to cross-compile. TOOLPREFIX=arm-linux-gnueabi- ARCH=arm PLAT=bcm2837 ARMV=armv8-a CPU=cortex-a53 i am getting following error while doing make [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] 32/mode/api/shared_types_gen.h [CPP] src/arch/arm/armv/armv8-a/32/machine_asm.s_pp In file included from src/arch/arm/armv/armv8-a/32/machine_asm.S:11:0: ./include/config.h:17:22: fatal error: autoconf.h: No such file or directory compilation terminated. make: *** [src/arch/arm/armv/armv8-a/32/machine_asm.s_pp] Error 1 rm 32/mode/api/shared_types_gen.h plat/machine/hardware_gen.h arch/object/structures_gen.h is there any solution for this... RegardsAshok

2 1

General question about software
by Raymond Jennings 26 Sep '17

26 Sep '17

So, I know that at a basic level, a block device driver would probably need I/O permissions, and I'm guessing that it would be handling requests from a file system driver. Is that basically how the seL4 software ecosystem is laid out? What's typical for how "software in the wild" is actually organized and layered on top of the microkernel? I only know about seL4 from a theoretical standpoint, read the manual and stuff, and mostly familiar with the actual kernel, but I'm a complete noob when it comes to actual software.

3 2

Raspberry pi 3 compilation error
by Prathamesh Rahate 26 Sep '17

26 Sep '17

Hi, I am trying to cross-compile seL4 for rapsberry pi 3 using steps mentioned hereseL4 on the Raspberry Pi 3 | | | seL4 on the Raspberry Pi 3 | | | I am getting following error while compiling, are there any patches available to fix this error: [STAGE] libsel4sync.a[libs/libsel4sync] done.[apps/sel4test-tests] building... [HEADERS] [STAGE] test_init_data.h [STAGE] arch/* [STAGE] arch_frame_type.h [STAGE] autoconf.h [CC] src/helpers.o [CC] src/main.o [CC] src/tests/multicore.o [CC] src/tests/preempt.o [CC] src/tests/serial_server.o [CC] src/tests/breakpoints.o [CC] src/tests/scheduler.o [CC] src/tests/pagetables.o [CC] src/tests/inc_untyped.o [CC] src/tests/interrupt.o [CC] src/tests/sync.o [CC] src/tests/iopt.o [CC] src/tests/ioports.o [CC] src/tests/vspace.o [CC] src/tests/ipc.o [CC] src/tests/schedcontext.o [CC] src/tests/fpu.o [CC] src/tests/ept.o [CC] src/tests/trivial.o [CC] src/tests/binding.o [CC] src/tests/cnodeops.o [CC] src/tests/threads.o [CC] src/tests/cspace.o [CC] src/tests/regressions.o/tmp/cc7e2jo9.s: Assembler messages:/tmp/cc7e2jo9.s:120: Error: selected processor does not support ARM mode `ldrex r2,[r3]'/tmp/cc7e2jo9.s:154: Error: selected processor does not support ARM mode `strex r0,r3,[r2]'make[1]: *** [src/tests/regressions.o] Error 1make: *** [sel4test-tests] Error 2user@user-Lenovo:~/seL4test$ Thanks,Prathamesh

2 1

User-space drivers
by ashokk＠spanidea.com 25 Sep '17

25 Sep '17

Hi guys, This is Ashokkumar, i want to write a sample serial(UART) communication user-space driver in sel4,can i get any help from your side. I am just started sel4 i don't know how to build and execute the programs,if you have any documents or examples about user-space programs please share with me... RegardsAshok

2 1

Some questions regarding seL4, U-Boot, and Raspberry Pi 3 patches
by Austin Seipp 21 Sep '17

21 Sep '17

Hello *, I hope you're all doing well. I recently got seL4 running on my Raspberry Pi 3, and wanted to report some notes here and ask some questions regarding the port, and perhaps get some help working on a patch (or twelve, I'm sure.) Recently I followed the Data61 blog post here to get a recent copy of seL4 on my RPi, but hit a few errors along the way that burned some time. In particular I got burned by the U-Boot glitch and getting seL4 building due to a glitch in the 'repo' setup for sel4test: https://research.csiro.au/ tsblog/sel4-raspberry-pi-3/ I ended up writing my own blog post, with effectively "fully reproducible" instructions (e.g. one of the codepad.org links on the RPi3 wiki page was dead) for a recent build. This includes proper setup for uboot.env in order to `fatload` and `bootm` the seL4 ELF binary off disk, the right U-Boot version, and using Docker to build the seL4 image: https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html That's all fine, but... I got curious about this U-Boot glitch, as even a recent (git) copy of U-Boot still suffered from the issue reported in the original Data61 blog post. I found it strange this regression would exist for nearly 9 months, unless it was possibly something intentional (e.g. an intended behavioral change) or it went unreported. The glitch is this: after booting the seL4 binary, the system immediately hangs with no output after trying to start the sel4test application. This glitch did not occur in versions of U-Boot up-to v2017.01. Versions v2017.03 and later (to now) suffer. I decided to spend some time bisecting this problem and found the issue. Versions of U-Boot after v2017.01 include the following patch, which causes the data cache to be enabled prior to U-Boot loading and executing ELF binaries: https://github.com/thoughtpolice/u-boot/commit/ 995eab8b5b580b67394312b1621c60a71042cd18 This behavior previously existed as a workaround for QNX, which required that the dcache be disabled before execution. U-Boot, previously, disabled the dcache when booting *any* ELF binary at all (the binary can of course enable it or check to see if it isn't enabled already), as a simplistic workaround. This patch changes it to only disable the dcache on U-Boot images (uImages) marked as QNX ELF binaries, so that QNX systems boot properly still. It would seem then that seL4 -- or at least sel4test -- requires the dcache to be disabled upon entry for the RPi3. If the dcache is enabled, as in the above patch, it otherwise hangs immediately. In fact, a recent copy of U-Boot *can* execute seL4 properly: you simply have to use `./tools/mkimage` inside U-Boot to mark the application as `mkimage -C none -A arm -T kernel -O qnx -d <input> <output>` first -- this creates a uImage with the appropriate header to mark the ELF as a QNX binary. U-Boot recognizes this and appropriately disables the dcache before application entry, once you use `bootm` or something. I took the time to write a patch to U-Boot in order to add a new OS definition -- "sel4" -- in order to address this problem more clearly. My change is here: https://github.com/thoughtpolice/u-boot/commit/ 720caf6c398584658abfa883d4d390f4b6200269 With this change, you can mark any seL4 binary as `-O sel4` to create an appropriately bootable uImage, with the dcache appropriately disabled. Assuming this is in place, the following U-Boot commands will execute seL4: U-Boot> setenv bootfile uImage U-Boot> fatload mmc 0 ${loadaddr} ${bootfile} U-Boot> bootm ${loadaddr} ## Booting kernel from Legacy Image at 00200000 ... Image Name: Image Type: ARM seL4 Kernel Image (uncompressed) Data Size: 3385548 Bytes = 3.2 MiB Load Address: 00000000 Entry Point: 00000000 Verifying Checksum ... OK Loading Kernel Image ... OK CACHE: Misaligned operation at range [20000000, 200078bc] CACHE: Misaligned operation at range [200078bc, 2032a720] CACHE: Misaligned operation at range [2032c000, 2033c820] ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[20000000..2033c81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[33000..44dfff] vaddr=[10000..42afff] virt_entry=2a03c Enabling MMU and paging Jumping to kernel-image entry point... ---- So with that all done, it's clear there's a change needed *somewhere* but I'm not sure where or what to do: 1) Is the above the right approach? Clearly, seL4 on the RPi3 assumed a disabled dcache during its development, but this has now changed, so for this platform something will need to be fixed, such as the above. 2) Or perhaps this is not a U-Boot problem, but should be fixed in seL4. Or in sel4test. For example, is there an option to assume the dcache is already enabled in the configuration? Maybe that should be toggled instead. Or does seL4 *always* assume it is disabled at boot? What about non-RPi3 platforms like other ARM systems? These likely use U-Boot as well, but it's unclear if the cache should be disabled here, too. In this case, the above U-Boot patch is (in theory) wrong, but if that's true, it was always wrong to begin with (as it always disabled the cache prior to ELF loading). If something like this was the case, then the rpi3 configurations (or perhaps some bootinfo code) needs to change. 3) Alternatively, this is just an outright bug in seL4 that should be fixed and U-Boot was previously masking it. (I'm not sure if the proofs cover this one :) 4) Perhaps it should be a mix of both. For example, perhaps the sel4/sel4test code should be changed to assume an already-enabled dcache, or fixed outright. But perhaps a U-Boot patch would still be good to submit upstream: for example, I could submit the above patch upstream, but *remove* the dcache code. This would allow U-Boot users to mark seL4 binaries appropriately for clarity and future compatibility and make U-Boot "officially support" seL4. And in the future, should seL4 need more patches/workarounds/requirements from U-Boot, it would be easier to add and maintain them. --- I'd prefer not to run myself into dead ends trying to get the wrong solution upstream to either seL4 or U-Boot, and it would be great to fix this for users. I'd also like to look into more adventurous stuff in the future (like multicore on the RPi3 which seems unsupported), so any advice is appreciated to get started. Even then: bisection and the patch creation only took an hour, so if it's wrong, not much was lost. -- Regards, Austin - PGP: 4096R/0x91384671

2 3

Re: [seL4] Some questions regarding seL4, U-Boot, and Raspberry Pi 3 patches
by Steven Johnston 19 Sep '17

19 Sep '17

Hi Austin I can confirm your blog post building method works. When attempting to boot from the SD card I receive a Wrong Image Format error: Hit any key to stop autoboot: 0 reading kernel.img 3385548 bytes read in 236 ms (13.7 MiB/s) Wrong Image Format for bootm command ERROR: can't get kernel image! However I was able to successfully network load the image and boot: U-Boot> dhcp 192.168.222.123:kernel.img Waiting for Ethernet connection... done. BOOTP broadcast 1 BOOTP broadcast 2 BOOTP broadcast 3 DHCP client bound to address 192.168.216.122 (1257 ms) Using sms0 device TFTP from server 192.168.222.123; our IP address is 192.168.216.122 Filename 'kernel.img'. Load address: 0x200000 Loading: ... done Bytes transferred = 3385548 (33a8cc hex) U-Boot> bootelf CACHE: Misaligned operation at range [20000000, 200078bc] CACHE: Misaligned operation at range [200078bc, 2032a720] CACHE: Misaligned operation at range [2032c000, 2033c820] ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[20000000..2033c81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[33000..44dfff] vaddr=[10000..42afff] virt_entry=2a03c Enabling MMU and paging Jumping to kernel-image entry point... ... Starting test 118: Test all tests ran Test suite passed. 118 tests passed. All is well in the universe Thank you for the push on RPI3! It helped me finish a thread I started months ago and also inadvertently confirmed the serial GPIO on a RPI3 I had been using was not operational. Steve > Date: Mon, 18 Sep 2017 01:49:40 +0000 > From: <Adrian.Danis(a)data61.csiro.au> > To: <aseipp(a)pobox.com>, <devel(a)sel4.systems> > Subject: Re: [seL4] Some questions regarding seL4, U-Boot, and > Raspberry Pi 3 patches > Message-ID: <829193ff-4b95-8d98-c2ad-6e626fdb5e1f(a)data61.csiro.au> > Content-Type: text/plain; charset="utf-8" > > Hi Austin, > > Thanks for the detective work! > > seL4 (or more specifically in this case the elfloader-tool) should be able to tolerate being started with either the cache enabled or disabled. In fact if you look in the mmu code (https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/…) you should notice some rough logic of > > if cache enabled > clean cache > disable cache > invalidate cache > > That code only operates on the architected caches though, and not on any platform specific cache controllers, although to my knowledge the rpi3 only has ARM architected caches. I would not be surprised if there were any errors in the dcache macro that walks through the cache levels though, which would be my guess as to where the problem is. > > I will create an issue internally to track this down, but will probably be a little while before anyone has time so if you're interested in fixing the elfloader then you're both welcome and encouraged to. Either way appreciate your efforts thus far. > > Adrian > > On Sun 17-Sep-2017 4:21 AM, Austin Seipp wrote: > Hello *, > > I hope you're all doing well. I recently got seL4 running on my Raspberry Pi 3, and wanted to report some notes here and ask some questions regarding the port, and perhaps get some help working on a patch (or twelve, I'm sure.) > > Recently I followed the Data61 blog post here to get a recent copy of seL4 on my RPi, but hit a few errors along the way that burned some time. In particular I got burned by the U-Boot glitch and getting seL4 building due to a glitch in the 'repo' setup for sel4test: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ > > I ended up writing my own blog post, with effectively "fully reproducible" instructions (e.g. one of the codepad.org<http://codepad.org> links on the RPi3 wiki page was dead) for a recent build. This includes proper setup for uboot.env in order to `fatload` and `bootm` the seL4 ELF binary off disk, the right U-Boot version, and using Docker to build the seL4 image: https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html > > That's all fine, but... > > I got curious about this U-Boot glitch, as even a recent (git) copy of U-Boot still suffered from the issue reported in the original Data61 blog post. I found it strange this regression would exist for nearly 9 months, unless it was possibly something intentional (e.g. an intended behavioral change) or it went unreported. > > The glitch is this: after booting the seL4 binary, the system immediately hangs with no output after trying to start the sel4test application. This glitch did not occur in versions of U-Boot up-to v2017.01. Versions v2017.03 and later (to now) suffer. > > I decided to spend some time bisecting this problem and found the issue. Versions of U-Boot after v2017.01 include the following patch, which causes the data cache to be enabled prior to U-Boot loading and executing ELF binaries: > > https://github.com/thoughtpolice/u-boot/commit/995eab8b5b580b67394312b1621c… > > This behavior previously existed as a workaround for QNX, which required that the dcache be disabled before execution. U-Boot, previously, disabled the dcache when booting *any* ELF binary at all (the binary can of course enable it or check to see if it isn't enabled already), as a simplistic workaround. This patch changes it to only disable the dcache on U-Boot images (uImages) marked as QNX ELF binaries, so that QNX systems boot properly still. > > It would seem then that seL4 -- or at least sel4test -- requires the dcache to be disabled upon entry for the RPi3. If the dcache is enabled, as in the above patch, it otherwise hangs immediately. > > In fact, a recent copy of U-Boot *can* execute seL4 properly: you simply have to use `./tools/mkimage` inside U-Boot to mark the application as `mkimage -C none -A arm -T kernel -O qnx -d <input> <output>` first -- this creates a uImage with the appropriate header to mark the ELF as a QNX binary. U-Boot recognizes this and appropriately disables the dcache before application entry, once you use `bootm` or something. > > I took the time to write a patch to U-Boot in order to add a new OS definition -- "sel4" -- in order to address this problem more clearly. My change is here: > > https://github.com/thoughtpolice/u-boot/commit/720caf6c398584658abfa883d4d3… > > With this change, you can mark any seL4 binary as `-O sel4` to create an appropriately bootable uImage, with the dcache appropriately disabled. > > Assuming this is in place, the following U-Boot commands will execute seL4: > > U-Boot> setenv bootfile uImage > U-Boot> fatload mmc 0 ${loadaddr} ${bootfile} > U-Boot> bootm ${loadaddr} > ## Booting kernel from Legacy Image at 00200000 ... > Image Name: > Image Type: ARM seL4 Kernel Image (uncompressed) > Data Size: 3385548 Bytes = 3.2 MiB > Load Address: 00000000 > Entry Point: 00000000 > Verifying Checksum ... OK > Loading Kernel Image ... OK > CACHE: Misaligned operation at range [20000000, 200078bc] > CACHE: Misaligned operation at range [200078bc, 2032a720] > CACHE: Misaligned operation at range [2032c000, 2033c820] > ## Starting application at 0x20000000 ... > > ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 > paddr=[20000000..2033c81f] > ELF-loading image 'kernel' > paddr=[0..32fff] > vaddr=[e0000000..e0032fff] > virt_entry=e0000000 > ELF-loading image 'sel4test-driver' > paddr=[33000..44dfff] > vaddr=[10000..42afff] > virt_entry=2a03c > Enabling MMU and paging > Jumping to kernel-image entry point... > > ---- > > So with that all done, it's clear there's a change needed *somewhere* but I'm not sure where or what to do: > > 1) Is the above the right approach? Clearly, seL4 on the RPi3 assumed a disabled dcache during its development, but this has now changed, so for this platform something will need to be fixed, such as the above. > > 2) Or perhaps this is not a U-Boot problem, but should be fixed in seL4. Or in sel4test. For example, is there an option to assume the dcache is already enabled in the configuration? Maybe that should be toggled instead. Or does seL4 *always* assume it is disabled at boot? What about non-RPi3 platforms like other ARM systems? These likely use U-Boot as well, but it's unclear if the cache should be disabled here, too. In this case, the above U-Boot patch is (in theory) wrong, but if that's true, it was always wrong to begin with (as it always disabled the cache prior to ELF loading). > > If something like this was the case, then the rpi3 configurations (or perhaps some bootinfo code) needs to change. > > 3) Alternatively, this is just an outright bug in seL4 that should be fixed and U-Boot was previously masking it. (I'm not sure if the proofs cover this one :) > > 4) Perhaps it should be a mix of both. For example, perhaps the sel4/sel4test code should be changed to assume an already-enabled dcache, or fixed outright. But perhaps a U-Boot patch would still be good to submit upstream: for example, I could submit the above patch upstream, but *remove* the dcache code. This would allow U-Boot users to mark seL4 binaries appropriately for clarity and future compatibility and make U-Boot "officially support" seL4. And in the future, should seL4 need more patches/workarounds/requirements from U-Boot, it would be easier to add and maintain them. > > --- > > I'd prefer not to run myself into dead ends trying to get the wrong solution upstream to either seL4 or U-Boot, and it would be great to fix this for users. I'd also like to look into more adventurous stuff in the future (like multicore on the RPi3 which seems unsupported), so any advice is appreciated to get started. Even then: bisection and the patch creation only took an hour, so if it's wrong, not much was lost. > > -- > Regards, > Austin - PGP: 4096R/0x91384671 > > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems<mailto:Devel@sel4.systems> > https://sel4.systems/lists/listinfo/devel > > >

1 0

Problem making the manual
by Raymond Jennings 18 Sep '17

18 Sep '17

I got an error log when I tried "make" in the manual directory. I got this: ====> Generating doxygen-output/xml/group__GeneralSystemCalls.xml ====> Generating doxygen-output/xml/group__DebuggingSystemCalls.xml ====> Generating doxygen-output/xml/group__BenchmarkingSystemCalls.xml ====> Generating doxygen-output/xml/group__ObjectApiX86.xml ====> Generating doxygen-output/xml/group__ObjectApiArm.xml ====> Generating doxygen-output/xml/group__ObjectApiAarch32.xml ====> Generating doxygen-output/xml/group__ObjectApiAarch64.xml ====> Generating doxygen-output/xml/group__ObjectApiIa32.xml ====> Generating doxygen-output/xml/group__ObjectApiX64.xml ====> Generating generated/GeneralSystemCalls.tex Traceback (most recent call last): File "tools/parse_doxygen_xml.py", line 327, in <module> sys.exit(main()) File "tools/parse_doxygen_xml.py", line 321, in main output_str = generate_general_syscall_doc(args.input, args.level) File "tools/parse_doxygen_xml.py", line 276, in generate_general_syscall_doc details, params, ret = parse_detailed_desc(member, ref_dict) File "tools/parse_doxygen_xml.py", line 157, in parse_detailed_desc ret_type = types_iter.next() AttributeError: 'list_iterator' object has no attribute 'next' make: *** [Makefile:126: generated/GeneralSystemCalls.tex] Error 1

3 3

I need help porting camkes/arm/vmm to new hardware
by Michael DeFrancis 13 Sep '17

13 Sep '17

To the sel4 development community: I am working on porting the sel4 virtual machine from the tk1 to a variety of arm hardware platforms, starting with the Xilinx parts listed below - and I could use some help getting started. I have the following hardware: - Tegra tk1 - Xilinx zynq7000 (zc706) - Xilinx zynq9000 (zcu102) I am successfully ported the 64 bit sel4 kernel to run on the zynq9000, but now I need to port the arm/vmm to run on the zynq9000 hardware as well. I am happy to share these updates with the sel4 community at large. I am uncertain what the best way to do this is - should I submit all of the changes to github, or is there another development repository? I would like to first port the arm/vmm from https://github.com/SEL4PROJ/camkes-arm-vm to the zynq7000<https://github.com/SEL4PROJ/camkes-arm-vm%20to%20the%20zynq7000> for testing, before porting it to the 64 bit zynq9000 platform. Could someone please put me in touch with the author of the arm/vmm that is designed to run on the tegra/tk1 hardware? I have some specific questions to ask regarding platform-specific files. At a high level, I know that I need to change the addresses of peripherals that are passed to my linux kernel (buildroot) for the zynq7000, but I am uncertain where to start. If someone could point me in the right direction, that would be very helpful. Further, if I could talk to a real person about this over the phone, that would be even better. My work phone is (1)(301)294-5263 and my cell phone is (1)(571)271-7278 - feel free to call me and leave me a message. I have not posted to devel(a)sel4.systems<mailto:devel@sel4.systems> previously, though I have been working on the sel4 project for a few months now. I work for Intelligent Automation Inc. in Rockville, Maryland - USA. ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

Announcing 7.0.0 release
by Kent.Mcleod＠data61.csiro.au 05 Sep '17

05 Sep '17

= seL4 Version 7.0.0 Release = Announcing the release of seL4 7.0.0 with the following changes: == Changes == * Support for building standalone ia32 kernel added in e7327fa6df3 * ia32: Set sensible defaults for FS and GS selectors in c2f6d48bcf2 * aarch64: Use tpidrro_el0 for IPC buffer instead of tpidr_el0 in ae9fe9b5d18 * More seL4 manual documentation added for aarch64 object invocations * Default NUM_DOMAINS set to 16 for x86-64 standalone builds in baa9798f793 * libsel4: Return seL4_Error in invocation stubs in 8fb06eecff9 ''' This is a source code level breaking change ''' * Add a CMake based build system in 0b73072016e * x86: Increase TCB size for debug builds in 4c8be8f4f91 * libsel4: x86: Remove nested struct declarations in a8d6315eb16 ''' This is a source code level breaking change ''' * Bugfix: x86: Unmap pages when delete non final frame caps in 08b9265563a = Notable changes = * CMake based build system added: Initial experimental support has been added for using CMake for building the kernel and some user level libraries. Currently the only project that takes advantage of this is seL4test when using the cmake.xml manifest in sel4test-manifest. Documentation can be found at: https://github.com/seL4/seL4_tools/tree/master/cmake-tool = Upgrade notes = * This release is not source compatible with previous releases. * seL4 invocations that previously returned long now return seL4_Error which is an enum. Our libraries have already been updated to reflect this change, but in other places where seL4 invocations are used directly, the return types will need to be updated to reflect this change. * On x86 some structs in the Bootinfo have been rearranged. This only affects seL4_VBEModeInfoBlock_t which is used if VESA BIOS Extensions (VBE) information is being used. = Known issues = * One of our tests is non-deterministicly becoming unresponsive on the SMP release build on the Sabre IMX.6 platform, which is a non verified configuration of the kernel. We are working on fixing this problem, and will likely do a point release once it is fixed. = Full changelog = Use `git log 6.0.0..7.0.0` in https://github.com/seL4/seL4 = More details = See the 7.0.0 manual <http://sel4.systems/Info/Docs/seL4-manual-7.0.0.pdf> included in the release or ask on the mailing list!

1 0

UX/RT - an seL4-based OS in the style of QNX and Plan 9
by Andrew Warkentin 03 Sep '17

03 Sep '17

I mentioned this here earlier, but I haven't really gone into a lot of detail about it here. I am planning to write an seL4-based OS similar to QNX and Plan 9 called UX/RT. I am intending it to be both an embedded OS (mostly for the larger types of embedded systems where QNX or Linux would be used, as opposed to simpler ones) as well as a desktop OS. I plan to use as much third-party code as possible to avoid making lots of extra work (likely LKL <https://github.com/lkl/linux> and/or the NetBSD rump kernel for device drivers, disk filesystems, and the network stack; a libc based on musl; and basic commands forked from those of FreeBSD). UX/RT will be a pure Unix-like system with no concept of "personality-neutral" services, and the root server will implement a subset of the Unix API directly (as in QNX, although the root server will be completely separate from the kernel of course, unlike that of QNX). However, there will be a Linux compatibility layer implemented with libraries and filesystem servers. I am going to avoid C for new code as much as possible for security, preferring Rust for anything performance-critical. The main concept behind the design will be to take "everything is a file" as far as it possibly can go. Nearly all resources in the system will appear in the filesystem, even things like process memory (kernel memory and the interface to the root server will be among the few non-files in the system, although the API of the root server will be implemented with an anonymous FD internally). The filesystem will be a combination of a thin layer on top of L4 IPC with read() and write() calling L4 IPC directly (short transfers will probably be sent entirely in message registers and long ones sent by using shared pages), and a memory mapping layer. The VFS will implement the name service and memory mapping parts of the filesystem; read() and write() will bypass the VFS layer entirely and will use seL4 IPC to communicate directly with the other thread. There will also be APIs that expose message registers and shared pages more directly although they will do it in a way that interoperates with read() and write() (these will mostly be used with a new "message-special" file type that preserves message boundaries but otherwise acts like a normal byte stream if used with read() or write()). No provisions will be made for use of IPC or capabilities outside the filesystem. Security will be based on an ACL-per-process model, where the root server will have an in-memory list of files for each process specifying which files it is allowed to access, as opposed to a hierarchical pure-capability model like other L4-based systems (a pure capability model seems like it would be a poor fit for a pure Unix-like system). It will be possible to either specify rwx permission bits explicitly or use the mode from the filesystem; it will also be possible for an ACL entry to specify all files under a particular directory. File descriptors will be implemented as groups of capabilities, and the root server will hand them out when a process successfully opens a file (unlike in QNX there will be no need for individual filesystem servers to check whether the client process is authorized to access a file). There will be an ACL management server that will persistently associate permissions with programs, and it will also be possible for sufficiently privileged processes to dynamically modify the ACLs of other processes. I currently have a bootloader, some basic infrastructure for building boot ISO images, and a patch for seL4 to support QNX-like XIP single-image boot using a variant of Multiboot2. I can build a boot ISO with a system image containing only the kernel, but it crashes with a triple fault somewhere in either the bootloader or the kernel (I haven't yet tried to track down where it's occurring). Once I move on to user mode code, I'm going to be using the Rust libraries from Robigalia as a basis for the root server (higher-level Rust-based components will use a normal Unix build of the Rust standard library instead). The code I have so far can be found at <https://gitlab.com/uxrt> for UX/RT itself and <https://gitlab.com/uxrt-bos> for the bootloader. I have some (long and not particularly well-organized) notes on my plans for UX/RT's architecture at <https://gitlab.com/uxrt/uxrt-toplevel/blob/master/architecture_notes>. Anybody is more than welcome to contribute if they want.

2 2

VGA buffer as stdout
by Michal Podhradsky 31 Aug '17

31 Aug '17

Hello, I have a question about standard output. I have a camkes component than can write into text-mode VGA buffer (basically it follows this simple example http://wiki.osdev.org/Bare_Bones#Writing_a_kernel_in_C ) but I would like to be able to redirect the kernel messages during startup to be printed on screen using VGA buffer. Once another component (either Linux in a VM, or some other camkes app) will initialize, it will be able to take control over the screen output (and for example show login window etc). My questions is - is this possible with seL4? And if so, what would it entail? I guess in the minimal version, I would have to provide a different implementation of seL4_DebugPutChar, is that correct? The VGA standard seems to define the buffer to be at 0xB8000, so it should be consistent between x86 platforms. Regards Michal

5 11

benchmark - idle utilization
by Alexander Boettcher 31 Aug '17

31 Aug '17

Hello, we use the seL4 benchmark interface to feed Genode's trace infrastructure with information about the CPU utilization of threads and of idle times. In general the integration was reasonable straightforward. One minor point we had. It seems that the idle time of a CPU can only be requested by a thread running on the vary same CPU. Requesting the CPU idle times of a remote CPU (the calling thread is on another CPU) is not supported, right ? In principle we may start on each CPU a thread just for the sake of requesting the idle utilization time, which however looks a bit of overkill. We "kind of" circumvent the issue for us by changing the syscall handling in the kernel in that regard, that the CPU number of the requested target thread is taken instead that of the caller thread, e.g. like this: --- a/src/benchmark/benchmark_utilisation.c +++ b/src/benchmark/benchmark_utilisation.c @@ -36,6 +36,11 @@ void benchmark_track_utilisation_dump(void) tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(lu_ret.cap)); buffer[BENCHMARK_TCB_UTILISATION] = tcb->benchmark.utilisation; /* Requested thread utilisation */ +#if CONFIG_MAX_NUM_NODES > 1 + if (tcb->tcbAffinity < ksNumCPUs) + buffer[BENCHMARK_IDLE_UTILISATION] = NODE_STATE_ON_CORE(ksIdleThread, tcb->tcbAffinity)->benchmark.utilisation; /* Idle thread utilisation */ + else +#endif buffer[BENCHMARK_IDLE_UTILISATION] = NODE_STATE(ksIdleThread)->benchmark.utilisation; /* Idle thread utilisation */ #ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT With this change, we still have to create a thread on every CPU (since we need a capability for the syscall), but at least the threads must not be running actively. Does this change (the patch) make sense to you and is it worthwhile to adjust in general on your side - or would you advise/envision another approach/direction ? (like specifying the cpu number for the idle times directly via the syscall or having a explicit syscall just for cpu idle times [but there are no specific thread idle capabilities as syscall parameter] etc.) Another question: Currently it seems that no idle CPU times are provided, as long as no user thread is actively running on that specific CPU. We can handle it, no problem in general - however we would have to adjust generic code (which runs on 8 different kernels) specifically for seL4 to handle this minor case. Could this possibly be changed (easily) ? Thanks, Alex. -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 3

Compile errors for Beaglebone Black
by Todd_Peterson＠mgtsciences.com 30 Aug '17

30 Aug '17

Hi, I am trying to compile seL4 for the BBB. I am getting the following errors when it gets to timer_service. I am following the instructions at https://github.com/seL4/refos-manifest. I got past another compile error by adding a typedef to device_timer.h for pstimer_t. Any help is appreciated. // tfp, added to avoid compiler error typedef uint32_t pstimer_t; [apps/timer_server] building... [HEADERS] [STAGE] autoconf.h [CC] src/state.o In file included from /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:22:0, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24: /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h: In function 'data_open_map': /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h:95:69: warning: passing argument 6 o f 'data_open' from incompatible pointer type [-Wincompatible-pointer-types] d.dataspace = data_open(session, name, flags, mode, dspaceSize, &errnoRetVal); ^ In file included from /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:21:0, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24: /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client.h:72:11: note: expected 'int ** (*)()' but ar gument is of type 'int *' seL4_CPtr data_open(seL4_CPtr session, char* name, int flags, int mode, int size, int* errno); ^ [CC] src/device_timer.o /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_handle_irq': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:146:5: warning: implicit declaration of function 'timer _handle_irq' [-Wimplicit-function-declaration] timer_handle_irq(s->timerDev, irq); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_init': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:239:5: error: unknown type name 'timer_config_t' timer_config_t config; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:11: error: request for member 'vaddr' in something not a structure or union config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TIMER_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52: error: 'dm_timer_paddrs' undeclared (first use in this function) config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TIMER_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52: note: each undeclared identifier is reported on ly once for each function it appears in /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:11: error: request for member 'irq' in something no t a structure or union config.irq = dm_timer_irqs[TIMER_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:18: error: 'dm_timer_irqs' undeclared (first use in this function) config.irq = dm_timer_irqs[TIMER_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:243:16: error: request for member 'vaddr' in something not a structure or union if (!config.vaddr) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:19: warning: implicit declaration of function 'ps_g et_timer' [-Wimplicit-function-declaration] s->timerDev = ps_get_timer(TIMER_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:17: warning: assignment makes pointer from integer without a cast [-Wint-conversion] s->timerDev = ps_get_timer(TIMER_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:250:11: error: request for member 'vaddr' in something not a structure or union config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TICK_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:252:11: error: request for member 'irq' in something no t a structure or union config.irq = dm_timer_irqs[TICK_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:253:16: error: request for member 'vaddr' in something not a structure or union if (!config.vaddr) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:258:16: warning: assignment makes pointer from integer without a cast [-Wint-conversion] s->tickDev = ps_get_timer(TICK_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:273:41: error: request for member 'properties' in somet hing not a structure or union for (uint32_t i = 0; i < s->timerDev->properties.irqs; i++) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:274:19: warning: implicit declaration of function 'time r_get_nth_irq' [-Wimplicit-function-declaration] int irq = timer_get_nth_irq(s->timerDev, i); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:282:44: error: request for member 'properties' in somet hing not a structure or union for (uint32_t i = 0; i < s->tickDev->properties.irqs; i++) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:289:21: warning: implicit declaration of function 'time r_start' [-Wimplicit-function-declaration] int error = timer_start(s->tickDev); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:310:13: warning: implicit declaration of function 'time r_periodic' [-Wimplicit-function-declaration] error = timer_periodic(s->timerDev, TIMER_PERIODIC_MAX); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_get_time': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:344:21: warning: implicit declaration of function 'time r_get_time' [-Wimplicit-function-declaration] uint64_t time = timer_get_time(s->timerDev); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:345:21: error: request for member 'properties' in somet hing not a structure or union if (!s->timerDev->properties.upcounter) { ^ make[1]: *** [/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/common/common.mk:265: src/device_timer.o] Error 1 make: *** [tools/common/project.mk:331: timer_server] Error 2 Todd Peterson Chief Embedded Systems Engineer Management Sciences, Inc. 6022 Constitution Ave NE Albuquerque, NM 87144 505-255-8611 (office) 505-205-7057 (cell) This email message and any attachments are for the sole use of the intended recipient(s) and may contain proprietary and/or confidential information which may be privileged or otherwise protected from disclosure. Any unauthorized review, use, disclosure or distribution is prohibited. If you are not the intended recipient(s), please contact the sender by reply email and destroy the original message and any copies of the message as well as any attachments to the original message.

1 0

Genode OS Framework 17.08 with extended seL4 support
by Alexander Boettcher 30 Aug '17

30 Aug '17

Hello, we're happy to announce the version 17.08 of the Genode OS Framework. Within the last release cycle (3-months) we upgraded our Genode/seL4 support from kernel version 3.2.0 to 6.0.0, enabled x86_64 and ARM support, added UEFI support to the seL4 kernel and enabled SMP for x86. A summary of changes and features are: - Hardware-accelerated graphics for Intel Gen-8 GPUs - The seL4 6.0 kernel on ARM and 64-bit x86 hardware - Genode as Xen DomU - Preliminary UEFI support for NOVA, base-hw, and seL4 - New server for capturing reports to files - New runtime for the sequential execution of components - Support for boot-time initialized frame buffer - FatFS-based VFS plugin - Extended non-blocking operation of the VFS - Refined time handling - Updated Muen separation kernel The long version of the official release documentation: https://genode.org/documentation/release-notes/17.08 All the best, -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 1

x86_64 kernel crash
by Alexander Boettcher 30 Aug '17

30 Aug '17

Hello, we're are in progress of extending our Genode/seL4 support, namely adding x86_64 and ARM support. During this work I encountered on x86_64 some sporadically crashes of the seL4 kernel. It happened during the debugging of our roottask on seL4 in form of a page fault in the kernel ("KERNEL EXCEPTION") or a static assertion in the kernel (see below). >From my understanding, this shouldn't be possible based on your verification work. Nevertheless, it happens reliable. (To be fair, the roottask was in this scenario already a bit confused and did things wrong - which however should never be enough to force the kernel in an exception or assertion - I presume.) I saved and stripped down the scenario which causes the kernel exception with high reliably and hope you can re-produce it and find the root cause. I stripped down the scenario to just the Genode image binary and the steps we did to create the seL4 kernel from the vanilla sources. Steps to reproduce: qemu-system-x86_64 -no-kvm -serial stdio -m 512 -kernel sel4 -initrd bomb_image.elf The binaries of "bomb_image.elf" can be found at [1] and the kernel "sel4" at [2]. The kernel is based on seL4 6.0 and a patch to pc99/autoconf.h (see [0]). Beside that it is the vanilla 6.0 kernel: https://github.com/seL4/seL4.git git commit 8564ace4dfb622ec69e0f7d762ebfbc8552ec918 "update VERSION file to 6.0.0" patch -p1 <~autoconfig.patch BOARD=x86_64 ARCH=x86 SEL4_ARCH=x86_64 PLAT=pc99 DEBUG=1 make objcopy -O elf32-i386 kernel.elf.strip sel4 (Qemu complains otherwise about 64bit elf for boot) The final "sel4" binary can be used with the "bomb_image.elf" and qemu as pointed out above. I tried Qemu 2.5.0 as shipped with Ubuntu 16.04 LTS and Qemu 2.8.0 (self-compiled). On real hardware the scenario typically leads after a while (kernel booted, roottask booted, scenario starts to run) to a reboot (without the messages or assertion as in the Qemu case, see below). The tool-chain for Genode is based on GNU GCC 6.3.0 (see [3] and [4]). The kernel was either compiled with Genode's toolchain (6.3.0) or with the standard GCC as provided by Ubuntu 16.04 LTS (GCC 5.4.0). On x86_32 I could not reproduce the issue. (On ARM I did not try.) I hope the information are helpful - if you need more just ask. Cheers, Alex. ========== KERNEL EXCEPTION ========== Vector: 0xe ErrCode: 0x0 IP: 0xffffffff80720e60 SP: 0xffffffff80740e08 FLAGS: 0x6 CR0: 0x8000003b CR2: 0x3007065 (page-fault address) CR3: 0x1ffb000 (page-directory physical address) CR4: 0x220 Stack Dump: *0xffffffff80740e08 == 0xffffff8001a99b00 *0xffffffff80740e10 == 0xffffffff80729b1f *0xffffffff80740e18 == 0x1 *0xffffffff80740e20 == 0xffffffff80721c59 *0xffffffff80740e28 == 0xffffffff *0xffffffff80740e30 == 0x0 *0xffffffff80740e38 == 0xffffff801f02b740 *0xffffffff80740e40 == 0xffffff801f02b740 *0xffffffff80740e48 == 0x1 *0xffffffff80740e50 == 0xffffff8001a99000 *0xffffffff80740e58 == 0x7 *0xffffffff80740e60 == 0x59 *0xffffffff80740e68 == 0xffffff8001a99b00 *0xffffffff80740e70 == 0xffffffff80729cf3 *0xffffffff80740e78 == 0x9000000000000007 *0xffffffff80740e80 == 0xffffff8001a99059 *0xffffffff80740e88 == 0xffffff80ffffffff *0xffffffff80740e90 == 0xffffffff80740f18 *0xffffffff80740e98 == 0xffffff800013c200 *0xffffffff80740ea0 == 0x10000 Halting... halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 16 or seL4 failed assertion '(cte_t*)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL && (cte_t*)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL' at src/object/cnode.c:457 in function cteInsert halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 18 or a fault by the roottask (and not in the kernel). So - this is no issue for the kernel: Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x18 with status 0x4 in thread 0xffffff800013c200 "child of: 'rootserver'" at address 0x20419cf [0] https://github.com/alex-ab/genode/blob/crash_sel4_kernel_vanilla/autoconfig… [1] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/image_bomb.… [2] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/sel4 [3] https://genode.org/download/tool-chain [4] https://sourceforge.net/projects/genode/files/genode-toolchain/17.05/ -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 3

Arm VMM Vchan
by Enrique Leon 26 Aug '17

26 Aug '17

Hello to All, I am trying to do some message passing between a vm component and a camkes component. I have tried by enabling the Vchan option on the build system and compiling the helloworld linux user level program on a tk1. I received an error about the /dev/vmm_manager not being able to open. What is the proper method of setting up the Vchan communication for camkes-arm-vmm on a tk1? Thank You

1 0

Re: [seL4] Devel Digest, Vol 39, Issue 26
by talos 25 Aug '17

25 Aug '17

Dear, I used "qemu-system-i386 -m 1024 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99" It showed "Booting from ROM" Thanks, Sincerely ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Thu, Aug 24, 2017 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 39, Issue 26 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, 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. Re: about camkesvm (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Thu, 24 Aug 2017 00:00:19 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] about camkesvm Message-ID: <1503532819201.94096(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hey Talos, Sorry we didn't make this clearer on that page: those defconfigs build an x86-pc image; not an ARM image. Could you try running Qemu again, but with something similar to, qemu-system-i386 -m <WHATEVER_RAM_SIZE_YOU_WANT> -kernel <SEL4_KERNEL_IMAGE> -initrd <CAPDL_INITRD_IMAGE> And tell me what happens? Sorry for the inconvenience. -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com> Sent: 22 August 2017 15:39 To: devel Subject: [seL4] about camkesvm Hi I started the tutorial following the link: https://wiki.sel4.systems/CAmkESVM I used "make minimal_defconfig" substituting "make cma34cr_minimal_defconfig" for int the directory config there is minimal_defconfig then make and qemu-system-arm -M kzm -nographic -kernel images/capdl-loader-experimental-image-ia32-pc99 but the error is Segmentation fault (core dumped) what's wrong? Thanks Sincerely -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170824/cd4992b3/attachmen…> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 39, Issue 26 *************************************

2 1

camkes-arm-vm Platform Support
by Robert VanVossen 24 Aug '17

24 Aug '17

Hello, Is Data61 or anyone else working on porting camkes-arm-vm to platforms other than the TK1? Thank you, Robbie VanVossen DornerWorks, Ltd.

2 1

about camkesvm
by talos 24 Aug '17

24 Aug '17

Hi I started the tutorial following the link: https://wiki.sel4.systems/CAmkESVM I used "make minimal_defconfig" substituting "make cma34cr_minimal_defconfig" for int the directory config there is minimal_defconfig then make and qemu-system-arm -M kzm -nographic -kernel images/capdl-loader-experimental-image-ia32-pc99 but the error is Segmentation fault (core dumped) what's wrong? Thanks Sincerely

2 1

Raspberry Pi3 + seL4
by Steven Johnston 23 Aug '17

23 Aug '17

Has anyone had issues with serial when running the test suite on a Raspberry Pi 3b? Currently I am following the blog post: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ In the seL4test project I have successfully compiled sel4test-driver-image-arm-bcm2837 from rpi3_debug_xml_defconfig. Along with this I have the following files: bootcode.bin, start.elf, u-boot.bin, and config.txt. Bootcode.bin and start.elf are from the current Raspian firmware. Config.txt just contains a line to enable UART ("enable_uart=1") and one to point and u-boot.bin ("kernel=u-boot.bin"). And per the comment section of the seL4 post I downgraded the version of u-boot to before March 2017 (currently using Jan 2017). I am not deviating from the blog posting but I am experiencing an issue not mentioned. I have no serial output (I do have a u-boot terminal prompt through HDMI, so I can load/boot the binary). When I boot seL4 I receive the misaligned cache messages (through HDMI) and then it hangs. Without serial I have no eyes to see if the seL4 tests are running. Other than wiring into the RPI3 UART (GND/TX/RX on pins 6/8/10) and enabling UART in config.txt is there another step I'm missing? Thanks for any direction you can point me in, Steve

2 2