Summary This RFC proposes to add a new capability which certain threads can invoke so seL4 can make SMC calls on ARM platforms in EL2 (virtualized mode) on the thread’s behalf. Motivation There are currently two ways to handle SMC calls when using seL4 as a hypervisor on ARM.
- You can configure the system so that any thread running at EL1/0 can directly make SMC calls. (Configure by enabling KernelAllowSMCCalls for the microkernel)
- You can configure the system so that SMC calls are trapped into seL4. This allows seL4 to decide what to do with the calls. In the current implementation
Both approaches leave something to be desired. The first option has various security implications and is essentially unprovable as it would allow any thread to make secure calls that could put the system in a bad state. The second option is more secure and allows you to emulate some SMC calls, such as PSCI, however, there may be some SMC calls that do need to be made on behalf of a thread, and this configuration does not allow that to happen. We want to essentially combine the two approaches by configuring the system for the second approach, and then allowing threads that have a new capability to forward SMC calls so that seL4 will make the actual SMC call on the thread's behalf. Guide-level explanation This change will allow you to forward to the microkernel, emulate, or block SMC calls based on platform specific configuration. When an SMC call is made by a VM, the microkernel intercepts the call. It then calls handle_smc() for the corresponding VMM thread. That function will decode the specific SMC call and decide whether to block it, emulate it, or forward the call back into seL4. There are examples already for multiple platforms on emulation and blocking. The zynqmp platform will have an example of forwarding the SMC with the new API call, seL4_ARM_SMC_Forward(). New concepts seL4_ARM_SMC_Forward() seL4_ARM_SMC_Forward() is the new ObjectInvocation API call and can be called in two ways:
- A VM attempts to make an SMC call which traps into the microkernel. The microkernel informs the VMM’s handler and the VMM decides that the SMC call really needs to be made. The VMM then calls seL4_ARM_SMC_Forward() with the SMC capability and all the arguments that the VM provided.
- Directly by constructing the SMC call from the thread with the SMC capability. This means that a trap isn’t needed.
Our expected use case has been using the first approach in the camkes-vm for VMM handlers on the behalf of its VM. I am not sure if there is a use case for the second approach, but it is certainly possible. In either case, the function still requires the caller to set all 8 registers, even if the specific SMC call uses less arguments. seL4_ARM_SMC seL4_ARM_SMC is the new capability. It needs to be given to any threads that you expect to call seL4_ARM_SMC_Forward(), otherwise it will be denied. In most use cases, it will be given to each VMM thread. For users We plan to implement this configuration as the default for users of camkes-vm for ARM platforms. However, it should be quite seamless. We will implement a default configuration for each platform that denies forwarding on any SMC calls so that functionality will remain the same. The exception will be for the zynqmp platform, which up until now has not been a supported platform for the camkes-vm. This was actually due to the fact that this platform required KernelAllowSMCCalls to be enabled to get Linux working as a VM. This change will fix that issue so that zynqmp will be a valid platform. This platform will have a different default, which allows specific SMC calls to be forwarded on so that Linux guests will boot correctly. If a user needs to update the configuration for their platform, they can make changes to projects/seL4_projects_libs/libsel4vmmplatsupport/src/plat/$KernelPlatform/devices/smc.c. Reference-level explanation This implementation will meet the SMC Calling Convention specification from ARM (ARM DEN 0028E v1.4) for 32-bit SMC calls. 64-bit SMC calls are partially supported, but full support could be added later. seL4_ARM_SMC_Forward()
static int seL4_ARM_SMC_Forward ( seL4_ARM_SMC _service,
seL4_ARM_SMCContext * smc_args,
seL4_ARM_SMCContext * smc_response
)
struct seL4_ARM_SMCContext
typedef struct seL4_ARM_SMCContext_ {
seL4_Word x0, x1, x2, x3, x4, x5, x6, x7;
} seL4_ARM_SMCContext;
Drawbacks The main drawback of this approach is that you are allowing the user to make the decision on which SMC calls should go through or not. This will require a fairly advanced configuration and allows the user to open themselves up to system-level vulnerabilities. However, I think the need for the feature outweighs the risk. Also, to help mitigate the risk in the camkes-vm, I think we can setup a default configuration that allows as few SMC calls as possible for most platforms. We have done some testing with Linux on the zynqmp platform and have identified the minimum SMC calls we need the VMM's to support just to boot the VMs. So that platform configuration will be more permissive but will meet the needs of a Linux guest VM. One other way to mitigate this issue is identifying some SMC calls that should never be made by a thread. Then create a platform-dependent blacklist in the microkernel that would disallow certain SMC calls even from threads that have the SMC capability. Rationale and alternatives
This design is the best because it gives users flexibility by allowing them to make some SMC calls while still being able to emulate other SMC calls. It is the preferred method, because the microkernel shouldn't need to be updated with each new platform, VMM configuration, and secure application implementation. It can all be configured in user space.
Alternative approaches SMC filtering could be done in the microkernel so that developers are less likely to configure the system incorrectly. However, there are some cases where the filtering is dependent on specific threads and the application level (Secure world communication) instead of just platform dependent. On the first point, instead of creating a cap for making the SMC call, you could have a cap for each numbered SMC call so that you could configure what SMC call each thread can make using the root thread. However, that is quite a bit of work as that will differ for each ARM platform and adds another step when porting the microkernel to new ARM platforms. That could also solve the second point, but then users would likely need to modify the microkernel to support their specific secure world application, which is something that should really be avoided. Another part of the implementation that could be done differently is using the VCPU capability with an access right instead of creating a new type of capability. The kinds of access rights are already determined as read, write, grant, and grantreply. A write access right would probably make the most sense, but it still seems obtuse that a write access on a VCPU capability would allow the invoker to make an SMC call. Besides that, there are two other issues I see with this approach:
- I can foresee a use-case where you have a health monitor component that isn’t associated with a VCPU but needs to be able to forward an SMC call to actually interact with EL3 or secure applications.
- If the VCPU capability ever needs read/write access rights that make more sense with the type of object it is, for example, limiting which threads can actually read or write that VCPUs registers.
For those reasons we believe a new capability makes the most sense. Impact of not implementing this Not implementing this will limit the ARM platforms we can use for the camkes-vm and/or the guests that can run on those platforms. It will also limit support for applications that run in secure side of the trustzone that need to communicate with the nonsecure side (Where sel4, VMMs, and the VMs run). Prior art Xen has a similar implementation for the Zynqmp where arbitration is done to allow/disallow/emulate SMC calls from guest VMs. The arbitration is quite specific and is automatically generated based on resource allocation for each VM. Xen does not have VMM pieces that run in Userspace. Basically all of the management runs in EL2. Therefore, all of the arbitration is done in Xen itself. This approach does not make sense for seL4 for the reasons stated above in the rationale section. However, this does show a need for this feature in hypervisors on ARMv8 platforms. If necessary, we could reference the Xen arbitration code to help improve the default arbitration for the zynqmp in our implementation. Unresolved questions
- Should this implementation be configurable?
- I would argue it makes the most sense to have it automatically enabled if you are using the VMM on ARM and KernelAllowSMCCalls is disabled. Then your default whitelist in the SMC handler, for most platforms, can be to allow no SMC calls through, which would mean the default configuration would essentially be the same as the second configuration that is defined in the motivation section. However, I am wondering if there is a case where you still just want to disable it completely?
- Should the microkernel have an overriding blacklist?
- How and who decides what the blacklist is?
- Is it configurable?
- I don't think this question blocks the RFC as the blacklist could be implemented easily enough after the proposed implementation.
|
