Monday mini mini-thread! AWS SideTrail, built by the automated reasoning group here at AWS, is the coolest formal analysis tool I've seen yet, because it catches bugs I've actually written! and the kind of bugs that have escaped careful code review.https://aws.amazon.com/blogs/security/how-aws-sidetrail-verifies-key-aws-cryptography-code/ …
-
-
Nearly-all cryptographic code has these kinds of side-channels, most software implementations of AES for example, and it's the basis for Lucky13 and other issues. But eyeballing the code changes it takes to fix is really hard.
Show this thread -
For example, OpenSSL fixed Lucky13, but then later introduced LuckyMinus20 - a regression in the same code, which was very hard to spot. SideTrail detects these kinds of issues glaringly, and gives the programmer the measurements they need to decide what to do!
Show this thread -
Fits right in with regression tests, like we've done in s2n: now running on every build! Anyway, end of thread, and read the code! It uses Boogie and LLVM and other amazing tricks.https://github.com/awslabs/s2n/tree/master/tests/sidetrail …
Show this thread
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.