4 ms·
Discover and Prevent Linux Kernel Zero-Day Exploit Using Formal Verification
- westurner 5y ago[Coq, VST, CompCert] Formal methods: https://en.wikipedia.org/wiki/Formal_methods https://en.wikipedia.org/wiki/Formal_methods Formal specification: https://en.wikipedia.org/wiki/Formal_specification https://en.wikipedia.org/wiki/Formal_specification Implementation of formal specification: https://en.wikipedia.org/wiki/Anti-pattern#Software_engineering https://en.wikipedia.org/wiki/Anti-pattern#Software_engineer... Formal verification: https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification From "Why Don't People Use Formal Methods?" https://news.ycombinator.com/item?id=18965964 https://news.ycombinator.com/item?id=18965964 : > Which universities teach formal methods? > - q=formal+verification https://www.class-central.com/search?q=formal+verification https://www.class-central.com/search?q=formal+verification > - q=formal+methods https://www.class-central.com/search?q=formal+methods https://www.class-central.com/search?q=formal+methods > Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs?
- westurner 5y agoCan there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all?
- vzaliva 5y agoFormal methods could be used to prevent side channel attacks. However preventing each type of attack requires specifying properties which needs to be proven to assure it is is not possible. I am not very famililiar with TLA+, but I think in general it is not guaranteed to provide side channel attacks, such as based on timing, CPU state, etc.