[seL4] Re: capdl-loader questions

On Wed, Dec 1, 2021 at 9:59 AM Sam Leffler via Devel <devel(a)sel4.systems> wrote: My Why? I and, the It's currently mutable because of the updates to it as it is processed. If these updates were removed, then it would be a good idea to make it immutable. How would you handle the mapped_frame_cap bookkeeping without storing it in the spec as a single frame could have multiple shared mappings which each require a cap?

#define'd size of each page What you suggest would be possible. For some object types (like an endpoint) the original cap is special and can be used to revoke all children caps that have been derived from it. All frame types don't have this property which means that the original cap is no different from any copies of it. Embedding whether the frame is shared into the object as an attribute would make this easier to optimize as I agree that it becomes pretty inefficient in typical systems with many more private frames than shared.

created fill tries the might be extra whether Short answer: For copy_addr_with_pt, yes we could make the 64kiB definition aarch32 specific and 4kiB on other platforms. Long answer: It looks like copy_addr_with_pt is defined to be an address range that is guaranteed to have mapped page tables down to the last level of the page table hierarchy and is therefore suitable for mapping 4kiB pages into (or 64k pages only on aarch32 which is the only supported arch which allows larger pages to also be mapped in at the lowest level page table entries. copy_addr on the other hand is guaranteed to not have a mapped page table at the lowest level of the page table hierarchy which allows for 1MiB, 2MiB, 4MiB and 16MiB page sizes to be mapped here and achieves this by picking a virtual address with alignment of 16MiB above the end of the image but still expecting this to be within the page table that is one level up from the lowest level page table in the hierarchy. Then init_frame tries either region when trying to initialize a frame of varying size between 4kiB and 16MiB. Frames the next size up, 1GiB, would not be able to be mapped by the loader without adding a new copy_addr variable that has larger alignment to guarantee it doesn't collide with a page table at the next level up.

I think The verified kernel configurations don't have a uart driver in the kernel. This decision follows from an L4 design principle that the kernel doesn't provide an implementation for anything that could be provided with an implementation outside of the kernel. In practice, if you know that the loader is only going to be used on a specific platform, then you could write a simple specialized uart driver that you link in instead of the entirety of libplatsupport. and object the None of I don't know the reason for this and it's older than the git history I have access to. It looks like its unnecessary for TCBs, and is likely still necessary for CNodes when loading specs that have CNodes that are moved into slots in other CNodes when constructing a multi-cnode CSpace.

It's a bug because it doesn't do it the same way as Arm, but the way arm does it is a bit misleading. The kernel itself only uses the read and write bits from cap rights for frame mappings, and a cap with write-only rights gets downgraded to kernel-only mapping, so really the kernel only lets you describe read-write, read-only or none. For both read-write and read-only cap abilities, the frame could be mapped exec or non-exec. The read right implies executable rights from the kernel's perspective. The capdl loader does add a little bit of extra security with using the grant right in the spec to imply whether the frame has executable permissions and tries to create the mapping accordingly (except on riscv which is a bug), but if the frame cap for this mapping is also given to the component in order to do things like cache maintenance invocations, then the component could use that capability to convert it's non-exec mappings to executable mappings. There's probably a good argument for overhauling how the kernel handles frame rights so that you can express executeNever as a capability right and associate it with the grant or grantreply bit in the existing capRights. I think this wasn't done originally because either there were no spare bits in the cap structure at the time, or armv6 didn't support executeNever mappings (but you'd have to fact-check me on that). I'm Correct. As I mentioned higher up, some caps are special as originals and allow additional operations to be performed on them compared to their copies even if the cap rights are the same for both. Initializing all of the cnodes in the system involves moving capabilities (seL4_CNode_Move) or deriving capabilities from source capabilities either with the same rights (seL4_CNode_Copy) or lesser rights (seL4_CNode_Mint). Its split into two passes because the derivation of capabilities need to happen before the source capabilities are moved into the destination CNode. of a context is appear to This is true for the kernel with the proofs. The very first implementation of this loader was as part of a project that wanted to verify it using the same tooling as the kernel proofs. So that comment is probably documenting a requirement that is no longer present. this matter where Yea, this one is a bit more involved.