[seL4] Re: Question about LionsOS

I agree with Gernot. Ultimately, in deployment as a secure system, isn't the whole point of this to have confidence that it is in fact secure? As a practical matter of convenience for development, I would find it much easier to work with Sel4 in a virtualized environment. However, I would not have confidence for production delivery if it is not on bare metal. Hopefully, we have assurance from the silicon on up, Security is incredibly difficult and it promises to get much more difficult quickly as AI weaponry comes online. For my long-term project I have been looking at a RISC-V platform that we can specify such that it can be visually inspected microscopically to verify that the silicon itself is as specified. I am not convinced that absolute security is possible even in theory, but the higher your security, the more you send attackers after lower hanging fruit. I took a brief look at the sources on GitHub and I was surprised to see that the coding standards violate a few of my rules as to single point of entry, single point of exit, wrapped return statements, etc. However, because the code base is small it can be read and reviewed and to the extent that stuff like that might post problems it can be systematically repaired. Gernot -- apropos of the single point of entry/exit in code, I was given to understand years ago that violating this made certain types of proofs as to code behavior theoretically impossible. I am curious as to how you work around this. Am I simply mistaken? Ignore if you wish, I will not be offended. On Thu, Apr 18, 2024 at 7:14 AM Gernot Heiser via Devel wrote:

On 18 Apr 2024, at 20:38, Hugo V.C. wrote:

The challenge that I probably didn't expressed correctly, is to integrate seL4 on top of other dynamic systems (in example to virtualize a browser), as seL4 needs to know in advance how much memory will have available... Running seL4 on bare metal is a "kids game" (don't want to offend anyone), the challenge is to integrate it on systems where resources are dynamically assigned.

I don’t think I understand. Running seL4 in any way other than on bare metal makes no sense whatsoever.

Gernot _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

-- Bob Trower --- From Gmail webmail account. ---