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

[Jerry Leichter]

>> __attribute__(( nonnull 1 )) \
>> int double( int *ptr )
>>  {
>>  if( ptr == NULL )
>>    return( -1 );
>>  return( *ptr * 2 );
>>  }
>> 
>> [...]
>>  thing = double( thingPtr );
>> [...]
> 
> I have never used that annotation in earnest yet, but
> I'll give it a guess....
> 
> You claimed to be passing it a pointer to an integer,
> with an annotation that told it that a null pointer
> was an error....
I have no idea exactly how gcc actually uses this annotation, but you might want to read https://docs.eiffel.com/sites/default/files/void-safe-eiffel.pdf.  This paper introduces the notion of "non-void" (Eiffel terminology for "non-null") reference types.  A non-void reference type is a reference type which does not include "void" in its range.  The compiler guarantees that a variable of this type cannot ever be observed to contain void.  If you think about it, this is really no different from guaranteeing, in a safe language, that a reference cannot point to random memory, or to an object of the wrong type.  This is a *compile-time* check:  The compiler doesn't add run-time checks for void; there would be no point, as it can prove they will never actually find void.

Surprisingly, once you decide this is the right way to do things ... it turns out not to be that hard.  The Eiffel collections libraries were modified to consistently take and return non-void references pretty much everywhere.

Java these days has a standardized @NonNull annotation which is intended to mean the same thing, though enforcement is generally left to lint-like code checkers.  I've used C++ compilers with similar annotation and checking.  Typically, their response to checking whether a non-null-typed reference is null is to complain about dead code.

                                                        -- Jerry