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.
aws.amazon.com/blogs/security…
aws.amazon.com/blogs/security…
Read the article first! but SideTrail is designed to find and also measure side-channels, which are code-paths that can leak secret data by introducing timing or other side-effects that depend on the secret data (and sometimes attackers can measure the effects).
With SideTrail you mark an entry and exit point in your code, and annotate whatever data as "THIS SHOULD BE SECRET" and it rigorously analyzes/simulates execution to tell if you if the code will execute any differently based on the data.
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.
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!
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. github.com/awslabs/s2n/tr…
