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.