Experimental prototype of CHERI-enabled seL4 is released
Hello, The CHERI Alliance has released a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This release includes CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment. The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, CHERI-Toooba, and CHERI-CVA6 on FPGA. For those who are unfamiliar with CHERI, CHERI support in seL4 enables memory-safe C/C++ user-level projects and applications without having to (re)write code in languages like Rust. This complement's seL4's strong isolation between different components, enforced by the MMU and seL4's software capabilities. We welcome any feedback. Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/ Regards, Hesham
Hi Hesham, 2 questions: do you run a modified seL4? is there any real world example of a Rust app running on top of you solution? Best, On Tuesday, July 29, 2025, Hesham Almatary via Devel <devel@sel4.systems> wrote:
Hello,
The CHERI Alliance has released a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This release includes CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment.
The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, CHERI-Toooba, and CHERI-CVA6 on FPGA.
For those who are unfamiliar with CHERI, CHERI support in seL4 enables memory-safe C/C++ user-level projects and applications without having to (re)write code in languages like Rust. This complement's seL4's strong isolation between different components, enforced by the MMU and seL4's software capabilities.
We welcome any feedback.
Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/
Regards, Hesham _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hello Hugo, On Tue, 29 Jul 2025 at 18:26, Hugo V.C. <skydivebcn@gmail.com> wrote:
Hi Hesham,
2 questions:
do you run a modified seL4?
Yes definitely, as mentioned in the blog post. The link to the fork [1] is in the blog post and we’ve submitted a PR [2] upstream for it (also in the blog post).
[1] https://github.com/CHERI-Alliance/CHERI-seL4 [2] https://github.com/seL4/seL4/pull/1469
is there any real world example of a Rust app running on top of you solution?
I’ve built and run Microkit’s Rust hello example on top without any issues. You can also reproduce that if you’d like. Happy to give further instructions if needed. Regards, Hesham
Best,
On Tuesday, July 29, 2025, Hesham Almatary via Devel <devel@sel4.systems> wrote:
Hello,
The CHERI Alliance has released a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This release includes CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment.
The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, CHERI-Toooba, and CHERI-CVA6 on FPGA.
For those who are unfamiliar with CHERI, CHERI support in seL4 enables memory-safe C/C++ user-level projects and applications without having to (re)write code in languages like Rust. This complement's seL4's strong isolation between different components, enforced by the MMU and seL4's software capabilities.
We welcome any feedback.
Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/
Regards, Hesham _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
I read the pull discussion here: https://github.com/seL4/seL4/pull/1469 you say: "This port has been tested with Microkit on Codasip's QEMU and hardware platforms (x730)" is Codasip's QEMU a custom QEMU to support x730? also, this question is for seL4 Foundation: are there plans to formal verify seL4 with this changes? I thing you guys have put together two different Worlds that open a powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains". And as we already have LionsOS, so we get a third option (old CamkES. LionOS/Microkit, Cheri-seL4). It is not competition, it is evolution just following different valid paths. ANY of those paths is 1000 times better than current OSs/solutions. I love to have different options, all around seL4. I wish you guys collaborate to expand seL4 ecosystem. Best, On Tuesday, July 29, 2025, Hesham Almatary < heshamalmatary@capabilitieslimited.co.uk> wrote:
Hello Hugo, On Tue, 29 Jul 2025 at 18:26, Hugo V.C. <skydivebcn@gmail.com> wrote:
Hi Hesham,
2 questions:
do you run a modified seL4?
Yes definitely, as mentioned in the blog post. The link to the fork [1] is in the blog post and we’ve submitted a PR [2] upstream for it (also in the blog post). [1] https://github.com/CHERI-Alliance/CHERI-seL4 [2] https://github.com/seL4/seL4/pull/1469
is there any real world example of a Rust app running on top of you
solution?
I’ve built and run Microkit’s Rust hello example on top without any issues. You can also reproduce that if you’d like. Happy to give further instructions if needed. Regards, Hesham
Best,
On Tuesday, July 29, 2025, Hesham Almatary via Devel <devel@sel4.systems>
wrote:
Hello,
The CHERI Alliance has released a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This release includes CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment.
The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, CHERI-Toooba, and CHERI-CVA6 on FPGA.
For those who are unfamiliar with CHERI, CHERI support in seL4 enables memory-safe C/C++ user-level projects and applications without having to (re)write code in languages like Rust. This complement's seL4's strong isolation between different components, enforced by the MMU and seL4's software capabilities.
We welcome any feedback.
Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/
Regards, Hesham _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hi Hugo, On Wed, 30 Jul 2025 at 10:07, Hugo V.C. <skydivebcn@gmail.com> wrote:
I read the pull discussion here:
https://github.com/seL4/seL4/pull/1469
you say:
"This port has been tested with Microkit on Codasip's QEMU and hardware platforms (x730)"
is Codasip's QEMU a custom QEMU to support x730?
Yes, it's a QEMU fork that adds a machine (currently called hobgoblin, but will be Codasip Prime in the next release) with CHERI support that's almost exactly the same as X730 hardware; code that runs on it also runs out of the box on X730. You can find it here https://github.com/CHERI-Alliance/qemu/tree/codasip-cheri-riscv_v3
also, this question is for seL4 Foundation: are there plans to formal verify seL4 with this changes?
I thing you guys have put together two different Worlds that open a powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains".
Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So your options are to 1) (re)write everything in Rust (which also requires a relatively rare intellectual capability), or 2) use something like CHERI which is arguably just "good practice, clean C/C++ code" from an application developer perspective.
And as we already have LionsOS, so we get a third option (old CamkES. LionOS/Microkit, Cheri-seL4). It is not competition, it is evolution just following different valid paths. ANY of those paths is 1000 times better than current OSs/solutions. I love to have different options, all around seL4.
LionsOS/Microkit, CAmkES, or pretty much any C/C++ userspace framework (e.g., sel4test, sel4bench, Kry10 OS, etc) could be ported and run on CHERI-seL4 (the CHERI-enabled microkernel itself). We hope there will be opportunities in the future (especially once we have commercial CHERI processors people can buy) to formally verify the CHERI extensions in the kernel (e.g., the PR we submitted), and we're happy to collaborate on that.
I wish you guys collaborate to expand seL4 ecosystem.
Best,
On Tuesday, July 29, 2025, Hesham Almatary <heshamalmatary@capabilitieslimited.co.uk> wrote:
Hello Hugo, On Tue, 29 Jul 2025 at 18:26, Hugo V.C. <skydivebcn@gmail.com> wrote:
Hi Hesham,
2 questions:
do you run a modified seL4?
Yes definitely, as mentioned in the blog post. The link to the fork [1] is in the blog post and we’ve submitted a PR [2] upstream for it (also in the blog post). [1] https://github.com/CHERI-Alliance/CHERI-seL4 [2] https://github.com/seL4/seL4/pull/1469
is there any real world example of a Rust app running on top of you solution?
I’ve built and run Microkit’s Rust hello example on top without any issues. You can also reproduce that if you’d like. Happy to give further instructions if needed. Regards, Hesham
Best,
On Tuesday, July 29, 2025, Hesham Almatary via Devel <devel@sel4.systems> wrote:
Hello,
The CHERI Alliance has released a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This release includes CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment.
The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, CHERI-Toooba, and CHERI-CVA6 on FPGA.
For those who are unfamiliar with CHERI, CHERI support in seL4 enables memory-safe C/C++ user-level projects and applications without having to (re)write code in languages like Rust. This complement's seL4's strong isolation between different components, enforced by the MMU and seL4's software capabilities.
We welcome any feedback.
Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/
Regards, Hesham _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
On 30 Jul 2025, at 19:39, Hesham Almatary via Devel <devel@sel4.systems> wrote:
also, this question is for seL4 Foundation: are there plans to formal verify seL4 with this changes?
I thing you guys have put together two different Worlds that open a powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains".
Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So
That’s a somewhat courageous statement. For one, just because an OS is “dynamic” doesn't mean it’s “rapidly changing” – high assurance OSes certainly don’t, verification or not. Secondly, there’s a lot of work on making verification more of a repeatable engineering process, there’s at least a whole DARPA program committed to this. At UNSW, we’re working on exactly this (and it surely doesn’t mean re-writing everything in Rust). That doesn’t mean that intra-AS safety isn’t a good thing, but please don’t over-claim. Gernot Confidential communication - This email and any files transmitted with it are confidential and are intended solely for the addressee. If you are not the intended recipient, please be advised that you have received this email in error and that any use, dissemination, forwarding, printing, or copying of this email and any file attachments is strictly prohibited. If you have received this email in error, please notify me immediately by return email and destroy this email.
Hello Gernot, On Wed, 30 Jul 2025 at 12:57, Gernot Heiser via Devel <devel@sel4.systems> wrote:
On 30 Jul 2025, at 19:39, Hesham Almatary via Devel <devel@sel4.systems> wrote:
also, this question is for seL4 Foundation: are there plans to formal verify seL4 with this changes?
I thing you guys have put together two different Worlds that open a powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains".
Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So
That’s a somewhat courageous statement.
For one, just because an OS is “dynamic” doesn't mean it’s “rapidly changing” – high assurance OSes certainly don’t, verification or not.
Understood. By dynamic OS, I didn't necessarily mean high assurance, I mean something like L4Re, Linux or FreeBSD, with many commits, drivers, PRs, changes, features added everyday. Linux and FreeBSD can currently build and run memory-safe on CHERI platforms, and can in the future run on CHERI-seL4 as VMs with hypervisor enabled, when supported.
Secondly, there’s a lot of work on making verification more of a repeatable engineering process, there’s at least a whole DARPA program committed to this. At UNSW, we’re working on exactly this (and it surely doesn’t mean re-writing everything in Rust).
Really looking forward to the outcome of that. Hopefully it'll make the lengthy reviewing and verification process/checks smoother and accessible to system developers with no verification expertise.
That doesn’t mean that intra-AS safety isn’t a good thing, but please don’t over-claim.
It's intra-AS memory-safety to be specific that CHERI mainly offers to existing C/C++ projects (besides software compartmentalisation). As things stand, IMO, I don't think formal verification will be able to keep up with rapidly-changing OSes like Linux or FreeBSD, but I'd be happy to be proven wrong in the future when such tools/solutions exist. Regards, Hesham
Gernot
Confidential communication - This email and any files transmitted with it are confidential and are intended solely for the addressee. If you are not the intended recipient, please be advised that you have received this email in error and that any use, dissemination, forwarding, printing, or copying of this email and any file attachments is strictly prohibited. If you have received this email in error, please notify me immediately by return email and destroy this email.
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hi guys, maybe a stupid question but I wonder if we can have formal verification of CHERI C (purecap) mode programs that run on a CHERI-enabled seL4? I mean, we are all on the same boat and as dinosaur 0day exploit writer that have bypassed almost any OS security protections that exist, I can see here two amazing technologies: formal verification and hardware enforcement. I love both. I know that may look like redundant but... can we have both or am I missing something? Best, El mié, 30 jul 2025 a las 14:04, Gernot Heiser via Devel (<devel@sel4.systems>) escribió:
On 30 Jul 2025, at 19:39, Hesham Almatary via Devel <devel@sel4.systems> wrote:
also, this question is for seL4 Foundation: are there plans to formal
verify seL4 with this changes?
I thing you guys have put together two different Worlds that open a
powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains".
Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So
That’s a somewhat courageous statement.
For one, just because an OS is “dynamic” doesn't mean it’s “rapidly changing” – high assurance OSes certainly don’t, verification or not.
Secondly, there’s a lot of work on making verification more of a repeatable engineering process, there’s at least a whole DARPA program committed to this. At UNSW, we’re working on exactly this (and it surely doesn’t mean re-writing everything in Rust).
That doesn’t mean that intra-AS safety isn’t a good thing, but please don’t over-claim.
Gernot
Confidential communication - This email and any files transmitted with it are confidential and are intended solely for the addressee. If you are not the intended recipient, please be advised that you have received this email in error and that any use, dissemination, forwarding, printing, or copying of this email and any file attachments is strictly prohibited. If you have received this email in error, please notify me immediately by return email and destroy this email.
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hello Hugo, On Thu, 31 Jul 2025 at 09:13, Hugo V.C. via Devel <devel@sel4.systems> wrote:
Hi guys,
maybe a stupid question but I wonder if we can have formal verification of CHERI C (purecap) mode programs that run on a CHERI-enabled seL4?
I was referred to this paper [1, 2] which also has formal verification work of CHERI C. I am not sure how this may (or not), integrate with or relate to the seL4/UNSW/DARPA work to have some formal verification work in userspace, and more specifically the memory safety aspects of it. [1] Zaliva, Vadim, et al. "Formal mechanised semantics of CHERI C: capabilities, undefined behaviour, and provenance." Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1. 2024. [2] https://www.cl.cam.ac.uk/~pes20/asplos24spring-paper110.pdf
I mean, we are all on the same boat and as dinosaur 0day exploit writer that have bypassed almost any OS security protections that exist, I can see here two amazing technologies: formal verification and hardware enforcement. I love both. I know that may look like redundant but... can we have both or am I missing something?
Best,
El mié, 30 jul 2025 a las 14:04, Gernot Heiser via Devel (<devel@sel4.systems>) escribió:
On 30 Jul 2025, at 19:39, Hesham Almatary via Devel <devel@sel4.systems> wrote:
also, this question is for seL4 Foundation: are there plans to formal
verify seL4 with this changes?
I thing you guys have put together two different Worlds that open a
powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains".
Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So
That’s a somewhat courageous statement.
For one, just because an OS is “dynamic” doesn't mean it’s “rapidly changing” – high assurance OSes certainly don’t, verification or not.
Secondly, there’s a lot of work on making verification more of a repeatable engineering process, there’s at least a whole DARPA program committed to this. At UNSW, we’re working on exactly this (and it surely doesn’t mean re-writing everything in Rust).
That doesn’t mean that intra-AS safety isn’t a good thing, but please don’t over-claim.
Gernot
Confidential communication - This email and any files transmitted with it are confidential and are intended solely for the addressee. If you are not the intended recipient, please be advised that you have received this email in error and that any use, dissemination, forwarding, printing, or copying of this email and any file attachments is strictly prohibited. If you have received this email in error, please notify me immediately by return email and destroy this email.
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Ok, maybe I was not clear... what I wanted to know is if CHERI C (purecap) programs can be formally verified. Just this. Not CHERI platform itself... I know it may look overkilling, but I like CHERI architecture, and it requires programs to be be in CHERI C (purecap) so my quesrion is: can those programs/code be formally verified? This is not a random question. I ask this because in real World we can have some "monster" C program that can be on a first stage ported to CHERI C. This will give a huge improvement in memory safety. Then a next stages we can formally verify sub modules of this program. So no need to wait for the full monster to be formally verified (actually this can even never happen) and we can gradually formally verify blocks/modules. But for this to happen we need to know if CHERI C (purecap) codw can be formally verified. On Tuesday, August 12, 2025, Hesham Almatary < heshamalmatary@capabilitieslimited.co.uk> wrote:
Hello Hugo,
On Thu, 31 Jul 2025 at 09:13, Hugo V.C. via Devel <devel@sel4.systems> wrote:
Hi guys,
maybe a stupid question but I wonder if we can have formal verification
of
CHERI C (purecap) mode programs that run on a CHERI-enabled seL4?
I was referred to this paper [1, 2] which also has formal verification work of CHERI C. I am not sure how this may (or not), integrate with or relate to the seL4/UNSW/DARPA work to have some formal verification work in userspace, and more specifically the memory safety aspects of it.
[1] Zaliva, Vadim, et al. "Formal mechanised semantics of CHERI C: capabilities, undefined behaviour, and provenance." Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1. 2024. [2] https://www.cl.cam.ac.uk/~pes20/asplos24spring-paper110.pdf
I mean, we are all on the same boat and as dinosaur 0day exploit writer that have bypassed almost any OS security protections that exist, I can see here two amazing technologies: formal verification and hardware enforcement. I love both. I know that may look like redundant but... can we have both or am I missing something?
Best,
El mié, 30 jul 2025 a las 14:04, Gernot Heiser via Devel (<devel@sel4.systems>) escribió:
On 30 Jul 2025, at 19:39, Hesham Almatary via Devel <devel@sel4.systems
wrote:
also, this question is for seL4 Foundation: are there plans to
formal verify seL4 with this changes?
I thing you guys have put together two different Worlds that open a
powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains".
Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So
That’s a somewhat courageous statement.
For one, just because an OS is “dynamic” doesn't mean it’s “rapidly changing” – high assurance OSes certainly don’t, verification or not.
Secondly, there’s a lot of work on making verification more of a repeatable engineering process, there’s at least a whole DARPA program committed to this. At UNSW, we’re working on exactly this (and it surely doesn’t mean re-writing everything in Rust).
That doesn’t mean that intra-AS safety isn’t a good thing, but please don’t over-claim.
Gernot
Confidential communication - This email and any files transmitted with it are confidential and are intended solely for the addressee. If you are not the intended recipient, please be advised that you have received this email in error and that any use, dissemination, forwarding, printing, or copying of this email and any file attachments is strictly prohibited. If you have received this email in error, please notify me immediately by return email and destroy this email.
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Looking this: https://github.com/CHERI-Alliance/qemu/tree/codasip-cheri-riscv_v3 I realize your patched Qemu is based on version 6.2, which is very old (2021). Do you have the patches so we try to apply them to a recent version of Qemu like 9.X or 10.X? Best, El mié, 30 jul 2025 a las 11:39, Hesham Almatary (< heshamalmatary@capabilitieslimited.co.uk>) escribió:
Hi Hugo,
On Wed, 30 Jul 2025 at 10:07, Hugo V.C. <skydivebcn@gmail.com> wrote:
I read the pull discussion here:
https://github.com/seL4/seL4/pull/1469
you say:
"This port has been tested with Microkit on Codasip's QEMU and hardware
platforms (x730)"
is Codasip's QEMU a custom QEMU to support x730?
Yes, it's a QEMU fork that adds a machine (currently called hobgoblin, but will be Codasip Prime in the next release) with CHERI support that's almost exactly the same as X730 hardware; code that runs on it also runs out of the box on X730. You can find it here https://github.com/CHERI-Alliance/qemu/tree/codasip-cheri-riscv_v3
also, this question is for seL4 Foundation: are there plans to formal verify seL4 with this changes?
I thing you guys have put together two different Worlds that open a powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains".
Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So your options are to 1) (re)write everything in Rust (which also requires a relatively rare intellectual capability), or 2) use something like CHERI which is arguably just "good practice, clean C/C++ code" from an application developer perspective.
And as we already have LionsOS, so we get a third option (old CamkES. LionOS/Microkit, Cheri-seL4). It is not competition, it is evolution just following different valid paths. ANY of those paths is 1000 times better than current OSs/solutions. I love to have different options, all around seL4.
LionsOS/Microkit, CAmkES, or pretty much any C/C++ userspace framework (e.g., sel4test, sel4bench, Kry10 OS, etc) could be ported and run on CHERI-seL4 (the CHERI-enabled microkernel itself). We hope there will be opportunities in the future (especially once we have commercial CHERI processors people can buy) to formally verify the CHERI extensions in the kernel (e.g., the PR we submitted), and we're happy to collaborate on that.
I wish you guys collaborate to expand seL4 ecosystem.
Best,
On Tuesday, July 29, 2025, Hesham Almatary < heshamalmatary@capabilitieslimited.co.uk> wrote:
Hello Hugo, On Tue, 29 Jul 2025 at 18:26, Hugo V.C. <skydivebcn@gmail.com> wrote:
Hi Hesham,
2 questions:
do you run a modified seL4?
Yes definitely, as mentioned in the blog post. The link to the fork [1] is in the blog post and we’ve submitted a PR [2] upstream for it (also in the blog post). [1] https://github.com/CHERI-Alliance/CHERI-seL4 [2] https://github.com/seL4/seL4/pull/1469
is there any real world example of a Rust app running on top of you
solution?
I’ve built and run Microkit’s Rust hello example on top without any issues. You can also reproduce that if you’d like. Happy to give further instructions if needed. Regards, Hesham
Best,
On Tuesday, July 29, 2025, Hesham Almatary via Devel
<devel@sel4.systems> wrote:
Hello,
The CHERI Alliance has released a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This release includes CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment.
The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, CHERI-Toooba, and CHERI-CVA6 on FPGA.
For those who are unfamiliar with CHERI, CHERI support in seL4 enables memory-safe C/C++ user-level projects and applications without having to (re)write code in languages like Rust. This complement's seL4's strong isolation between different components, enforced by the MMU and seL4's software capabilities.
We welcome any feedback.
Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/
Regards, Hesham _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hello Hugo, On Thu, 31 Jul 2025 at 08:32, Hugo V.C. <skydivebcn@gmail.com> wrote:
Looking this:
https://github.com/CHERI-Alliance/qemu/tree/codasip-cheri-riscv_v3
I realize your patched Qemu is based on version 6.2, which is very old (2021). Do you have the patches so we try to apply them to a recent version of Qemu like 9.X or 10.X?
Unfortunately there is no set of patches to apply to recent QEMU versions, rebasing/merging to a recent version is a lot of work and is on the TODO list though, but it's not a priority at the moment. Regards, Hesham
Best,
El mié, 30 jul 2025 a las 11:39, Hesham Almatary (<heshamalmatary@capabilitieslimited.co.uk>) escribió:
Hi Hugo,
On Wed, 30 Jul 2025 at 10:07, Hugo V.C. <skydivebcn@gmail.com> wrote:
I read the pull discussion here:
https://github.com/seL4/seL4/pull/1469
you say:
"This port has been tested with Microkit on Codasip's QEMU and hardware platforms (x730)"
is Codasip's QEMU a custom QEMU to support x730?
Yes, it's a QEMU fork that adds a machine (currently called hobgoblin, but will be Codasip Prime in the next release) with CHERI support that's almost exactly the same as X730 hardware; code that runs on it also runs out of the box on X730. You can find it here https://github.com/CHERI-Alliance/qemu/tree/codasip-cheri-riscv_v3
also, this question is for seL4 Foundation: are there plans to formal verify seL4 with this changes?
I thing you guys have put together two different Worlds that open a powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains".
Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So your options are to 1) (re)write everything in Rust (which also requires a relatively rare intellectual capability), or 2) use something like CHERI which is arguably just "good practice, clean C/C++ code" from an application developer perspective.
And as we already have LionsOS, so we get a third option (old CamkES. LionOS/Microkit, Cheri-seL4). It is not competition, it is evolution just following different valid paths. ANY of those paths is 1000 times better than current OSs/solutions. I love to have different options, all around seL4.
LionsOS/Microkit, CAmkES, or pretty much any C/C++ userspace framework (e.g., sel4test, sel4bench, Kry10 OS, etc) could be ported and run on CHERI-seL4 (the CHERI-enabled microkernel itself). We hope there will be opportunities in the future (especially once we have commercial CHERI processors people can buy) to formally verify the CHERI extensions in the kernel (e.g., the PR we submitted), and we're happy to collaborate on that.
I wish you guys collaborate to expand seL4 ecosystem.
Best,
On Tuesday, July 29, 2025, Hesham Almatary <heshamalmatary@capabilitieslimited.co.uk> wrote:
Hello Hugo, On Tue, 29 Jul 2025 at 18:26, Hugo V.C. <skydivebcn@gmail.com> wrote:
Hi Hesham,
2 questions:
do you run a modified seL4?
Yes definitely, as mentioned in the blog post. The link to the fork [1] is in the blog post and we’ve submitted a PR [2] upstream for it (also in the blog post). [1] https://github.com/CHERI-Alliance/CHERI-seL4 [2] https://github.com/seL4/seL4/pull/1469
is there any real world example of a Rust app running on top of you solution?
I’ve built and run Microkit’s Rust hello example on top without any issues. You can also reproduce that if you’d like. Happy to give further instructions if needed. Regards, Hesham
Best,
On Tuesday, July 29, 2025, Hesham Almatary via Devel <devel@sel4.systems> wrote:
Hello,
The CHERI Alliance has released a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This release includes CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment.
The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, CHERI-Toooba, and CHERI-CVA6 on FPGA.
For those who are unfamiliar with CHERI, CHERI support in seL4 enables memory-safe C/C++ user-level projects and applications without having to (re)write code in languages like Rust. This complement's seL4's strong isolation between different components, enforced by the MMU and seL4's software capabilities.
We welcome any feedback.
Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/
Regards, Hesham _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Ok, I understand, but think about it. Qemu 9.x intruduces control-flow integrity, IOMMU,... nobody runs 6.2... Maybe a subset of the full patch (just RISC-V not MIPS, just a specific CPU... On Thursday, July 31, 2025, Hesham Almatary < heshamalmatary@capabilitieslimited.co.uk> wrote:
Hello Hugo,
On Thu, 31 Jul 2025 at 08:32, Hugo V.C. <skydivebcn@gmail.com> wrote:
Looking this:
https://github.com/CHERI-Alliance/qemu/tree/codasip-cheri-riscv_v3
I realize your patched Qemu is based on version 6.2, which is very old
(2021). Do you have the patches so we try to apply them to a recent version of Qemu like 9.X or 10.X?
Unfortunately there is no set of patches to apply to recent QEMU versions, rebasing/merging to a recent version is a lot of work and is on the TODO list though, but it's not a priority at the moment.
Regards, Hesham
Best,
El mié, 30 jul 2025 a las 11:39, Hesham Almatary (< heshamalmatary@capabilitieslimited.co.uk>) escribió:
Hi Hugo,
On Wed, 30 Jul 2025 at 10:07, Hugo V.C. <skydivebcn@gmail.com> wrote:
I read the pull discussion here:
https://github.com/seL4/seL4/pull/1469
you say:
"This port has been tested with Microkit on Codasip's QEMU and
hardware platforms (x730)"
is Codasip's QEMU a custom QEMU to support x730?
Yes, it's a QEMU fork that adds a machine (currently called hobgoblin, but will be Codasip Prime in the next release) with CHERI support that's almost exactly the same as X730 hardware; code that runs on it also runs out of the box on X730. You can find it here https://github.com/CHERI-Alliance/qemu/tree/codasip-cheri-riscv_v3
also, this question is for seL4 Foundation: are there plans to formal verify seL4 with this changes?
I thing you guys have put together two different Worlds that open a powerful new field: software formally verfied (seL4) + hardware enforced "memory protection". I a real World where very few orgs have the (intellectual) capability of formally verify all the software they use (specifically C/C++), Cheri support on top of seL4 looks very interesting to "CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains".
Exactly. Formal verification works great on a slowly moving delveoplement project such as the seL4 microkernel itself, but once you start building an actual dynamic OS on top of seL4 that'll need to keep rapidly changing and is an order of magnitude bigger in size, formally verifying this C/C++ codebase is really impractical and won't be scalable, let alone having the scarcity of experts to do so. So your options are to 1) (re)write everything in Rust (which also requires a relatively rare intellectual capability), or 2) use something like CHERI which is arguably just "good practice, clean C/C++ code" from an application developer perspective.
And as we already have LionsOS, so we get a third option (old CamkES. LionOS/Microkit, Cheri-seL4). It is not competition, it is evolution just following different valid paths. ANY of those paths is 1000 times better than current OSs/solutions. I love to have different options, all around seL4.
LionsOS/Microkit, CAmkES, or pretty much any C/C++ userspace framework (e.g., sel4test, sel4bench, Kry10 OS, etc) could be ported and run on CHERI-seL4 (the CHERI-enabled microkernel itself). We hope there will be opportunities in the future (especially once we have commercial CHERI processors people can buy) to formally verify the CHERI extensions in the kernel (e.g., the PR we submitted), and we're happy to collaborate on that.
I wish you guys collaborate to expand seL4 ecosystem.
Best,
On Tuesday, July 29, 2025, Hesham Almatary < heshamalmatary@capabilitieslimited.co.uk> wrote:
Hello Hugo, On Tue, 29 Jul 2025 at 18:26, Hugo V.C. <skydivebcn@gmail.com> wrote:
Hi Hesham,
2 questions:
do you run a modified seL4?
Yes definitely, as mentioned in the blog post. The link to the fork [1] is in the blog post and we’ve submitted a PR [2] upstream for it (also in the blog post). [1] https://github.com/CHERI-Alliance/CHERI-seL4 [2] https://github.com/seL4/seL4/pull/1469
is there any real world example of a Rust app running on top of
you solution?
I’ve built and run Microkit’s Rust hello example on top without any issues. You can also reproduce that if you’d like. Happy to give further instructions if needed. Regards, Hesham
Best,
On Tuesday, July 29, 2025, Hesham Almatary via Devel
<devel@sel4.systems> wrote:
> Hello, > > The CHERI Alliance has released a prototype of CHERI-seL4, an > experimental version of the seL4 microkernel with CHERI support. This > release includes CHERI-Microkit, a lightweight userspace framework, > and a set of exercises and tutorials designed to help developers > explore CHERI’s potential in a real microkernel environment. > > The release is aimed at developers who want to build and experiment > with memory-safe C/C++ software on seL4. It supports the draft > CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, > CHERI-Toooba, and CHERI-CVA6 on FPGA. > > For those who are unfamiliar with CHERI, CHERI support in seL4 enables > memory-safe C/C++ user-level projects and applications without having > to (re)write code in languages like Rust. This complement's seL4's > strong isolation between different components, enforced by the MMU and > seL4's software capabilities. > > We welcome any feedback. > > Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/ > > Regards, > Hesham > _______________________________________________ > Devel mailing list -- devel@sel4.systems > To unsubscribe send an email to devel-leave@sel4.systems >
Just an observation: the CHERI seems to be covered by multiple patents, including an European one. https://patents.google.com/patent/EP3819774B1/en https://copilot.microsoft.com/chats/ta8nCxScGESH7MdGZsubx ----------------------citation------start----------------------------- The CHERI (Capability Hardware Enhanced RISC Instructions) architecture has been adapted to RISC-V, but identifying all patents that specifically cover the RISC-V-related CHERI instruction set is a bit tricky. CHERI itself is a research-driven architecture developed by SRI International and the University of Cambridge, and much of its work has been published openly for academic and security purposes2. However, there are some patents and applications that touch on related technologies: x) U.S. Patent Application #20210365266: Describes a RISC-V implemented processor with hardware acceleration supporting user-defined instruction sets. While not explicitly labeled as CHERI, it may overlap in concept with CHERI-style extensions. x) The CHERI-RISC-V architecture is being refined for standardization, and while the core CHERI work is largely open-source, individual implementations or enhancements by third parties (e.g., hardware vendors) may be patented separately. ----------------------citation------end------------------------------- If the only point of using the RISC-V over ARM was that hardware vendors can produce those chips without needing to pay license fees or be otherwise restricted due to patents, then I really do not understand, why do people bother with the CHERI. A workaround might be to use formal verification of software combined with a patent-free instruction set. Thank You for reading my comment.
Hello Martin, On Thu, 31 Jul 2025 at 10:57, Martin Vahi via Devel <devel@sel4.systems> wrote:
Just an observation: the CHERI seems to be covered by multiple patents, including an European one.
https://patents.google.com/patent/EP3819774B1/en
https://copilot.microsoft.com/chats/ta8nCxScGESH7MdGZsubx ----------------------citation------start----------------------------- The CHERI (Capability Hardware Enhanced RISC Instructions) architecture has been adapted to RISC-V, but identifying all patents that specifically cover the RISC-V-related CHERI instruction set is a bit tricky. CHERI itself is a research-driven architecture developed by SRI International and the University of Cambridge, and much of its work has been published openly for academic and security purposes2.
However, there are some patents and applications that touch on related technologies:
x) U.S. Patent Application #20210365266: Describes a RISC-V implemented processor with hardware acceleration supporting user-defined instruction sets. While not explicitly labeled as CHERI, it may overlap in concept with CHERI-style extensions.
x) The CHERI-RISC-V architecture is being refined for standardization, and while the core CHERI work is largely open-source, individual implementations or enhancements by third parties (e.g., hardware vendors) may be patented separately.
----------------------citation------end-------------------------------
If the only point of using the RISC-V over ARM was that hardware vendors can produce those chips without needing to pay license fees or be otherwise restricted due to patents, then I really do not understand, why do people bother with the CHERI. A workaround might be to use formal verification of software combined with a patent-free instruction set.
This is completely wrong. CHERI as an open ISA extension is similar to RISC-V and is entirely open-source and patent-free (including a fully open specification that is even machine executable and has formally proven properties); you don't need any licence or permission to use or implement it in your processor and there have been many open-source implementations of CHERI. See [1] that has a list of open publications, resources, implementations, etc about CHERI since its inception over the past decade. A hardware vendor can implement RISC-V as an ASIC processor without having a licence or paying and still choose to patent it if they add their own extra accelerators or IP, and that's the same for CHERI. This is exactly what your second search result is saying with regard to CHERI-RISC-V; nothing in your search results suggests that CHERI is patent-protected at all. In this technical report [2], there is an explicit declaration by Cambridge and Arm (Morello) that they have not filed any patents covering the material in the report. [1] https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ [2] https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-953.pdf Regards, Hesham
Thank You for reading my comment.
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
participants (4)
-
Gernot Heiser -
Hesham Almatary -
Hugo V.C. -
Martin Vahi