[Cryptography] Ada vs Rust vs safer C

Jerry Leichter leichter at lrw.com
Sun Sep 18 19:13:34 EDT 2016


>> If there are annotations that are really helpful and not utterly Windows-
>> specific, we can put them into GCC.  We just need documentation.
> 
> None of them are Windows-specific, it's just things like "this value can only
> take ranges between 0 and 100" or "this value points to a buffer whose size is
> defined by that other value".  There are composite annotations that say things
> like "this is a handle to some Windows-specific thing", but they're just
> convenience macros built up from the lower-level primitives.
There was a project called ESC (Enhanced Static Checking or something like that) at the DEC labs way back when that did analysis like this - based on annotations - of Modula-3 code.  It later got picked up by a group at MIT would produced a portable version which targeted C, among other languages.  The name, however, is something I can no longer recall.

This was based on a very expressive annotation language and a fairly powerful proof engine, so with proper annotations you could verify some quite meaningful properties of C (or other language) programs.  Unfortunately, the annotation language was highly mathematical in form, well beyond the comfort zone (or even competence) of the vast majority of programmers.  So the effort never had any significant real-world impact.

This is the side of annotations and program verification systems that's proved a stumbling block pretty much forever.  No one has really solved the problem of working either with un-annotated code in languages that are in actual use; or designing an annotation system that real-world programmers can use effectively.

And that doesn't even get to the problem of existing code.  If you design this stuff in from the beginning, it can work fairly well.  In fact, the MIT system could probably be workable in a project that started off with someone with the appropriate background defining a bunch of assertions appropriate to the project at hand, providing the developers with what would effectively be an annotation DSL that they could use without needing to understand all the details.

But trying to retrofit any reasonable level of annotation and you're likely to end up throwing your hands up in despair.  A classic example is const-correctness in C++.  If done consistently, up front, it's a *big* help in pinning down the semantics of your code - in a compiler-checkable way - and avoiding all kinds of bugs.  But anyone who's tried to add const declarations to an existing code base of any size knows how that goes:  It's an all-or-nothing effort.  You start at the bottom, add some const's, find that the methods that call your methods now fail to compile, fix those ... and repeat until you've walked through a substantial portion of the code, or have given it up as a lost cause.

I've recently been repeating this experience in Java.  Java now has a way to annotate a variable or parameter or return value - and even, since Java 8, things like the values in a map - as non-null; and even the standard compilers will tell you about violations.  A *fantastic* way to avoid the dreaded NPE's of too much Java code.  But like const-correctness, non-null annotations spread.  You annotate the parameters of some method, then have to fix up all the callers.  The job can quickly become overwhelmingly large.  Since the compiler messages for violations are typically warnings, what you tend to find is that someone changed a subtree of the call graph and gave up, leaving the warnings from callers into that subtree alone.  So now you have the worst of both worlds:  Looking at subtree, it appears that it's "NPE safe" - the @NonNull annotations guarantee it, no?  But in fact the warnings at the points of call mean that the annotations can't actually be trusted to mean anything.  (The compiler doesn't insert checks at transitions from unannotated to annotated code.  That might be an interesting addition.)

The fact that no one has annotated the Java library - nor is anyone likely to - doesn't help the cause.

There are actually some fairly general kinds of program assertion annotations available now for Java, but other then @NonNull, none are yet checked by any compiler.  There are some generic checking frameworks available, but they don't seem to have gotten much traction.  The Java community, in general, seems to have little interest in compile-time checking - "Just write a complete set of unit tests".  (Hmm, I wonder if there would be more support if someone developed an analyzer that generated unit test to cover the annotations in a program.  TDD via annotations....)

                                                        -- Jerry



More information about the cryptography mailing list