RFC-22: SBI capability

[Ivan-Velickovic]

This RFC proposes a new SBI capability for the purpose of accessing hardware protected by machine mode (M-Mode).

An initial implementation is available at seL4/seL4#1532.

[Indanz]

(Rendered version here.)

The 28-bit limit on EID is not sufficient to hold currently defined extensions, most are actually 31-bits, including:

• Timer Extension, EID 0x54494D45, 31-bits
• RFENCE Extension, EID 0x52464E43, 31-bits
• System Reset Extension, EID 0x53525354, 31-bits
• Debug Console Extension, EID #0x4442434E, 31-bits

The EIDs used seem to be somewhat random 31-bit numbers. The standard says it are signed 32-bit numbers, so a practical limit of 31-bits seems reasonable to assume.

Otherwise I'm in favour of this RFC, same rationale as SMC applies.

[Ivan-Velickovic]

The EIDs used seem to be somewhat random 31-bit numbers. The standard says it are signed 32-bit numbers, so a practical limit of 31-bits seems reasonable to assume.

I mistakenly assumed that the spec ordered the chapters by EID value and since the last chapter (firmware specific extension space) uses 28-bits that that was the maximum EID value.

Thank you for checking that. I will fix the EID to use 31-bits and then decrease the bits for FID.

[Ivan-Velickovic]

The EIDs used seem to be somewhat random 31-bit numbers

I believe the encoding is based on the name, e.g for timer the bits used convert to ASCII for "TIME".

[Indanz]

The PR is twice the size of the Arm SMC one, mainly because of badging per EID and FID, which adds a lot of complexity for not much gain. This double badging is also hard to explain to users, because it is not intuitive: SBI caps have effectively two badge values in this proposal.

One level of badging as has been done for SMC and combining the EID and FID bits into one badge value would simplify things a lot, but is only possible for 64-bit and not for 32-bit. Typically RISC to waste so many bits on inefficient encoding.

Some kind of complexity is needed to work around the 32-bit badge limitation, I'm not sure whether what we have now is the best way of dealing with it.

Possible alternatives:

1. Add an enum for the EIDs and combine those with the FID into one value. This would mean you have to create a cap per EID+FID combination like for SMC. There are 15 EIDs defined (counting the reserved ranges as one each), so we need 4 bits for those. That leaves 28 bits for FID (or rest of EID+FID for the ranges). But it would be more efficient to combine the extensions which have only one or few functions into one group, but that requires extra decoding. Limiting FID to e.g. 26 bits seems a better compromise.
2. Forget about FID, and only do badging for EID. This works fine in practice, except for a few scary exceptions like Console Read and PMU snapshot shared memory.
3. Do badging for EID, but add an extra syscall to set FID (it can only be set once).

[Ivan-Velickovic]

There are 15 EIDs defined (counting the reserved ranges as one each), so we need 4 bits for those

Will this work for the vendor specific/firmware EIDs which depend on the SBI implementation? There could be any number of those.

[Indanz]

There are 15 EIDs defined (counting the reserved ranges as one each), so we need 4 bits for those

Will this work for the vendor specific/firmware EIDs which depend on the SBI implementation? There could be any number of those.

That was the whole point. If we use 4 bits for the enum, we have 28 bits for the rest, which can include the lower bits of the EID. But I forgot we then still have to define a split between those lower EID bits and the FID bits.

[Indanz]

It does say:

The lower 24 bits of the firmware EID must match the lower 24 bits of the SBI implementation ID

and

The lower 24 bits of vendor specific EID must match the lower 24 bits of the mvendorid value.

So at least the firmware and vendor EIDs are not arbitrary and we don't have to check them (because there is only one valid value), we can use all the remaining bits for FID.

For the experimental extension it would make more sense to use the remaining bits for EID and not check FID, or to split it 50/50 or something.

Edit: So for simplicity we could make the behaviour the same for experimental features as for firmware and vendor EIDs, and just not check the other bits of the EID. It's still better than using an unrestricted, unbadged cap. I don't think it matters too much what we do here. To use new, standard EIDs seL4 doesn't know about yet users would already need to use unbadged caps.

[Indanz]

Variant 4: No badging at all, just another syscall to set both EID and FID. Then we can use 32 bits for EID and 28-bits for FID. A zero EID would imply EID and FID are unrestricted, a non-zero EID would imply both EID and FID must match the set ones.

[kent-mcleod]

Is the cap needed for riscv32?

[Indanz]

Is the cap needed for riscv32?

Aarch32 doesn't have SMC either, so making SBI caps 6-bit RISCV-only would solve all problems too. Let's call that variant 5.

[kent-mcleod]

2. Forget about FID, and only do badging for EID. This works fine in practice, except for a few scary exceptions like Console Read and PMU snapshot shared memory.

Also you can further "attenuate" the rights of a cap by giving it to a user level server that can apply more specific access policy to clients.

[Indanz]

Also you can further "attenuate" the rights of a cap by giving it to a user level server that can apply more specific access policy to clients.

True. We could do EID-only for 32-bit and EID+FID for 64-bit.

[lsf37]

2. Forget about FID, and only do badging for EID. This works fine in practice, except for a few scary exceptions like Console Read and PMU snapshot shared memory.

Also you can further "attenuate" the rights of a cap by giving it to a user level server that can apply more specific access policy to clients.

I strongly object to that option. It is a direct violation of the principle of least privilege. The whole purpose of these caps is to be able to restrict authority in the system and safely make some very specific aspects of the underlying machine-mode code available to user space safely.

This authority in particular (like SMC) is of the catastrophic kind, i.e. it is a huge hole in the proof assumptions and it leads right into completely unverified, not very high quality code that runs at a higher privilege level than the kernel. It undermines everything. If the kernel is not even able to restrict that and always requires trusted user-level code to run any of these functions, we don't really need to bother with security for the rest of the kernel.

If you ever want to certify a system that uses SMC or SBI calls, you will want to know exactly which calls can be made, and you want to be able to nicely list those and prove that no other calls can ever be made. Even if the user-level component that makes these calls is trusted, you don't want to require the same level of formal verification for it as you would for the kernel. All of that can be easily achieved if you have a verified initialiser that produces caps that only allow you to make specific calls and you can show that those caps are only available to your trusted component.

[lsf37]

It sounds to me like the main objection to the proposed API is "hard to explain to the user". For that: a) I disagree, it is easy to explain with two code examples and b) this is a non-goal -- it doesn't matter if it is hard to explain. What matters is if it achieves security, performance, and verification, and I would argue that it does that better than all of the other variants proposed so far.

I'll go into more details on the variants below, but first: I do agree that the proposal is complex, which does have an influence on verification. We do not have any two-level badging for anything else in the kernel, and while the API is designed carefully to use the existing interfaces that the proofs talk about, it will be necessary to reason through those deeper cap derivation tree levels, which will be annoying and subtle.

The main reason we did not go with just flat badging (AFAIR) was user convenience (also a non-goal, but if everything else is equal, it's still good) and the fact that on rv32, we don't have an existing mechanism to set >32 bit badges on caps even if storage space in the cap is available.

Two new options that sound viable to me that have less complexity are:

5. extend the existing badge mechanism in general with something like a "long" badge, i.e. two data words that are set in the mint/mutate operations, and use that for flat full EID+FID badges on rv32. (Use the normal old badging mechanism for rv64, or also two simultaneous badge words if that is more consistent/convenient -- wouldn't really matter at that point)

6. not support SBI calls on rv32 (unclear to me if that is actually an option -- it was for SMC, but that doesn't mean it is here), and use a flat 64 bit badge on rv64 for EID+FID.

More details on the other variants:

1. adding encoding details for a tighter encoding could work, but it would mean that the kernel now knows a lot more about the structure of SBI than in the current proposal and if we get anything wrong there, we have no guard rails. I.e. we reduce the value of verification with that option. We can still do that if nothing else works, but if we have other options, I don't think it's preferable.

2. absolutely not, see other comment. If we do that, we don't really need to bother with any badging at all, or with verification for that matter.

3. extra syscall: this does not solve anything, and would increase the size of the code change instead of reducing it. It would also be a lot harder to verify. There are two existing mechanisms that we can re-use verification for: normal badging via mint/mutate (which is exactly what that mechanism was designed for) and the control cap/instance cap pattern. In the latter, we get mostly duplication. We did that for SGI caps, because they fit with the existing interrupt handler pattern and could re-use some of that mechanism, but that would not apply here.

4. is a variation of 3 with the same downsides

In more detail, for verification for the new options we have:

5. verification cost on extending the general API to (optionally) long badges would be smaller than reasoning about double-badging as we have in the proposal now. The only interface that changes with long badges in terms of the proofs is argument decoding and the function that sets the cap data. Both are easy. How the cap data is interpreted for the cap derivation tree is independent of all that and if we make it flat, it'd be the same reasoning as we have now, just checking an additional field. That would overall be simpler. It would also open up that mechanism for any future APIs that want more user-modifiable cap data.

6. the simplest of all, of course, but I don't know if that's an option

[Ivan-Velickovic]

A draft implementation of variant 5 is available at seL4/seL4#1547.

[lsf37]

A draft implementation of variant 5 is available at seL4/seL4#1547.

It looks like variant 5 is the better option. The summary of variant 5 is:

Extend the existing badge mechanism in general with a "long" badge, i.e. two data words that are set in the CNodeMint operation, and use that for flat full EID+FID badges. Still allow invocations on the 0-badge with all invocations like for SMC.

Thanks to seL4/seL4#1551, the general long-badge mechanism can be a variation of CNodeMint without having to add a separate CNodeMintLong invocation that duplicates the decoding logic there (as in the current draft implementation).

NB: the mechanism is added only to CNodeMint, because CNodeMutate does not allow setting badges in general

This is better than the current version of the RFC text that proposes a two-level Mint operation, because it is less complex and offers a nice generalisation of CNodeMint that is likely to be useful for future capabilities that have space for larger badges (compared to endpoints and notifications). It is also straightforward to verify because it aligns very closely with the mechanisms for SMC caps that currently are under verification.

If people are happy with this, my proposal would be to update the RFC accordingly and go ahead with variant 5.

[mbrcknl]

Sorry I'm late to the discussion. To be clear, I'm not suggesting to change anything. Variant 5 seems good.

2. Forget about FID, and only do badging for EID. This works fine in practice, except for a few scary exceptions like Console Read and PMU snapshot shared memory.

Also you can further "attenuate" the rights of a cap by giving it to a user level server that can apply more specific access policy to clients.

I strongly object to that option. It is a direct violation of the principle of least privilege. The whole purpose of these caps is to be able to restrict authority in the system and safely make some very specific aspects of the underlying machine-mode code available to user space safely.

This authority in particular (like SMC) is of the catastrophic kind, i.e. it is a huge hole in the proof assumptions and it leads right into completely unverified, not very high quality code that runs at a higher privilege level than the kernel. It undermines everything. If the kernel is not even able to restrict that and always requires trusted user-level code to run any of these functions, we don't really need to bother with security for the rest of the kernel.

If you ever want to certify a system that uses SMC or SBI calls, you will want to know exactly which calls can be made, and you want to be able to nicely list those and prove that no other calls can ever be made. Even if the user-level component that makes these calls is trusted, you don't want to require the same level of formal verification for it as you would for the kernel. All of that can be easily achieved if you have a verified initialiser that produces caps that only allow you to make specific calls and you can show that those caps are only available to your trusted component.

But I do want to give an alternative viewpoint:

• Anything you can say about the need to restrict the EID or FID, you could in future find yourself saying about particular combinations of the 5 argument words, or even particular combinations of arguments in the context of previous SBI calls. The need for user-level attenuation of high-powered caps seems inevitable.
• We don't have a verified initialiser. If we can verify an initialiser in a way that ties into the security theorems, then we can do the same for user-level attenuation. And I am increasingly confident that we will do both. (Just not in the very near future.)

[Indanz]

* Anything you can say about the need to restrict the EID or FID, you could in future find yourself saying about particular combinations of the 5 argument words, or even particular combinations of arguments in the context of previous SBI calls. The need for user-level attenuation of high-powered caps seems inevitable.

True, but it becomes less and less likely to be needed.

* We don't have a verified initialiser. If we can verify an initialiser in a way that ties into the security theorems, then we can do the same for user-level attenuation. And I am increasingly confident that we will do both. (Just not in the very near future.)

According to @lsf37 we do have a verified initialiser, but ignoring that:

As far as I understood that one works based on the same security theorems the kernel has. If the kernel only supports e.g. FIDs, adding more fine grained support to the initialiser seems difficult.

But the bigger issue is that the proof would need to apply not only to the initialiser, but also to the runtime user space component that does the actual attenuation, which is unrealistic. No one is going to spend extra time and work because SBI calls are per definition unverifiable as they execute with higher privileges and potentially full access to all memory, and you'll have no guarantee the SBI call does what it should anyway. It would be a pointless exercise.

Best we can do is limit as much as possible now in a way that is the least amount of verification work.

[lsf37]

The TSC has approved variant 5 in the meeting from 3 Dec 2026.