On 1/27/20, Klein, Gerwin (Data61, Kensington NSW)
<
Gerwin.Klein@data61.csiro.au> wrote:
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.
capDL limitations won't be an issue for UX/RT since it won't use capDL
at all (the only user code in common with CAmkES will be libsel4, with
the other low-level code being Rust-based and derived from feL4 and
Robigalia). Kernel capabilities will just be treated as a supervisor
implementation detail and not exposed to applications at all (only the
root server and the low-level system library will deal with kernel
objects directly). File descriptors and mapping descriptors
(identifying a specific mapping of a file) will be the only true
capabilities that normal user programs see (they will be wrappers for
groups of kernel capabilities). There will also be process file
permissions that will be capability-like in that they can be
transferred securely between processes, but unlike true capabilities
will not serve as identifiers. These will be the main security
mechanism, since they will be more compatible with Unix software than
a pure capability model.
I wouldn't think that they'd be an issue for CAmkES either since it
probably wouldn't ever need to merge any untyped objects. Not sure
about Genode, but AFAIK it uses its own XML-based capability
definition language everywhere rather than using capDL, and it treats
untyped objects as an implementation detail much like UX/RT.
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.
Yes, requiring the user process to revoke the capability first would
probably actually make more sense.
On 1/27/20, Klein, Gerwin (Data61, Kensington NSW)
<
Gerwin.Klein@data61.csiro.au> wrote:
Still not quite sure I understand correctly what seL4_Untyped_Replace would
do. The description above sounds like the following:
- c_u: a cap to an untyped
- c_o: a cap to an object retyped from that untyped, i.e. c_u is the direct
parent of c_o
- you want a retype operation that is equivalent to:
- revoke c_o
- delete c_o. There is now a hole in somewhere in the space covered by
c_u.
- retype a new object of equal or smaller size into the space made
available by that hole
Yes, that's exactly what I meant.
In terms of kernel design, this one is harder to justify to the minimality
principle, because you could achieve the same effect with the additional
untyped cap that I think you were mentioning before, i.e. between c_u and
c_o, have a cap c_u2 of the size that is needed for c_o, and revoke/retype
that one (which also neatly covers what could go wrong if the authorising
cap disappears, e.g. because some overlord server revoked everything — the
kernel would catch that at invocation time of the in-between untyped).
UX/RT won't have to deal with issues relating to revocation of the
parent untyped, since only the root server will deal with untyped
objects and it will only ever use one copy of each untyped capability,
although that could be a problem for other OSes with a more recursive
architecture.
Given the size of most objects, one untyped cap per object sounds like not
too bad of an overhead, but of course this also means managing the
relationship between these untypeds and the object caps.
It's still more overhead than the Linux kernel's buddy allocator,
which uses bitmaps to track free blocks, rather than having to use
some kind of associative array. I know that some use of associative
arrays is probably unavoidable (at least with the allocator design I'm
using), but it would be nice to have as few capabilities as possible
so as much as possible can be tracked with bitmaps.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel