Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
Discover and Prevent Linux Kernel Zero-Day Exploit Using Formal Verification (digamma.ai)
3 points by vzaliva on June 8, 2021 | hide | past | favorite | 3 comments


[Coq, VST, CompCert]

Formal methods: https://en.wikipedia.org/wiki/Formal_methods

Formal specification: https://en.wikipedia.org/wiki/Formal_specification

Implementation of formal specification: https://en.wikipedia.org/wiki/Anti-pattern#Software_engineer...

Formal verification: https://en.wikipedia.org/wiki/Formal_verification

From "Why Don't People Use Formal Methods?" https://news.ycombinator.com/item?id=18965964 :

> Which universities teach formal methods?

> - q=formal+verification https://www.class-central.com/search?q=formal+verification

> - 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?


Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all?


Formal 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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: