Re: SPI, Ounce Labs Target Poorly Written Code

[Blue Boar <BlueBoar () thievco com>]

Peter Amey wrote:

I would assert that using SPARK it is very /hard/ to something stupid
and /impossible/ to do something stupid that wouldn't be obvious to
the SPARK Examiner tool.  In fact, the only way I can think of doing
so would be to construct a formal specification for stupidity and
then correctly implement it (which is clearly feasible).


To clarify, I'm talking about things like passing unfiltered user input 
to a system shell, or a native API, something like that.  I wasn't 
neccessarily referring to blowing up your buffers, etc...


If SPARK is designed to stop things like that, then I'll happily go and 
try to do something stupid in it...


My basic point (which I probably made poorly) is that a language that 
keeps one from blowing up their buffers, getting their signs wrong, 
etc... won't help logic errors and bad design.  I have nothing against 
"secure" languages, and I'd be happy to see them in wider use.  I was 
just sceptical about these libraries under discussion that can keep 
someone from introducing security holes.


                                                BB