[UncleMeat]

It is not possible to remove ub from the spec without turning everything into a pdp-11 emulator, which will sabotage performance on many platforms.

I also don’t believe that a single person on the planet can write a secure c program of meaningful complexity. Static analysis tooling has demonstrated that it isn’t up to the task of saving developers from themselves.

[dnautics]

What about SEL4?

[kaba0]

Written over many many years by experts of a field, and the end result is at most somewhat complex, nowhere near the complexity of even the monolith SPA of your favorite website.

[dnautics]

GP said:

> meaningful complexity

Not, "the most complex". If an OS that can lock down DARPA self-flying helicopter software is not meaningful enough for you....

[kaba0]

Less than 10 000 lines of code. But let’s say we accept it as an exception — it is most definitely not the “standard way” of writing C programs.

[dnautics]

From GP:

> It is not possible to remove ub from the spec

did not say "it is not standard to remove ub"...

[posix_me_less]

The speed of development was very low, and how many people can check the proofs?

[dnautics]

> The speed of development was very low,

Not a part of GP's assertion

> and how many people can check the proofs?

it's not necessary, the proofs are checked using automation. I'm directly taking a shot at this assertion:

> Static analysis tooling has demonstrated that it isn’t up to the task

[oscardssmith]

Just because you have a proof doesn't mean it proves the right thing.

[dnautics]

Congratulations. You have won the argument "there is no perfectly secure system", which no one was arguing.

[UncleMeat]

I've got a strong background in formal verification. I do not believe that "formally verified" means "security bug free". In fact, I personally know researchers who have had vulns found in their formally verified code more than a decade after they completed the verification.

[posix_me_less]

I agree, there are lots of outrageous claims out there about "provably secure software" which seem very dubious.

What are your thoughts on SEL4, is it really a breakthrough it is made to be in success of formal verification? Is there a way for users/administrators deploying it to verify themselves authors' claims? Or is it too difficult? I am afraid the latter...

In 2004 Peter Gutmann in his thesis/book criticized the hype around effectivity of formal methods in computer security [1]. Has the situation changed?

[1] https://archive.org/details/springer_10.1007-b97264

[UncleMeat]

Breakthrough? No. Good work? Yes.

[dnautics]

I don't think there is any reasonable standard of security that demands perfection.