[Cryptography] formal verification +- resource exhaustion

James A. Donald jamesd at echeque.com
Thu Mar 2 21:21:16 EST 2017


>> Also, as mentioned elsewhere on this thread, higher-level constructs (e.g.
>> smart pointers) can make it easier to reason about code and prove invariants.

On 3/2/2017 8:16 PM, Peter Gutmann wrote:
> As far as I know they make it much harder to analyse, not easier.

They make it harder for machines to analyze.  But what the machine 
analysis actually means for human purposes is not always clear.

> since it bans a whole range of risky C behaviour, and also
> forces you to think a lot more about how you structure your code.

Forces you to do a lot more work.  Which work you can get wrong, and 
which work smart pointers and RAII make the compiler do for you without 
you having to think about them.

Obviously it is impossible to prove that an arbitrary C program will not 
have resource leaks, wild reads and writes to freed memory, etc.  A 
human may well be able to reason that a program is correct, when a 
mechanical theorem prover could not.So if one employs a mechanical 
theorem prover one is somewhat arbitrarily restricted from writing an 
arbitrary C program.  In which case one loses many of the benefits of C. 
  That C is a low level language means it can do things that are often 
difficult in other languages.

If we restricted C to stack and static variables and forbade pointers, 
would not have memory leaks or wild writes.  And we would not be able to 
write a lot of programs, even though it is still Turing complete.

Because C requires manual management of memory and resources, people 
always get it wrong.  They always have leaks, always have wild reads and 
wild writes.  Many people therefore propose garbage collected languages 
for ordinary not terribly good programmers, which is why Java has become 
the standard and major language.  Java is more or less C with garbage 
collection and a touch of C++.  You can write the same program in less 
time in Java because you do not have to do manual memory management. 
But memory is only one resource among many.

There are lots of things that Java really cannot do, or really cannot do 
well.  I suspect that there are lots of things a C program amenable to 
theorem proving really cannot do, or really cannot do well, though 
obviously you know more of this than I do.

You recommend a tool that is a lot more work than my existing tools, and 
can probably do less than my existing tools, recommend it largely 
because it produces programs that would be free from resource leaks and 
wild writes.  Now if I was still writing in C, I would probably have an 
intolerable problem of wild writes and resource leaks in any large 
program, and would be desperately looking for a cure, any cure.  But 
writing in C++11, I do not.


More information about the cryptography mailing list