bumper sticker slogan for secure software

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

On 7/20/06 1:57 PM, "Gary McGraw" <gem at cigital.com> wrote:

> I'm afraid that's not true.  John Knight has a famous paper that shows that
> design/requirements bugs persist in n-version programming paradigms.  I'll let
> the interested people google that one up for themselves.
>
> gem

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.  For design/requirements bugs,
I'm reading:

Why Are Formal Methods Not Used More Widely?
John C. Knight Colleen L. DeJong Matthew S. Gibble Lu?s G. Nakano
Department of Computer Science
University of Virginia
Charlottesville, VA 22903

http://www.cs.virginia.edu/~jck/publications/lfm.97.pdf

and the evidence is that engineers presented with formal specifications were
able to spot many design errors ("Validation by inspection was effective").
Therefore if you have a formal, high-level version it can be validated
better, and formal methods give proof that the lower-level code conforms.

I call that all-around better, and I'm hoping for more of it and better ways
to do it.  Now if you order a cat and needed a dog, nobody can help you.

Pascal


>  -----Original Message-----
> From:  Pascal Meunier [mailto:pmeunier at cerias.purdue.edu]
> Sent: Thu Jul 20 13:54:42 2006
> To: Florian Weimer; der Mouse
> Cc: SC-L at securecoding.org
> Subject: Re: [SC-L] bumper sticker slogan for secure software
>
>
>
> On 7/20/06 11:58 AM, "Florian Weimer" <fw at deneb.enyo.de> wrote:
>
> > * der Mouse:
> >
> > > > > Absolute security is a myth.  As is designing absolutely secure
> > > > > software.
> > >
> > > > I have high hopes in formal methods.
> > >
> > > All formal methods do is push bugs around.  Basically, you end up
> > > writing in a higher-level language (the spec you are formally verifying
> > > the program meets).  You are then subject to the bugs present in *that*
> > > "program" (the spec) and the bugs present in the "compiler" (the formal
> > > verifier).
> >
> > But people are forced to spend more time with the code, which
> > generally helps them (in particular smart people) to eradicate bugs.
> > Another way to achieve the same thing is to freeze the code base and
> > let it mature over decades, but I don't see the business model for
> > that.
>
> Also, writing it twice with different languages, especially at different
> levels of abstraction, makes it less likely that the same bugs will appear
> in both.  You can choose the higher level language so that it has great
> expressive power exactly for the things that are a pain to capture and
> verify (and thus a source of bugs) in the lower-level language.  Last time I
> checked, formal methods were even able to catch design errors in some
> networking protocols.  But you're right, they are not absolutely perfect
> because the tools and operators aren't, etc...  That doesn't mean they can't
> help a great deal.  I have great hopes for their usefulness.  Maybe some day
> they will help so much that the distinction between what they can produce
> and absolutely secure software will become too small to matter.  Whether
> we'll still be alive when that happens is another question.
>
> Pascal
>
>
>
> _______________________________________________
> Secure Coding mailing list (SC-L)
> SC-L at securecoding.org
> List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
> List charter available at - http://www.securecoding.org/list/charter.php
>
>
>
>
> ----------------------------------------------------------------------------
> This electronic message transmission contains information that may be
> confidential or privileged.  The information contained herein is intended
> solely for the recipient and use by any other party is not authorized.  If
> you are not the intended recipient (or otherwise authorized to receive this
> message by the intended recipient), any disclosure, copying, distribution or
> use of the contents of the information is prohibited.  If you have received
> this electronic message transmission in error, please contact the sender by
> reply email and delete all copies of this message.  Cigital, Inc. accepts no
> responsibility for any loss or damage resulting directly or indirectly from
> the use of this email or its contents.
> Thank You.
> ----------------------------------------------------------------------------
>
> _______________________________________________
> Secure Coding mailing list (SC-L)
> SC-L at securecoding.org
> List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
> List charter available at - http://www.securecoding.org/list/charter.php