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