4 ms·
To people interested in software process. There is a consensus that formal verification and automatic checks in software (even hardware) are a debugging tool, n
by posix_me_less 5y ago
To people interested in software process. There is a consensus that formal verification and automatic checks in software (even hardware) are a debugging tool, not a comprehensive success/security policy like the linked article would suggest.
- cvwright 5y ago"People interested in software process" have been trying, and failing, to write secure C code for 50 years. But they've made a ton of money trying!
- posix_me_less 5y agoC was not initially intended for such a thing, although later people tried to restrict it. Also, "secure C code" is too vague. It depends on the scope. Grep is quite secure in what it does. Linux, less so.
- touisteur 5y agoI'm curious where you get this consensus. It's not at all shared by everyone, especially with the huge strides SPARK and Frama-C have made.
- posix_me_less 5y agoI didn't mean academic consensus. More like industry / security-aware people in IT consensus - almost nobody in software does formal verification and it would be foolish for any user, whether person, business or government, to take this as solution to their VM hosting security problems. Yes formal verification has made advancements and is a useful tool, in proper context. Not in the context the article is selling the work of the researchers.