Re: [seL4] Are there any plans to re-add seL4_Untyped_RetypeAtOffset?

On 26 Jan 2020, at 12:40, Andrew Warkentin wrote:

As an alternative to seL4_Untyped_RetypeAtOffset, would it maybe be possible to add an seL4_Untyped_Merge invocation that would take two adjacent untyped objects and a third slot for a destination and merge them into a single untyped, revoking the original two untypeds, and an seL4_Untyped_Replace invocation that would be similar to seL4_Untyped_Retype except that it would revoke the original untyped (failing if called on an initial untyped object). These would allow almost comparable optimizations to seL4_Untyped_RetypeAtOffset (although some "filler" untyped objects for free blocks would still have to be created). Could these be implemented without a searchable CDT? Would they be any easier to verify?

In terms of verification, seL4_Untyped_Merge would be much easier than the searchable CDT (because it is fairly local), functional correctness probably an order of magnitude. Thinking through confidentiality, integrity, availability, and capDL theorems this also sounds fine, if you present both untyped caps, you are not gaining more authority by merging them. capDL can probably not express the operation (it doesn’t have the information wether two untypeds are adjacent) but doesn’t really need to, since you wouldn’t run it in system initialisation. In total probably 6-8 weeks of verification work. You likely would want to tweak the operation such that user space does the revocation in a separate syscall to avoid reasoning about preemption in the new operation. In terms of wether seL4_Untyped_Merge is a good kernel primitive I have to admit I initially found it somewhat ad-hoc, but the longer I think about it, the more sense it makes. It’s the reverse of incrementally splitting untypeds as far as that can be done, and it’s not something one could achieve in user space. Would have to have a bit more discussion with the kernel design experts if there is something that should be tweaked, but it sounds reasonable to me at the moment. I’m not sure I understand the need for seL4_Untyped_Replace. Is the only difference between seL4_Untyped_Replace and seL4_Untyped_Retype that the original Untyped disappears? If so, I think one could achieve that already by seL4_Untyped_Retype and then deleting the parent cap without revoking. Cheers, Gerwin