- Devel - lists.sel4.systems

Porting Qubes OS to seL4 project
by Paul Vlase 23 Mar '16

23 Mar '16

Hello, My name is Paul Vlase and I am following a master degree right now. I am interested in porting the Qubes OS to seL4 project and I saw that you are working already on it. Is there anything I can help you on this project? Thank you, Paul Vlase

1 0

[CAmkES] CAmkES 2.1.0 Release Notes
by Stephen Sherratt 22 Mar '16

22 Mar '16

CAmkES 2.1.0 Release Notes ========================== ## New Features - runner takes an `--architecture` command line argument which selects the target architecture. Valid arguments are: aarch32, arm_hyp, ia32 - added the ability to specify a hardware dataport as cached. Previously all hardware dataports were mapped uncached. This feature is intended to be used on dataports backed by DMA-able memory to improve access times. Functions to flush dataports from the cache are also provided. - support for seL4 3.0.0 ## Removed Features - `--hyp` command line argument is replaced with `--architecture arm_hyp` ## API Removals ### Unmarshalling Helpers These were intended for use in templates, but are no longer used in any internal templates: - `camkes_marshal` - `camkes_marshal_string` - `camkes_unmarshal` - `camkes_unmarshal_string` ### DMA Utilities These had been deprecated for a long period and are now being removed: - `camkes_dma_page_alloc` - `camkes_dma_page_free` You can find it at: https://github.com/seL4/camkes-tool/tree/camkes-2.1.0 A manifest for the 2.1.0 compatible versions of test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.1.x.xml Release notes on the wiki: https://wiki.sel4.systems/CAmkES%202.1.0 Enjoy! ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

What happens to the IPC buffer when you make another process within the same Vspace?
by Qiwei Wen 20 Mar '16

20 Mar '16

Hi, I'm trying to write a multithreaded seL4 application. It's to be made up of sel4util processes with different cspaces and sharing the same Vspace. I managed to achieve this, but what confuses me is that since the processes share the same Vspace, wouldn't GetIPCBuffer() return the same result for each of them? I looked at libsel4/arch_include/arm/sel4/arch/functions.h, and GetIPCBuffer() is simply: return *(seL4_IPCBuffer**)seL4_GlobalsFrame; Since seL4_GlobalsFrame is just a fixed memory location (0xffffc000) in the shared address space, why does seL4_GetIPCBuffer() return different results for different processes? Below is the output: ========================== PARENT: IPCBUFFER: 00273000 CHILD: GlobalsFrame: ffffc000, *GlobalsFrame 10076000 CHILD: setting shared to 97 PARENT: CHILD DIED, shared char: 97, MR16: 00000000 ============================= Is it that the frame ffffc000 mapping is changed on every context switch perhaps? Can I absolutely trust that IPC is still working correctly with this set up? Thanks, David

5 4

Isabelle itself proven?
by Steve VanderLeest 20 Mar '16

20 Mar '16

Since the formal verification of functional correctness of seL4 was performed using the Isabelle theorem prover, could someone tell me if Isabelle itself has been formally verified? If so, could you suggest some good references to that work? Regards, Steve Steven H. VanderLeest, Ph.D. Chief Operating Officer DornerWorks, Ltd. 3445 Lake Eastbrook Grand Rapids, MI 49546 www.dornerworks.com

3 2

Booting process
by Daniel Wang 19 Mar '16

19 Mar '16

Hi all, I’m very new to seL4 development. I’m particularly interested in understanding seL4 kernel source code. Could someone points me out how the seL4 is booted and where should I start learning? Thanks -Dan

3 2

seL4 wiki
by Anna Lyons 19 Mar '16

19 Mar '16

Hi all, We've created a public wiki for seL4 development here: https://wiki.sel4.systems/ The kernel team have put some effort into creating the initial content, but there is much more to be done. Contributions encouraged! New accounts are restricted to avoid spam, but if you have posted on this mailing list your account will be approved quickly. Otherwise contact us. Thanks, Anna Lyons seL4 Kernel Engineer | PhD Student DATA61 | CSIRO E <mailto:Brigitte.Biscotto@data61.csiro.au> Anna.Lyons(a)data61.csiro.au<mailto:Anna.Lyons@data61.csiro.au> Level 3, K17 Building, UNSW Gate 14, Barker Street, Kensington, NSW, 2033 l Locked Bag 6016, Sydney NSW 1466 www.data61.csiro.au<http://www.data61.csiro.au/> CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 [cid:image001.png@01D0EFD9.052ECFC0] ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

FYI: microkernel.info community site
by Jakub Jermář 14 Mar '16

14 Mar '16

Hello, just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it. I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better. Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github. Thanks, Jakub [1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

8 8

Capability faults on seL4_Send and seL4_Call
by Qiwei Wen 12 Mar '16

12 Mar '16

Hi all, I understand that capability faults for seL4_Send and seL4_Call only happen when the look-up fails, and not when illegal operations are attempted, such as calling a null cap or a piece of untyped memory. Is there another way at all, then, that such errors can be handled by user-level code? This is part of a project where the faulting process needs to surrender control to another process whenever it performs a system call on an invalid capability. Is there a way to achieve this given that fault endpoints will not work? Thanks, David

1 0

using camkesvm with qemu
by Julien Delange 10 Mar '16

10 Mar '16

Hi, I am currently trying to use the camkesvm example and run it in qemu. I am currently able to compile the c162_twovm_defconfig application. However, when running, I have the following issue (see below). So, I am wondering what would be the good arguments to start the application in qemu. I noticed that the kernel/initrd image for linux are specific in a header file, I assume this is also included in the image loaded by capdl. Any idea about how to run this example with qemu and/or how to test it? Thanks! Starting node #0 vt-x: not supported <<seL4 [decodeUntypedInvocation/193 T0xe2ff1900 "rootserver" @804afa7]: Untyped Retype: Insufficient memory or offset outside untyped>> Unmasking IOAPIC source 2 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 3 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 4 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 16 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 17 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 18 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 23 on ioapic 0 without ever setting its mode! <<seL4 [decodeCNodeInvocation/107 T0xe2ff1900 "rootserver" @804a4b2]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.>> capDL-loader :: << Error: init_cnode_slot:1471: seL4_FailedLookup >> Ignoring call to sys_rt_sigprocmask

3 4

Recovering from cap fault?
by Qiwei Wen 10 Mar '16

10 Mar '16

Hi all, On page 26 of the manual (1.2) there's an instruction on how to restart a thread following a capability fault. The program counter where the faulting thread should pick up execution is said to be message register 0. What I'm trying to do is to restart the execution on the next instruction following the system call instruction so as to skip it. Try as I might, it will not work and the faulting thread is stuck in an endless number of faults. Below is the relevant code: seL4_Word pc = seL4_GetMR(0); printf("cap fault, pc: %08x, on %s\n",pc,seL4_GetMR(2)?"wait":"send"); //assert(!faultnum++); seL4_MessageInfo_t info = seL4_MessageInfo_new (seL4_CapFault,0,0,1); seL4_SetMR(0,pc + 4); seL4_Reply(info); It does restart, but immediately cap-faults again at the very same program counter. Is it supposed to work? What did I do wrong? Cheers, David

2 1