Support badged SMC caps to restrict SMC function IDs

[midnightveil]

Please review commit by commit.

Summary

Add the ability to provide caps for performing SMC invocations which are 'badged',
only allowing certain function invocations. This allows for exposing certain
functions to specific PDs without granting unilateral rights to do anything, i.e.
following a principle of least privilege. This mechanism was explicitly
discussed in RFC 9: New Capability for seL4 SMC Forwarding.

Motivation

The existing Microkit SDF syntax allows for protection domains to be given
SMC capabilities. However, this is an unbadged SMC capability, which allows
access to all SMC functions, i.e. a lot of power over the system.

<protection_domain name="arm_smc" smc="true">
    <!-- elided -->
</protection_domain>

PDs are then allowed to invoke the microkit_arm_smc_call(...) function with
the seL4_ARM_SMCContext *args and seL4_ARM_SMCContext *resp structs. This
performs an invocation on seL4_ARM_SMC_Call(ARM_SMC_CAP, args, resp).

Even if all a PD wants to do is call the PSCI_VERSION (function 0x84000000),
they have all the rights to reboot the system, on/offline CPUs, etc.

seL4 provides a simple mechanism to restrict SMC capabilities; by providing
a badged SMC capability, only function IDs that match the badge are allowed.
For allowing multiple SMC function IDs, one needs multiple badged copies of the
SMC capability.

Proposal

Using the existing <cspace> cap-mapping feature, we add a new node type to the
SDF file, the cap_smc.

<protection_domain name="arm_smc">
    <!-- elided -->

    <cspace>
        <!-- An (ARM) SMC capability that permits SMC calls to 0x84000000 (PSCI_VERSION) -->
        <cap_smc slot="1" function_id="0x84000000" />
    </cspace>
</protection_domain>

User code then looks like this:

#define CAP_SMC_PSCI_VERSION  (microkit_cspace_root_slot_to_cptr(1))

seL4_ARM_SMCContext args = { .x0 = PSCI_VERSION_FID, 0 };
seL4_ARM_SMCContext resp;

seL4_Error err;
err = seL4_ARM_SMC_Call(CAP_SMC_PSCI_VERSION, &args, &resp);
if (err != seL4_NoError) {
    /* error - e.g. if invoked with wrong function ID, etc. */
}

Specifying a function_id="0" is an escape hatch for development, or when you
don't care about security, which provides an SMC capability that is unbadged
and so allows any SMC function call.

As part of this proposal, we remove the microkit_arm_smc_call() and smc="true"
attribute from the Microkit API. This is because the next release, Microkit 3.0.0,
is planned to be a breaking change. This
is the last commit of this PR and could be dropped instead, leaving in a deprecated
API.

Rationale and alternatives

We briefly discuss the choices in the design space made in this proposal.

First, we continue allowing unbadged SMC capabilities to be provided, i.e.
function_id="0". We could instead disallow this entirely and have part of this
include policy to never allow this to be the case. We reject this as it can be
useful for development to allow any function ID.

The second point is the decision to expose the seL4 API and capabilities directly,
for calling seL4_ARM_SMC_Call. This makes it the responsibility of the user
to manage calling multiple SMC call function IDs themselves. This is instead how
CAmkES works: see camkes_get_smc_cap
and vm_smc_handler of CAmkES-VM.

seL4_Word smc_function_id = args->r0;
seL4_ARM_SMC smc_cap = camkes_get_smc_cap(smc_function_id);
seL4_ARM_SMC_Call(smc_cap, &args, &resp);

We could do this in Microkit, too. This requires providing information to the PD
about which SMC capabilities are where, and then providing a function to distinguish
based on function ID. We choose not to do this, generally we only pass information
to PDs when the user requests, e.g. setvar, and it is up to the user to choose
how to encode data about the system in their program; Microkit just provides the
mechanisms.

Original README

Original README

Note: this contains a breaking change by removing the SMC attribute.
This should be fine, as the 3.0.0 release is planned to be breaking anyway.
This change could be reverted; it is left as a separate commit to make that easy.

The other design choice here was that we do not permit "function_id=0", or some other way to make badge = 0 <=> unbadged smc cap which has no allowlisting, instead allowing everything. This is always (in my opinion) a bad design.

<system>
    <protection_domain name="arm_smc" priority="1">
        <program_image path="arm_smc.elf" />

        <cspace>
            <!-- An (ARM) SMC capability that permits SMC calls to 0x84000000 (PSCI_VERSION) -->
            <cap_smc slot="1" function_id="0x84000000" />
        </cspace>
    </protection_domain>
</system>

[Indanz]

The current way of doing SMC is by setting an attribute smc=true on the PD description and calling microkit_arm_smc_call().

The proposed way is using the recently added cap export mechanism and letting users call seL4_ARM_SMC_Call() directly on that cap.

I agree that this is a better API, as it is more generic and avoids the Microkit wrapper function.

However, the cap_smc part makes it SMC specific again. That's probably in line with the other exported caps, but I would have made it more generic and support all boot caps and have a generic badge thing instead of function_id, which requires SMC specific code again. I think I made the same comment on other caps exported via cspace.

I would not disallow function_id="0" for unbadged SMC caps, that is user policy. It can be handy for testing and if a process needs to do multiple SMC calls and one of them is destructive, then it doesn't add much to badge the caps.

[dreamliner787-9]

That's probably in line with the other exported caps, but I would have made it more generic and support all boot caps and have a generic badge thing instead of function_id, which requires SMC specific code again.

If I understand correctly your proposal is something like this?

<system>
    <protection_domain name="arm_smc" priority="1">
        <program_image path="arm_smc.elf" />
        <cspace>
            <cap_initial type="smc" badge="0x84000000" slot="1"/>
        </cspace>
    </protection_domain>
</system>

Then type is just these:

This would be interesting and a step toward adding a dynamic escape hatch to Microkit,

out of date

[midnightveil]

FYI, reason why I pinged you both is because this is somewhat closer to #362 than perhaps it should be, utilising the cspace element which was merged previously without wider discussion.

I don't know if it's worth a proper RFC about whether we should make Microkit abstract away multiple function IDs as part of its API.

[Indanz]

If I understand correctly your proposal is something like this?

<system>
    <protection_domain name="arm_smc" priority="1">
        <program_image path="arm_smc.elf" />
        <cspace>
            <cap_initial type="smc" badge="0x84000000" slot="1"/>
        </cspace>
    </protection_domain>
</system>

One step further, type can also be something else, like "tcb", "sc", but then it needs a source attribute to find the correct one, likefrom="pd name". The equivalent for the above would be:

<cap type="SMC" from="init" badge="0x84000000" slot="1"/>

Of course, from="init" could be the default, so you can leave it out.

(And it's perfectly fine to have aliases like function_id so you can use that instead of badge. But I wouldn't try to restrict it to just SMC caps, that would add unnecessary code. It can also make it harder for other tools parsing the SDF, so maybe better not.)

This would be interesting and a step toward adding a dynamic escape hatch to Microkit,

It's not just an escape hatch, it's a more generic way to copy caps.

The advantage is that cap type specific code is contained to the cap lookup part and that the rest of the code can be generic. That means you can add new cap types without changing the XML format.

The type attribute isn't used as a real type, it's just a way to specify which cap it is, because here's no other way to do that.

[Indanz]

FYI, reason why I pinged you both is because this is somewhat closer to #362 than perhaps it should be, utilising the cspace element which was merged previously without wider discussion.

I'm in strong favour of #362, but it's not up to me, what do actual users of Microkit think?

I don't know if it's worth a proper RFC about whether we should make Microkit abstract away multiple function IDs as part of its API.

I wouldn't do that, that doesn't seem within scope of Microkit. Don't forget all you can count on is the SMC Calling Convention, you can't count on it following e.g. PSCI.

[midnightveil]

I wouldn't do that, that doesn't seem within scope of Microkit. Don't forget all you can count on is the SMC Calling Convention, you can't count on it following e.g. PSCI.

I'm specifically thinking about an equivalent to camkes_get_smc_cap.

[Furao]

I understand wanting to generalize this and provide a very powerful tool for advanced seL4 developers, but I think it would be quite confusing for newer developers, especially if its the only option.

<system>
    <protection_domain name="arm_smc" priority="1">
        <program_image path="arm_smc.elf" />
        <cspace>
            <cap_initial type="smc" badge="0x84000000" slot="1"/>
        </cspace>
    </protection_domain>
</system>

Presumably there will be some updates to the documentation, but a user needs to understand that they need a cap of type SMC for each smc call they want to allow and that the func_id is represented by the badge (which isn't actually mentioned in the seL4 User manual). Then they need to understand what value to use for slot.

While the microkit API is somewhat inconsistent about what it provides, it has provided benefit by abstracting some of the more confusing parts of the microkernel.

Do you think we could support both approaches?

The commented proposal provides the escape hatch which essentially lets you do whatever you need with initial_caps, but is likely only going to be used by advanced developers.

Then Microkit could still provide abstractions on commonly used functionality, such as SMC. As a user, I would hope for a more simple specification such as this:

<system>
    <protection_domain name="arm_smc" priority="1">
        <program_image path="arm_smc.elf" />
        <allowed_smc_calls>
            <smc_call func_id="0x84000000"/>
            <smc_call func_id="0x84000020"/>
            <smc_call func_id="0x8400003A"/>
        </allowed_smc_calls>
    </protection_domain>
</system>

You could also have a more obvious way to specify things like allowing all calls, without needing to understand how that is actually done:

<system>
    <protection_domain name="arm_smc" priority="1">
        <program_image path="arm_smc.elf" />
        <allowed_smc_calls allow_all="true" />
    </protection_domain>
</system>

[midnightveil]

OK, thanks for the feedback. I think your proposal makes sense.

I'll propose that this generates the metadata used for a microkit_get_smc_cap(function_id) function.

Just to confirm, the other proposal was this, which is explicit about function IDs:

<protection_domain name="arm_smc">
    <!-- elided -->

    <cspace>
        <!-- An (ARM) SMC capability that permits SMC calls to 0x84000000 (PSCI_VERSION) -->
        <cap_smc slot="1" function_id="0x84000000" />
    </cspace>
</protection_domain>

Not cap_initial which does then use badge, which I agree is quite confusing.

[midnightveil]

Something to note that if we do provide an microkit_get_smc_cap cap function, we need to actually implement it. CAmkES does code generation, which in the end makes the code do O(n) checks against the values with immediates in the instruction stream - godbolt. For Microkit we'd have to patch in values at runtime and probably do a linear search through an array, unless we want the complexity of a perfect hash function or a binary search. I don't think that's worth the tradeoff, but when it is a Microkit provided function, as opposed to <cap_smc slot="1" function_id="0x84000000" /> this is policy Microkit imposes. However, we can actually impose policy with Microkit, the question is do we want to?

[Indanz]

Presumably there will be some updates to the documentation, but a user needs to understand that they need a cap of type SMC for each smc call they want to allow and that the func_id is represented by the badge (which isn't actually mentioned in the seL4 User manual).

Yes, SMC is currently not properly documented in the manual, other than the SMC syscall with too little information, see seL4/seL4#1422.

Do you think we could support both approaches?

The old, simple way can be retained easily enough.

As a user, I would hope for a more simple specification such as this:

<system>
    <protection_domain name="arm_smc" priority="1">
        <program_image path="arm_smc.elf" />
        <allowed_smc_calls>
            <smc_call func_id="0x84000000"/>
            <smc_call func_id="0x84000020"/>
            <smc_call func_id="0x8400003A"/>
        </allowed_smc_calls>
    </protection_domain>
</system>

Implementing this would be quite tricky in Microkit though: It would need to pass the func_id<->cap mapping to user space via e.g. bootinfo and use that to check if the call is allowed and find the right cap. Maybe this could be done via setvar or something, but that's not exactly user friendly either at this point.

I think it would be much simpler to expand the existing way by adding function_id support instead of just "true", like smc="func_id". That's simple to implement and use for both the user and Microkit, while being backward compatible.

The complicated cspace way can be used for when that's not good enough.

But adding more and more very use case specific, tricky code to Microkit is exactly the kind of thing that I'm trying to push back against. Simple wrappers for simple things is somewhat fine, but now you're proposing to add complicated wrappers for complicated things, without supporting all use cases. That's the road to bloatware, subtle bugs and maintenance hell in 10 year time.

Maybe Microkit is already really close to mapping a read-only page per process with PD-specific metadata, then adding this wouldn't be too bad I suppose...

[Furao]

Presumably there will be some updates to the documentation, but a user needs to understand that they need a cap of type SMC for each smc call they want to allow and that the func_id is represented by the badge (which isn't actually mentioned in the seL4 User manual).

Yes, SMC is currently not properly documented in the manual, other than the SMC syscall with too little information, see seL4/seL4#1422.

Do you think we could support both approaches?

The old, simple way can be retained easily enough.

As a user, I would hope for a more simple specification such as this:

<system>
    <protection_domain name="arm_smc" priority="1">
        <program_image path="arm_smc.elf" />
        <allowed_smc_calls>
            <smc_call func_id="0x84000000"/>
            <smc_call func_id="0x84000020"/>
            <smc_call func_id="0x8400003A"/>
        </allowed_smc_calls>
    </protection_domain>
</system>

Implementing this would be quite tricky in Microkit though: It would need to pass the func_id<->cap mapping to user space via e.g. bootinfo and use that to check if the call is allowed and find the right cap. Maybe this could be done via setvar or something, but that's not exactly user friendly either at this point.

I think it would be much simpler to expand the existing way by adding function_id support instead of just "true", like smc="func_id". That's simple to implement and use for both the user and Microkit, while being backward compatible.

The most important part for me personally is that I need to support around 20 to 30 function IDs for each VM on the ZCU102.

The complicated cspace way can be used for when that's not good enough.

But adding more and more very use case specific, tricky code to Microkit is exactly the kind of thing that I'm trying to push back against. Simple wrappers for simple things is somewhat fine, but now you're proposing to add complicated wrappers for complicated things, without supporting all use cases. That's the road to bloatware, subtle bugs and maintenance hell in 10 year time.

Yes, I see that argument.

Maybe Microkit is already really close to mapping a read-only page per process with PD-specific metadata, then adding this wouldn't be too bad I suppose...

[midnightveil]

Maybe Microkit is already really close to mapping a read-only page per process with PD-specific metadata, then adding this wouldn't be too bad I suppose...

Yeah, we have a bunch of separate setvars already for things like this. I was considering something here: #422.

But we can do this with setvars.

---

I am leaning towards Microkit providing this feature, I think.