Re:Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk
by Animats on Saturday November 02, 2024 @04:41PM
(#42029090)
It'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-2...
Re:Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk
by cryptonector on Saturday November 02, 2024 @06:15PM
(#42029601)
> 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.
Re:Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk
by microkerneldude on Sunday November 03, 2024 @02:11AM
(#42031591)
seL4 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/ – not yet verified, but will be.
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.