[Cryptography] Formal Verification (was Re: Trust & randomness in computer systems)

[Peter Gutmann]

Christian Huitema <huitema at huitema.net> writes:

>C/C++ extensions like SAL Annotations make static code analyzers really
>powerful. If developers use SAL honestly, the code analyzers will definitely
>catch have Heart Bleed or Go To Fail bugs. Adding ASSERT statements liberally
>expresses a lot about code intent, and will catch potential issues during a
>debug break.

SAL is probably the best thing we have right now in terms of analysis, in that
while analysers like Coverity and Fortify and Klocwork have more powerful
analysis engines than PREfast, they have to infer things about code behaviour
that are made explicit by SAL annotations.  A Coverity that understands SAL
would be a very powerful analyser indeed.

The one downside with SAL is that you're stuck with what Microsoft give you.
If there's something that your API does but the Windows one doesn't, there's
no way to express it in SAL.  In other words SAL is very non-orthogonal in
places, you can say "this by-value parameter can have the range [0...1000]"
(_In_range_ in SAL terms) but not "this by-reference parameter can have the
range [0...1000]" (_Deref_inout_range_ in SAL terms, it's documented but
doesn't actually exist).  There's also no obvious feedback channel to get
things fixed, you just have to wait for the next version of Visual Studio to
appear and hope something's changed.

>They tend to be arcane, something like "use after free during a race
>condition." 

SAL can detect some types of lock contention statically, which is impressive.
Or at least it would be if the annotation worked the way it was documented.

Peter.