Re: Buffer overflow Article - CACM

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Harald Korneliussen wrote:
> Peter Amey wrote:
> 
>>OF course, using SPARK, we can statically prove the absence of buffer
>>overflows (and many other potential exploits) and thus add precisely
>>nothing in the form of a run-time overhead!
>>
>>Peter
> 
> 
> I though that with SPARK, you have to write your program with no moving
> parts (or dynamic data structures) and then supply a suite of proofs,
> which may be quite hard, even with the assistant? How often is this
> practical?
> 

Obviously how hard it is it depends what it is you are trying to prove. 
  Proving that a SPARK program is free from all run-time errors (of 
which "buffer overflow" is but one) is remarkably straightforward.  A 
majority of SPARK users are using this technology in an industrial 
setting on a regular basis.

For exception-freedom proof, you do not have to add extra annotations, 
the Examiner generates the necessary proof obligations from the language 
rules of Ada; it essentially generates proof obligations that mirror 
what the LRM requires for run-time checks.  It is necessary to provide 
some extra information, such as the bounds of the predefined types such 
as Integer using a configuration file mechanism.

The Simplifier tool, that comes with the SPARK Examiner, usually 
discharges over 95% of the resulting verification conditions (assuming 
the code is correct of course!).  Sometimes the process prompts the 
addition of a precondition here and there which is, of course, extremely 
useful intelligence for future maintenance of the software.

This paper: http://www.praxis-his.com/pdfs/Industrial_strength.pdf gives 
an overview of the process.  The Simplifier hit rate has gone up sharply 
since it was written but the principles are the same.

regards


Peter