Summary:
There are system registers that are useful to be able to access from user level. Two examples are system registers related to the Arm Generic Timer and registers related to the Performance Monitor Unit. There are already kernel configuration options that enable user access to these registers, however these configurations are all or nothing and aren’t allowed under verified kernel configurations. Instead, a better approach would be to add support for enabling/disabling access to these registers on a per-TCB and per-register basis that would allow the kernel to enable/disable access as part of a regular context switch. Authority to access these registers would need to be held by some hardware control capability.
Motivation:
Certain hardware features are unavailable to user level without explicit user access being enabled by the kernel. The generic timer provides access to 64 bit timestamp counters and per-core timer compare registers that can generate timeout interrupts. User level access allows application software to use these hardware features without interfering with any access requirements the kernel has. An implementation that allows user level access to be restricted to certain TCBs would allow systems to be built where efficient timer drivers can be implemented using the core-local timers and counters.
The performance monitor unit provides a 64bit cycle counter and 32-bit event counters that provide detailed information the performance of executing software. User access allows application software to monitor its own performance with fine-grained control. Being able to restrict access to these registers to specifically authorized TCBs would allow trusted components to use performance monitor counters to monitor system behavior without also allowing access to untrusted components.
Currently, although the kernel supports enabling access to these registers at user level, this cannot be done in a verified configuration as there’s no access-control associated with the registers. Adding the necessary access control would hopefully allow these hardware mechanisms to be used in verified configurations which would allow them to be used in actual production applications.
Guide-level Explanation:
There is currently the following kernel compile-time config options:
- KernelArmExportPCNTUser: Allow user access to the register containing the Generic Timer physical counter value.
- KernelArmExportVCNTUser: Allow user access to the register containing the Generic Timer virtual counter value.
- KernelArmExportPTMRUser: Allow user access to the Generic Timer physical timer control and compare registers that control generation of physical timer interrupts.
- KernelArmExportVTMRUser: Allow user access to the Generic Timer virtual timer control and compare registers that control generation of virtual timer interrupts.
- KernelArmExportPMUUser: Allow user access to the PMU registers which control the performance monitor unit and read and write performance counter values.
When enabled, access to the above registers is currently allowed for any thread at user level. This creates communication channels and there’s no way to prevent unauthorized TCBs from tampering with intended register values.
Instead of these register accesses being all or nothing, we would create a new capability type, a hardware control capability, which authorizes its holder to configure TCBs to enable or disable access to these registers. If a TCB has been configured to have access to these registers then the kernel enables user level access when context switching to that TCB. When a TCB doesn’t have access to a register, user access is disabled when switching to that TCB.
As the kernel uses one of the timers in the Generic Timer, user level access to the same timer registers that the kernel uses would never be allowed.
Delegation of authority to enable or disable these system registers would be supported by deriving copies of the hardware control cap. As part of a capability derivation, the scope of authority could be reduced. This means it would be possible to give a “process” the authority to enable time stamp counter access to all threads it creates but restricting it from being able to also give those threads access to the PMU registers.
Revoking access to these hardware capabilities would result in the TCBs losing any access to the system registers that was enabled by the now-revoked capability.
There would be no additional storage added to a TCB object for saving or restoring state during a context switch that is related to these system registers. While there could be some value in being able to save and restore PMU counter state during a context switch, this is out of scope of this proposal.
On hypervisor configurations, the Generic Timer timer registers are already context switched when switching VCPUs. To keep this proposal simpler, these registers would not be available for TCB control as they are already managed by the VCPU object type.
The initial copy of the new hardware control capability would be provided to the root task in the initial CNode and described in the seL4_Bootinfo_t struct.
This mechanism is fairly generic, can be copied over to other architectures and can easily extended to other types of CPU enforced user level access control of hardware mechanisms. (E.G. cache maintenance instructions)
Reference-level explanation:
This section can be added if this gets as afar as an implementation
Drawbacks:
This would increase the amount of work the kernel would need to do during a context switch due to the added TCB lookup for system register access plus the modification of the control registers for changing the access control. It is expected that this additional work is << 5% of a context switch cost and can also be done inside the fastpath. This would need to be checked once there is an implementation.
Rationale and alternatives:
The main alternative is to do nothing. This would mean that the hardware features would continue to be unusable from user level in verified configurations. The mechanisms could still be used in unverified configurations, but this would prevent any production applications that could claim to use a verified configuration.
Prior art:
Linux gettimeofday() uses a user level implementation provided by the vdso that leverages the Generic Timer hardware mechanisms on supported platforms to access the time counters without requiring entering the kernel.
Unresolved questions:
Would this have any significant impacts on the security proofs?