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 < [email protected]> wrote: > Hello Hugo, > > On Thu, 31 Jul 2025 at 09:13, Hugo V.C. via Devel <[email protected]> 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 >> (<[email protected]>) escribió: >> >> > On 30 Jul 2025, at 19:39, Hesham Almatary via Devel <[email protected] > >> > 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 -- [email protected] >> > To unsubscribe send an email to [email protected] >> > >> _______________________________________________ >> Devel mailing list -- [email protected] >> To unsubscribe send an email to [email protected] > _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
