3 ms·
What does it mean to prove the correctness of code like this. For example, is it possible to prove that no side channel attack exists in a function or library?
by asdfasgasdgasdg 7y ago
What does it mean to prove the correctness of code like this. For example, is it possible to prove that no side channel attack exists in a function or library? What form does such a proof take? How do you express, mathematically, that no disclosure of data is possible in response to arbitrary requests and function calls? Are there any recent major vulnerabilities that would have been prevented if the code had been formally proven first? Heartbleed? Spectre? Meltdown?
- jimbob45 7y agoWell, to start, if you write pure functional code, then you can reason about the code without having to worry about side effects. EDIT: As a starting point. Pure functional programming is one tool among the many in your toolbox. It should not be anyone's entire strategy.
- polemic 7y agoBold assertion in the face of side channel and timing attacks.
- mcguire 7y agoIs crypt32 supposed to be secure against side channel and timing attacks?
- magicalhippo 7y agoSide effects != side channels. Side channel is stuff like your multiplication code takes different amounts of time depending on the arguments, or your cache hit/miss patterns depend on arguments and thus can leak the argument.
- cjbprime 7y agoHeartbleed was found (after the fact) by a simple fuzzer. The ability of fuzzers has massively increased in recent years.
- asdfasgasdgasdg 7y agoFuzzers are great! I have fuzzed one or two mission critical high exposure libraries in my time. But they are a totally different thing than formal verification.