Robbie VanVossen ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3Ab7eb56... ) *updated* an issue RFCs ( https://sel4.atlassian.net/browse/RFC?atlOrigin=eyJpIjoiMjdiNDNlZTMwNDdlNDQz... ) / RFC ( https://sel4.atlassian.net/browse/RFC-9?atlOrigin=eyJpIjoiMjdiNDNlZTMwNDdlND... ) RFC-9 ( https://sel4.atlassian.net/browse/RFC-9?atlOrigin=eyJpIjoiMjdiNDNlZTMwNDdlND... ) Add new capability for seL4 SMC Forwarding ( https://sel4.atlassian.net/browse/RFC-9?atlOrigin=eyJpIjoiMjdiNDNlZTMwNDdlND... ) Change By: Robbie VanVossen ( https://sel4.atlassian.net/secure/ViewProfile.jspa?accountId=557058%3Ab7eb56... ) h1. Summary This RFC proposes to add a new , badged capability which certain threads can invoke so seL4 can make SMC calls on ARM platforms in EL2 (virtualized mode) on the thread’s behalf. h1. Motivation Currently, seL4 running in EL2 traps all SMC calls. Then , if setup, seL4 decides what calls a handler to do deal with these calls the call. Some SMC calls are emulated, such as PSCI for the camkes-vm , but most are just ignored. However, there may be some SMC calls that actually need to make it to the Supervisor, and this configuration does not allow that to happen. This RFC proposes a solution to this problem by giving threads creating a new badged , badged capability which can be given to specific threads to allows them to forward configured SMC calls to seL4 so that the microkernel will make the actual SMC call on the thread's behalf. h1. 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, which it does for all SMC calls made at EL1. 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_Call()}}. h2. New concepts h3. seL4_ARM_SMC_Call() {{seL4_ARM_SMC_Call()}} 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_Call()}} 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. h3. 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_Call()}}, otherwise it will be denied. We expect that in most use cases, it will be given to each VMM thread. The capability is badged and the badge represents the SMC Function Identifier. Therefore, the specific SMC calls that each Thread can make is configurable and checked by seL4. h2. For users We plan to implement this configuration as an example configuration of camkes-vm for the zynqmp platform. Due to WCET implication of this approach, it will not be the default for all platforms. It should only be enabled when actually needed for a specific platform or application. Without this change, Linux is unable to run as a guest on camkes-vm for the zynqmp platform. Here is an example for how to enable SMC calls for some VMs in the {{devices.camkes}} file implemented for a platform in {{camkes-vm-apps}} {code:none}vm0.allow_smc = true; vm0.allowed_smc_functions = [ 0xC2000001, // PM_GET_API_VERSION 0xC2000017  // PM_FPGA_GET_STATUS ]; vm1.allow_smc = true; vm1.allowed_smc_functions = [ 0xC2000001, // PM_GET_API_VERSION 0xC200000D, // PM_REQUEST_NODE 0xC200000E  // PM_RELEASE_NODE ]; vm2.allow_smc = false; vm2.allow_smc_functions = [];{code} As you can see in this example, you can configure each VM to allow or not allow any disallow SMC calls. For each VM that has SMC calls enabled, you then specify which  SMC function calls they can make. These are integers that are defined per platform. As you can see, VMs can share the same calls functions and they can have different calls functions as well. h1. Reference-level explanation This implementation will meet the SMC Calling Convention specification from ARM ([ARM DEN 0028E v1.4|https://developer.arm.com/documentation/den0028/latest?_ga=2.116565828.39037...]) for 32-bit SMC calls. 64-bit SMC calls are partially supported, but full support could be added later. h2. seL4_ARM_SMC_Call() {code:c}static int seL4_ARM_SMC_Call   (  seL4_ARM_SMC   _service, seL4_ARM_SMCContext *   smc_args, seL4_ARM_SMCContext *   smc_response ){code} {noformat}Parameters [in] _service Capability to allow threads to interact with SMC calls. [in] smc_args The structure that has the provided arguments. [out] smc_response The structure to capture the responses. Returns{noformat} h2. struct seL4_ARM_SMCContext {code:c}typedef struct seL4_ARM_SMCContext_ { /* register arguments */ seL4_Word x0, x1, x2, x3, x4, x5, x6, x7; } seL4_ARM_SMCContext;{code} h1. Drawbacks There are a couple of drawbacks to allowing SMC calls to actually go through. Both relate to allowing a supervisor to do anything in the system past initialization time. One drawback is that the worst case execution time (WCET) is no longer guaranteed for the system. Each SMC call can take an arbitrarily long amount of time. This means a thread can essentially lock up all of the cores for an  unspecified amount of time. The core the SMC call is made on is obviously blocked because the supervisor will not return to seL4 until it completes its function. The other cores will become locked as soon as seL4 runs and tries to grab the Big Kernel Lock (BKL).  One potential fix for the multicore issue is to release the BKL before making the SMC call. However, that is out of the scope of this RFC as it has a lot of implications. The current approach will be to have this config option off by default and add documentation about how enabling it affects WCET. Another drawback is the effect this has on assurance. Since the Supervisor is a higher privilege level than seL4, it can make changes to the system of which seL4 is unaware. This would likely add on to the assumptions made if the proof ever included this configuration setting. The proofs would have to assume that the SMC calls that are made will not invalidate the proof. This is on the User to look at what each allowed SMC call does and check that it won’t interfere with the proof. h1. 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. h2. 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. h2. 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). h1. 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|#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. h1. Unresolved questions # How do we address the WCET issue? (Doesn’t need to be solved by this RFC because we are documenting the effects) ( https://sel4.atlassian.net/browse/RFC-9#add-comment?atlOrigin=eyJpIjoiMjdiND... ) Add Comment ( https://sel4.atlassian.net/browse/RFC-9#add-comment?atlOrigin=eyJpIjoiMjdiND... ) Get Jira notifications on your phone! Download the Jira Cloud app for Android ( https://play.google.com/store/apps/details?id=com.atlassian.android.jira.core&referrer=utm_source%3DNotificationLink%26utm_medium%3DEmail ) or iOS ( https://itunes.apple.com/app/apple-store/id1006972087?pt=696495&ct=EmailNotificationLink&mt=8 ) This message was sent by Atlassian Jira (v1001.0.0-SNAPSHOT#100211- sha1:6a2b617 )