[Cryptography] [FORGED] Re: How programming language design can help us write secure crypto code

[Christian Huitema]

On Sunday, November 1, 2015 6:40 AM Thierry Moreau wrote:
> 
> On 31/10/15 01:29 AM, Peter Gutmann wrote:
> > ...
> >    causes the compiler to check that, in calls to my_memcpy, arguments dest
> and
> >    src are non-null. If the compiler determines that a null pointer is passed
> >    in an argument slot marked as non-null, and the -Wnonnull option is
> enabled,
> >    a warning is issued.
> 
> This is a compile-time verification, a compile-time warning. It is
> obviously the case that compile-time "determinations" are limited, and a
> reasonable programmer would not expect a compile-time warning for a null
> pointer that can be "determined" only at run-time.

Actually, a lot can be determined at compile time. If the function's manifest specifies that an argument shall not be null, the compiler can check whether the calling program guarantees that the argument will not be null. That is done by tracing the variable through the potential execution paths, which requires annotating functions handling that variable, checking for "== NULL" tests, etc. Of course at compile time the exact values of a variable cannot be known, but a check whether a variable is guaranteed non null or not is entirely possible.
> > ...
> > Here's what gcc actually does:
> >
> >    The nonnull attribute specifies that some function parameters should be
> non-
> >    null pointers. For instance, the declaration [...] causes the compiler to
> >    silently remove any checks for null pointers in the code when compiling it.
> >    No warnings will be issued.

That's arguably perfectly fine, if the compiler can also check that the function will never be called with a non-null argument. Of course, that's a big if. It implies that the non-null property is exposed in the language or its extensions, and properly verified. It also requires that if the function is placed in a library, the linker does not assemble it with an application that does not honor the extensions.

By the way, the same kind of declarations tests can be used to verify array bounds, zero termination of strings, actual initialization of variables, etc. It is technically possible to extend C to do all that. 

-- Christian Huitema