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]
