RFC-15: Support CHERI/Morello in seL4

[lsf37]

Original Jira issue and discussion.

[heshamelmatary]

Moving the higher-level discussion here, we agreed at the seL4 summit that I submit a hybrid kernel then re-iterate.
The current discussions on the hybrid kernel PR, as discussed is summarised as follows:

1. We concluded that we globally, by default, forbid passing tagged pointers inter-AS.
2. I suggested we also give the user a config option (and PTE bits) to control passing tagged pointers in the IPC buffer for different threat models, given that they know what they're doing, at their own risk.
3. Even if the user allows 2, it still has the option to have strict CHERI security and avoid pointer aliasing by having non-overlapping address spaces for mutually distrusting (and untrustworthy compartments).

I am copying the main questions from the PR here to discuss:

1. Any CHERI design blockers that must be addressed before this RFC/PR gets accepted.
2. Whether the verification-visible changes in non-CHERI shared code are minimal enough to be tolerated.
3. Future optional CHERI design trade-offs that aren't blockers for this PR to get merged, but important to think about.
4. anything else?

[lsf37]

I would like to raise an additional higher-level issue that so far has not been clear to me from the RFC description and only clarified from the description in the PR seL4/seL4#1344:

The proposal seems to be to only support userspace in CHERI C (purecap) mode.

It is unclear to me what the value would be of running seL4 in such a setting. I can see value in seL4 isolating traditional non-CHERI user-space processes (written in any programming language) from purecap user-space processes that want more fine-grained security. But if everything in user space is purecap anyway, you don't really need seL4, you don't even need a kernel, you could just run a threading library and have very similar properties. Conversely, requiring everything in userspace to be purecap, is a massive restriction on what languages, libraries and applications can be run on top of seL4. Certainly not something I think the TSC should endorse for seL4.

It makes sense to explore the purecap-only option as a research project, because that is likely the harder part to implement, but for an RFC to change seL4, supporting only purecap user space is non-starter for me. A proposal to change seL4 must support both to be useful.

Happy to be convinced otherwise if there are good arguments in the other direction.

[heshamelmatary]

Hi Gerwin,

Thanks for raising that. We totally agree with you that supporting "legacy" (e.g., unmodified non-CHERI source-code and/or binaries) makes sense to run side-by-side with purecap CHERI tasks. However, we don't think supporting "hybrid" as in allowing users to manually annotate pointers, adds much value. We're happy to include "legacy" support to the RFC and investigate the implementation efforts this may require as well. Is that what you're looking for or do you mean something else?

The whole reason to run this project is to allow system builders to have access to both a formally verified separation for tasks/VMs and also strong memory safety in tasks and guest VMs. i.e., we very much see seL4 as complementary technologies. This is one of the reasons that we also see legacy task support as essential, since you might well want (for example) a configuration in which you have formally verified isolation between a legacy 64-bit Arm VM and a hardened CHERI-enabled task or VM.

[heshamelmatary]

I am trying to modify the RFC file to integrate adding support for legacy code. However, since this is just a PR, I can't fork and submit PRs to modify this file. What's the recommended way if I want to modify the RFC proposal?