4 ms·
> The trouble with SEL4 is that it's not much more than a hypervisor. People tend to run Linux on top of it, which loses most of the security benefits. Well, y
by cryptonector 2y ago
> The trouble with SEL4 is that it's not much more than a hypervisor. People tend to run Linux on top of it, which loses most of the security benefits.
Well, yeah, that's a problem.
But the bigger problem is that this works for jets, as long as you don't need updates. It doesn't work for general purpose computers, for office productivity software, for databases (is there an RDBMS with a correctness proof?), etc. It's not that one couldn't build such things, it's that the cost would be absolutely prohibitive.
- Animats 2y agoIt's not for everything. But the serious verification techniques should be mandatory in critical infrastructure. Routers, BGP nodes, and firewalls would be a good place to start. Embedded systems that control important things - train control, power distribution, pipelines, water and sewer. Get those nailed down hard. Diagrams like this scare me.[1] [1] https://new.abb.com/docs/librariesprovider78/eventos/jjtts-2017/presentaciones-peru/(miguel-mendoza)-the-debut-of-the-relion-2-2.pdf https://new.abb.com/docs/librariesprovider78/eventos/jjtts-2...
- cryptonector 2y ago> Routers, BGP, ... Well, but those need new features from time to time, and certification would make that nigh impossible. I'd settle for memory-safe languages as the happy middle of the road.
- microkerneldude 2y agoseL4 is a bit more than a hypervisor, but it's definitely very low-level. In terms of a useful seL4-based system, you may want to look at https://trustworthy.systems/projects/LionsOS/ https://trustworthy.systems/projects/LionsOS/ – not yet verified, but will be.