[seL4] Re: propagating initial thread's capabilities

On Mon, Mar 28, 2022 at 11:04 AM Sam Leffler wrote:

On Sun, Mar 27, 2022 at 3:43 PM Kent Mcleod wrote:

...

On Mon, Mar 28, 2022 at 6:29 AM Sam Leffler via Devel wrote:

...

The rootserver gets various caps setup for it by the kernel (see Table 9.1 in the manual). This includes the gobal ASID, IRQ, Domain, and Sched controllers. I need these caps in a process created by the rootserver. This is within a CAmkES environment. So far I've created CAmkES component attributes that signal the rootserver should hand-off a cap by moving the rootserver's cap to the designated CNode just before it terminates. This involves modifications to CAmkES, capDL, and the rootserver. Is there a better way? Is there an existing example of doing this? Are any of these global objects accessible some other way than hand-off from the rootserver?

CapDL and the capdl-loader-app should already be able to move these caps without extra modifications. They exist in the spec: https://github.com/seL4/capdl/blob/master/capDL-tool/CapDL/Model.hs#L376-L38...

The "interrupts" tutorial (https://docs.sel4.systems/Tutorials/interrupts.html) works by having the irq_control cap moved into one of the component CNodes. The capdl spec fragment that does this is: ``` cnode_timer { // ... 0x8: irq_control } ``` Note that this tutorial isn't CAmkES but uses a CapDL spec and the rootserver to set up the tutorial apps.

Within camkes, I'm not immediately aware of any public examples that use any of these caps. There's one template that does appear to support moving a sched_control cap to a component: https://github.com/seL4/camkes-tool/blob/271d6a2405d571272b252fcf308e7581cdd... A custom CAmkES template could be added which would work for any of the special caps you mentioned as they are all defined in the library camkes uses to generate specs: https://github.com/seL4/capdl/blob/master/python-capdl-tool/capdl/Object.py#...

Very nice. This looks to eliminate many of my mods. Some questions: 1. I've been handing off the ASDIPool object at seL4_CapInitThreadASIDPool but following your suggestions appears to create a new ASDIPool instead of passing along the rootserver's. My template snippet is:

/*- if configuration[me.name].get('asid_pool', False) -*/ /*- set asid_pool = alloc('asid_pool', type=seL4_ASID_Pool, core=configuration[me.name].get('domain_ctrl')) -*/ const seL4_CPtr ASID_POOL = /*? asid_pool ?*/; /*- endif -*/

(I blindly copied the core setting, looks like it may be ignored). IIUC I may be able to have multiple asid pools (depending on the arch) and that may be preferred but for now I was intending to assign all my vspace roots to the same pool. Is that happening? (I'm just going off what I see in system.cdl & capdl_spec.c). If I am getting a new ASID pool is there any way to express that I want seL4_CapInitThreadASIDPoo and not a new object?

I was assuming you wanted the seL4_CapASIDControl cap. I don't think there is a way to move/copy the seL4_CapInitThreadASIDPool cap without teaching the CapDL spec and rootserver about it. I don't think that would be an uncontroversial change. Having multiple ASID pools shouldn't be an issue (unless you're extremely space constrained as each one is 4k). Having more ASID pools allows you to have slightly better isolation between untrusted components if they don't share an ASID pool but are able to dynamically assign/unassign vspaces to an ASID pool object because of the ASID-reuse caveat: https://github.com/seL4/seL4/blob/master/CAVEATS-generic.md#re-using-address... (this does also apply to RISCV).

2. UntypedMemory. My first foray down this path was to hand-off the UntypedMemory objects. Can I use similar techniques to make this happen w/o mods to signal the rootserver to DTRT. Seems more difficult given this comes via BootInfo and requires moving an unknown (at compile-time) # of UntypedMemory caps. My current scheme moves the untypeds and also passes along a page with an updated version of BootInfo to identify the set of caps for the UntypedMemory objects.

I believe the only existing way you could do this is by naming the exact untypeds in the spec, by providing a physical address. As you say, this is hard to do if you don't know ahead of time what the bootinfo is going to contain (you can precalculate it though if you know the size of the rootserver and kernel images). It still seems that the way forward here is to have some sort of builtin way of parameterizing the spec to describe how the loader can move remainder UT objects into a range of slots and also fill in a frame with the book keeping information.

3. While I'm getting a lesson in CAmkES templates + capDL, is there a way to arrange to allocate a FrameObject and install the cap to it in "my_cnode" (or somewhere else that I can access to unmap the page so I have just page-size gap in the vspace)? This is for temporarily mapping pages to write their contents (as the rootserver does when constructing a component's vspace contents). I've got something ugly that seems to DTRT but would love to "do it right".

The mechanisms do exist. The seL4HardwareMMIO template (https://github.com/seL4/camkes-tool/blob/master/camkes/templates/seL4Hardwar...) is an example where the mapping caps are moved into the CSpace of the component. The magic is encapsulated in the register_shared_variable() implementation which has to call `cap.set_mapping_deferred()` on each frame cap and add the list of caps to an address space allocator with `addr_space.add_symbol_with_caps(symbol, sizes, caps)` to defer assigning the CNode slot it's placed in until the VSpace is created for the component. This generates a spec where the cap containing the VSpace mapping is moved into a specified CNode slot so that the mapping can be unmapped.

...

The loader moves these special caps in a final move phase after all other caps have been created so that they are moved after any caps have already been derived from them.

These global objects can't be copied or created and so the only way for them to get given to a new CSpace is for them or a CNode that they're stored in to be moved to the target CSpace.

...

-Sam _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems