bumper sticker slogan for secure software

[pmeunier at cerias.purdue.edu (Pascal Meunier)]

On 7/20/06 3:46 PM, "Florian Weimer" <fw at deneb.enyo.de> wrote:

> * Pascal Meunier:
>
> > But it's true for stupid bugs like buffer overflows and format string
> > vulnerabilities, in which we're still swimming, and the proof is the fact
> > that those aren't possible in some languages.
>
> Could you name a few such language implementations? 8-)
>
> In most cases, the components that enforces the absence of buffer
> overflows are written in C.
<snip>

That's irrelevant.  What is important is that some magic formal tool could
say that some code in language "A", where bug of type "k" is possible, is
not equivalent to the version in language "B", where type "k" bugs are
impossible, ergo you have found a type "k" bug (in the absence of any other
bug in that section of code...).

I know someone is going to ask, "why didn't you code it only in language B
then?", to which there can be many different answers, and I don't want to
get into that.


> >  For design/requirements bugs, I'm reading:
>
> Safety-critical software is a very different beast.  You can make much
> stronger assumptions about the environment.  It's not clear if the
> results apply to software security in open system.
>
> I'm not saying that formal methods have no value.  But I doubt that
> comparisons with projects at completely different
> dollars-per-line-of-code levels give immediate insights.

That's one of the things I'm hoping for:  that more and better formal
methods become more affordable and practical.  Spark, for example,
demonstrated that the costs of some formal methods were much lower than what
people expected, in real projects.  That gives me hope.

Pascal