GNU Coding Standards: Writing Robust Programs

Re:GNU Coding Standards: Writing Robust Programs by UncleMeat on Friday June 11, 2021 @02:26PM (#27476868)

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.

[ Parent | on HN ]

Re:GNU Coding Standards: Writing Robust Programs by posix_me_less on Saturday June 12, 2021 @09:52AM (#27484500)

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

[ Parent | on HN ]

Re:GNU Coding Standards: Writing Robust Programs by UncleMeat on Saturday June 12, 2021 @11:51AM (#27485257)

Breakthrough? No. Good work? Yes.

[ Parent | on HN ]

Re:GNU Coding Standards: Writing Robust Programs by dnautics on Friday June 11, 2021 @03:26PM (#27477438)

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

[ Parent | on HN ]