Was this paper discussed here before?

[Alex Potanin]

https://www.usenix.org/system/files/usenixsecurity26-mauthe.pdf

The authors start from the observation that capability operating systems have existed for six decades yet there is no systematic way to compare them, nor even consensus on what capabilities are for. They give a precise definition of a capability system, separate three capability models to clear up common misconceptions, and then derive eleven additional characteristics (e.g. how capabilities are obtained, delegated and revoked) that can be used to describe and distinguish systems. These characteristics are applied to a systematically collected corpus of seminal and recent capability systems — from Dennis & Van Horn, Hydra, EROS, Amoeba, Mach and seL4 through CHERI/CheriOS/CHERIoT, Capsicum, Fuchsia, M3 and Linux capabilities — producing a taxonomy (Table 1) with three archetypes: Ticket Capability Systems, Object Capability Systems and a newly identified class of IPC Capability Systems. The analysis is used to surface open challenges in building pure object-capability systems and to list research directions, with four stakeholder groups considered. The paper-collection tooling is released as an artifact.

[Mark S. Miller]

Looks like a great paper!

> --
> You received this message because you are subscribed to the Google Groups "cap-talk" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/cap-talk/a24bfcaf-11d8-4610-905c-b827dc5ec0a2n%40googlegroups.com.



--
Cheers,
--MarkM

[Gernot Heiser]

On 24 Oct 2026, at 08:57, Mark S. Miller <eri...@gmail.com> wrote:
>
> Looks like a great paper!

I have a number of issues with it. Need to finish reading, though

Gernot

[Gernot Heiser]

On Thu, Oct 22, 2026 at 9:49 AM 'Alex Potanin' via cap-talk
<cap-...@googlegroups.com> wrote:

https://www.usenix.org/system/files/usenixsecurity26-mauthe.pdf

On 24 Oct 2026, at 10:08, Gernot Heiser <gernot...@gmail.com> wrote:

On 24 Oct 2026, at 08:57, Mark S. Miller <eri...@gmail.com> wrote:

Looks like a great paper!

I have a number of issues with it. Need to finish reading, though

OK, here we go (haven’t read S6 yet).

# Notes on Mauthe et al, Usenix'26

## General

Doesn't mention several systems that clearly should be mentioned (all directly cite at least one of the 9 publications they use as the root of their graph). Specifically:

* KeyKOS: cites [58} & other Hydra paper, 171 cites according to GS

* Angel: cites [76]

* Mungi: cites [11,58} & SOSP version of [96], 194 cites according to GS

This is reflective of an unstated & unmotivated HW bias -- this is clearly not written by OS people.

Most evident in C12, which cannot be satisfied by software implementations. However, this criterion based on a fundamental misconception. Clearly, the cap AC must be implemented somewhere, and that somewhere has full access to everything ("ambient authority"). Somehow the authors imply that doing this in hardware doesn't matter, but doing it in software does. If given the choice between an unverified HW implementation and a verified SW implementation, I know what I'd choose!

In terms of SW implementations, they seem to prefer sparseness-protected user-level caps (which is sort-of understandable given their HW bias, in that these are more like tagged caps in behaving like normal data). I used to think similarly 20 years ago. But given the massive privilege amplification you get from covert channels (leaking a few dozen bits gives you full access to an object) I don't think these constitute a defensible approach these days.

## Specific comments on their criteria:

### Composability C4

This requires that in order for A to delegate O to B, A needs access to B, and claims that this "can be used for implementing separation of duties, strong encapsulation, and highly privileged applications that follow [POLA]". They also claim that seL4 doesn't have that property.

I challenge this on multiple levels.

For one, seL4 clearly provides this functionality: If A has a cap to B's Cspace, it can insert the cap to O there, which is exactly what I understand this definition to require.

However, using this delegation method clearly violates POLA. Why does A need control over B to delegate a cap? seL4 (like many others, incl EROS IIRC, which by the way they claim does satisfy C4) has a better mechanism: A can send a cap over IPC (an Endpoint), as long as A has Grant right on the EP, and B can receive that right, without giving A any rights over B itself. That looks much more like POLA to me. And it certainly provides better encapsulation.

### Policy-controlled delegation C8

EROS is the only system the credit with this, all others, incl seL4, do not, according to the paper.

seL4's formally verified information-flow control explicitly disproves this assessment.

### Protection domain tracing C9

Maintaining "centralized mapping of subjects to their respective protection domains."

I'm not exactly sure what this means; they claim it's satisfied for.few systems (EROS being one of them, seL4 not). 

In seL4, Cap tables (Cspaces) are kept in the kernel, pointed to by thread control blocks, is that not centralised and mapped from subjects? Maybe it comes down what Subjects are? Strictly speaking, I'd say it's Cspaces themselves, as they define access. If you think it should be active entities, then it's threads, but they point directly to Cspaces. According to C10 (Minimal Subject Unit) they claim seL4 subjects are "processes", which would mean address spaces (VSpaces). You could argue that there's no direct reference from a VSPace to a CSpace, but it's the thread that invokes the cap, so I really don't understand what this is to mean.

### Single-level store C11

That's simply a policy that should be implemented on top, I don't see the relevance of this.

### Ringless system design C12

Discussed above, misconception on what the TCB is

### Persistence C13

Again, this is orthogonal to caps (and suspect Shap agrees, given that Coyotos went away from this).

### Explicit revocation C14

Again, I have no clue in which way seL4 doesn't satisfy that, it clearly has targeted revocation

### Exclusive access C15

This, again, seems a hardware-focussed view that is pretty meaningless for a software implementation of capabilities, where you can use standard locking strategies or OS mechanisms to synchronise access. In any case, it seems obvious that this can be implemented by revoking all other caps to an object, resulting in exclusive ownership.

So, I doubt that this is a property that needs to be inherent in the cap system, but in any case is something that can be achieved in seL4.

### Cooperative access C16

I'm not exactly sure what it means to be able to "designate only" vs operate on an object.

seL4 has caps with no rights that "designate" an object. But it seems the intent is more what we get when we encapsulate data into a server (that has exclusive access) and invoke that server via a protected procedure call (IPC).

## Taxonomy

I'm not sure how useful this distinction of "ticket cap", "Ocap" and "IPC cap" systems is, but I'm definite that seL4 is clearly misclassified. They write:

"These [IPC cap] systems stand out because the objects they consider - IPC and RPC channels - are their defining features. By their very design to focus on IPC protection, they are hybrid capability systems, i.e., they mix capability-based access control for IPC with other forms of access control for everything else."

Putting seL4 into that category is simply nonsense, as all resources are cap controlled, even kernel memory (which goes much further than any other system I know of).

[Matt Rice]

On Fri, Oct 23, 2026 at 11:05 PM Gernot Heiser <gernot...@gmail.com> wrote:
>

> ### Persistence C13
>
> Again, this is orthogonal to caps (and suspect Shap agrees, given that Coyotos went away from this).

Hopefully Shap chimes in, but my recollection is that coyotos explored
whether and how far persistence could be kicked out of the kernel/tcb,
But eventually it was decided to keep it, I do not recall it actually
being implemented after that.

The ability to reconstruct capabilities purely from data is a very
powerful operation.
One which I've never figured out a way to do efficiently with the seL4
untyped/retype mechanism given inability to read capability metadata
and type codes outside the kernel.
I don't know what the plan for it was, whether the ability to read the
metadata and typecode of a capability was to be governed by a
capability or something, along with userspace device drivers. But the
priority definitely seemed to be running coyotos as an ephemeral
system.

[William ML Leslie]

On Fri, 23 Oct 2026 at 02:49, 'Alex Potanin' via cap-talk <cap-...@googlegroups.com> wrote:

https://www.usenix.org/system/files/usenixsecurity26-mauthe.pdf

The authors start from the observation that capability operating systems have existed for six decades yet there is no systematic way to compare them, nor even consensus on what capabilities are for. They give a precise definition of a capability system, separate three capability models to clear up common misconceptions, and then derive eleven additional characteristics (e.g. how capabilities are obtained, delegated and revoked) that can be used to describe and distinguish systems. These characteristics are applied to a systematically collected corpus of seminal and recent capability systems — from Dennis & Van Horn, Hydra, EROS, Amoeba, Mach and seL4 through CHERI/CheriOS/CHERIoT, Capsicum, Fuchsia, M3 and Linux capabilities — producing a taxonomy (Table 1) with three archetypes: Ticket Capability Systems, Object Capability Systems and a newly identified class of IPC Capability Systems. The analysis is used to surface open challenges in building pure object-capability systems and to list research directions, with four stakeholder groups considered. The paper-collection tooling is released as an artifact.

I really enjoyed this paper.  Here are a few concerns that I had reading it.

This paper references the man page on linux (or posix) capabilities, which are not capabilities according to any reasonable definition.  Evidently the authors just liked the word.

The difference between EROS and Coyotos is mostly about IPC performance and generality, and the difference between Coyotos and seL4 is mostly about persistence and heap typing.  These are all capability systems, but I don't think the differences have any bearing on the capability system itself.  Persistence and the SLS are interesting topics, but they are orthogonal to capability systems.  I don't understand the distinction between 5.3 "IPC capability systems" and 5.2 "Object capability systems".

I share Gernot's frustration with the HW bias.  If you are forced to work with commodity hardware - and I assume if your bank account looks anything like mine, that's you too - whether or not the hardware provides protection rings or any more capability-friendly separation tools is just not up to the system designer.  It's not an interesting feature of the architecture, it's a technical limitation that nevertheless hasn't prevented you from building a capability system. A capability system is often a lintel, supporting the bricks over a gaping security hole that is modern hardware.

I am a bit frustrated at the talk of "subjects" having a "set" of capabilities.  While there's a sense in which it's true, at no time do capability systems rely on the fact that a component has a "set" of capabilities, or otherwise "aggregated at the subject level".  It has capabilities, and it decides precisely which ones to use.  You could use this "set" notation to limit your review in an audit, but if this is discussed anywhere, I did not notice.  Your audit will be easier if you don't flatten them semantically into a set.  I think this mistake shows itself clearly in 6.4 "Avoiding Confused Deputies" where it says that "Giving the capability to the deputy alone would not mitigate the risk of confusion".  This entire paragraph appears to be hallucinated.

Section 6.5, limitations of the access control matrix, perhaps would do better discussing the fact that the access control matrix is a static view of the system.  It should be clear at this point that the failure to understand the dynamic nature of real security properties was Lampson's fatal flaw.

Systems where capabilities rely on unguessability (which is what I think I understand the "ticket capability systems" section to be discussing) are a necessity in any situation where you don't own all of the computing infrastructure, which is not surprisingly most of what people do with computers these days.  The lack of confinement is understood in this case, and probably not especially desirable, either.  We usually want confinement as an internal property of a system.

I don't know why they think explicit revocation isn't possible in this case.  There are multiple ways to achieve it.  You can have delegation be an explicit step involving the server, so the server can participate in revocation.  Or it can be done by proxying.

The paper's paragraph on the TCB is valuable, and I think most of the take away for why to formalise and build on capability systems.

On revocation, it is always valuable, but often hard to implement cheaply.  Linear capabilities and other techniques to simplify revocation is a rich area of exploration.

--

William ML Leslie

responsible ai use is not a thing