[Cryptography] How programming language design ca help us write secure crypto code

[Peter Gutmann]

Dennis E. Hamilton <dennis.hamilton at acm.org> writes:

>The "perfect programmer" assumption has always been bad news.  Now that I am
>working on open-source productivity software hawked to casual users, I find
>the "perfect user" assumption to be an even-worse companion.

At the risk of sounding like a Microsoft commercial, there's one company
that's going to great lengths to deal with the "perfect programmer"
assumption.  For example here's ExAllocatePoolWithTag():

  __drv_allocatesMem(Mem)
  _When_((PoolType & PagedPool) != 0, _IRQL_requires_max_(APC_LEVEL))
  _When_((PoolType & PagedPool) == 0, _IRQL_requires_max_(DISPATCH_LEVEL))
  _When_((PoolType & NonPagedPoolMustSucceed) != 0,
       __drv_reportError("Must succeed pool allocations are forbidden. "
                         "Allocation failures cause a system crash"))
  _When_((PoolType & (NonPagedPoolMustSucceed |
                    POOL_RAISE_IF_ALLOCATION_FAILURE)) == 0,
       _Post_maybenull_ _Must_inspect_result_)
  _When_((PoolType & (NonPagedPoolMustSucceed |
                    POOL_RAISE_IF_ALLOCATION_FAILURE)) != 0,
       _Post_notnull_)
  _Post_writable_byte_size_(NumberOfBytes)
  NTKERNELAPI PVOID NTAPI
  ExAllocatePoolWithTag (
    _In_ __drv_strictTypeMatch(__drv_typeExpr) POOL_TYPE PoolType,
    _In_ SIZE_T NumberOfBytes,
    _In_ ULONG Tag
  );

This allows the compiler to check at compile time that you're using the
function correctly.  The above (which should be at least somewhat intuitive,
or maybe I've just spent too much time with the SAL annotations) specifies the
precise conditions under which you can call ExAllocatePoolWithTag().  Instead
of getting the dreaded IRQL_NOT_LESS_OR_EQUAL bluescreen at some point whem
the code is run, the _IRQL_requires_max_ annotation tells you at compile time
what you can and can't do.

The above example looks like quite a handful, but MS have done it all for you
so you don't normally see the annotations, just their product.

Oh, and when the annotation says something like _Post_notnull_, it's used to
guide the analyser to warn about problems.  NULL checks are not removed from
the code.

Now if only Windows 10 didn't suck so much, sigh.

Peter.