Re: [SC-L] Harvard vs. von Neumann

[Blue Boar]

der Mouse wrote:
>> Like it or not, the Web doesn't work right without Javascript now.
> 
> Depends on what you mean by "the Web" and "work right".  Fortunately,
> for at least some people's values of those, this is not true.

Obviously, I'm oversimplifying. I claim that there are enough web sites
that require active content to function right (in other words, that's a
big part of the reason they are popular) and that there is a big enough
critical mass of users who want to use those that it's going to stay.

Or another way to put it: First browser that drops support for
Javascript commits market suicide.

(Actually, the ratio of people who want flashy website to those who care
about disabling Javascript is probably 10,000:1, but I digress.)

Ryan
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Harvard vs. von Neumann

[David Crocker]

der Mouse wrote:

>>
> What Turing actually tells us is that it is possible to construct 
> programs that may be correct but whose correctness is not decidable. 
> This is a far cry from saying that it is not possible to build 
> well-structured programs whose correctness _is_ decidable.

True as far as it goes - but don't forget that you also haven't shown the latter
to be possible for programs of nontrivial size.
<<

Well, if you consider 86,000 lines of Ada a nontrivial size, this was shown back
in 1998 by the METEOR project. See "Meteor:
A Successful Application of B in a Large Project" by Patrick Behm, Paul Benoit,
Alain Faivre, and Jean-Marc Meynadier. The key to verifying large programs is to
structure them well, so that the verification can be done in a highly modular
fashion. The Design-by-Contract paradigm is an example of this.

>>
> The higher the level in which the human "codes", the [fewer] mistakes 
> there are to be made, assuming equal familiarity with the language 
> etc.

...but the more complex the "compiler", and the greater the likelihood of bugs
in it causing the resulting binary to fail to implement what the human wrote.
<<

This is potentially true, but is mitigated by a number of factors. First,
specification languages (and, for that matter, programming languages) do not
need to be as complicated as some existing programming languages (C++ springs to
mind). Second,
the semantics of the language you are starting from are formally defined (unlike
almost all programming languages), so the problem is much better defined than it
is for typical compilers. Third, what you call the "compiler" is in fact a
refiner (which refines specifications to algorithms) followed by a code
translator. The code translator is essentially a compiler for a fairly minimal
but well-defined programming language and is therefore well-known technology.
The difficult part is the refiner, but this can use mathematical rules to ensure
correctness - provided of course that the rules are correctly implemented. It
can also generate verification conditions to be passed to a prover in order to
ensure that the generated code really does meet the specification. If there is
any doubt as to the correctness of the theorem prover, the proofs can be passed
to an independent proof checker for verification.

In our own product, which does a limited amount of refinement of specifications
to code, the part that does the refinement was much easier to specify than the
code translator and we have found it highly reliable.

[snip]

>>
There are three places where problems can appear: (1) the specifications can
express something other than what the users want/need; (2) the coders can make
mistakes translating those specifications to code; (3) the translation from code
to binary can introduce bugs.  (No, step (2) cannot be eliminated; at most you
can push around who "the coders" are.  Writing specifications in a formal,
compilable language is just another form of programming.)
<<

Writing "executable specifications" can indeed be viewed as a form of high-level
programming, but it has a number of benefits:

- it is more concise, which leaves less room for some types of error;
- it relates much more directly to the requirements
- requirements can be added to the specification, then it can be proven that the
specification meets the requirements. For example, you might wish to express the
requirement "The HTML generated by this component will not include the text
"

Re: [SC-L] What's the next tech problem to be solved in softwaresecurity?

[Gary McGraw]

There is one on the drawing boards about this, but don't hold your breath!  I 
am working on it with Fabio Arciniegas.

Exploiting Online Games is first, and that comes out in July.

gem

company www.cigital.com
podcast www.cigital.com/silverbullet
blog www.cigital.com/justiceleague
book www.swsec.com



From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of McGovern, James 
F (HTSC, IT)
Sent: Monday, June 11, 2007 10:51 AM
Cc: sc-l@securecoding.org
Subject: Re: [SC-L] What's the next tech problem to be solved in 
softwaresecurity?

The next problem to be solved is moving higher up the food chain by teaching 
architects secure architecture principles. Would love to see Gary McGraw tackle 
this subject in his next book...


From: [EMAIL PROTECTED] on behalf of Kenneth Van Wyk
Sent: Sun 6/10/2007 9:37 AM
To: Secure Coding
Subject: Re: [SC-L] What's the next tech problem to be solved in 
softwaresecurity?


First off, many thanks to all who've contributed to this thread.  The
responses and range of opinions I find fascinating, and I hope that
others have found value in it as well.  Great stuff, keep it coming.

That said, I see us going towards that favorite of rat-holes here,
namely the "my programming language is better than yours, nyeah!"
path.  Let's please avoid that.  I'm confident that we've seen it
enough times to know that it ends with no clear winners (but plenty
of losers).

Cheers,

Ken
-
Kenneth R. van Wyk
SC-L Moderator
KRvW Associates, LLC
http://www.KRvW.com






*
This communication, including attachments, is
for the exclusive use of addressee and may contain proprietary,
confidential and/or privileged information. If you are not the intended
recipient, any use, copying, disclosure, dissemination or distribution is
strictly prohibited. If you are not the intended recipient, please notify
the sender immediately by return e-mail, delete this communication and
destroy all copies.
*
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] What's the next tech problem to be solved in softwaresecurity?

[McGovern, James F (HTSC, IT)]

The next problem to be solved is moving higher up the food chain by teaching 
architects secure architecture principles. Would love to see Gary McGraw tackle 
this subject in his next book...



From: [EMAIL PROTECTED] on behalf of Kenneth Van Wyk
Sent: Sun 6/10/2007 9:37 AM
To: Secure Coding
Subject: Re: [SC-L] What's the next tech problem to be solved in 
softwaresecurity?



First off, many thanks to all who've contributed to this thread.  The 
responses and range of opinions I find fascinating, and I hope that 
others have found value in it as well.  Great stuff, keep it coming.

That said, I see us going towards that favorite of rat-holes here, 
namely the "my programming language is better than yours, nyeah!" 
path.  Let's please avoid that.  I'm confident that we've seen it 
enough times to know that it ends with no clear winners (but plenty 
of losers).

Cheers,

Ken
-
Kenneth R. van Wyk
SC-L Moderator
KRvW Associates, LLC
http://www.KRvW.com








*
This communication, including attachments, is
for the exclusive use of addressee and may contain proprietary,
confidential and/or privileged information.  If you are not the intended
recipient, any use, copying, disclosure, dissemination or distribution is
strictly prohibited.  If you are not the intended recipient, please notify
the sender immediately by return e-mail, delete this communication and
destroy all copies.
*

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Harvard vs. von Neumann

[ljknews]

At 9:00 AM -0400 6/11/07, Gary McGraw wrote:

> If we assumed perfection at the implementation level (through better
> languages, say), then we would end up solving roughly 50% of the
> software security problem.
> 
> Clearly we need to make some progress at the architecture/design level
> to attain reasonable levels of software security.

> Perfect languages won't solve the software security problem.

And neither will perfect designs.

Both approaches needed.

But a large percentage of failures that result from weak languages are
already categorized in standard terms like "buffer overflow".
-- 
Larry Kilgallen
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Harvard vs. von Neumann

[der Mouse]

> What Turing actually tells us is that it is possible to construct
> programs that may be correct but whose correctness is not decidable.
> This is a far cry from saying that it is not possible to build
> well-structured programs whose correctness _is_ decidable.

True as far as it goes - but don't forget that you also haven't shown
the latter to be possible for programs of nontrivial size.

> The higher the level in which the human "codes", the [fewer] mistakes
> there are to be made, assuming equal familiarity with the language
> etc.

...but the more complex the "compiler", and the greater the likelihood
of bugs in it causing the resulting binary to fail to implement what
the human wrote.

> And you are just repeating the same fallacious proposition by saying
> "you cannot have total correctness".

It simply has not been formally established.  This does not make it
wrong, just unproven.  (Personally, I don't think it is wrong.)

> Had you instead said "you can never be sure that you have established
> that the requirements capture the users' needs", I would have had to
> agree with you.

That too.

There are three places where problems can appear: (1) the
specifications can express something other than what the users
want/need; (2) the coders can make mistakes translating those
specifications to code; (3) the translation from code to binary can
introduce bugs.  (No, step (2) cannot be eliminated; at most you can
push around who "the coders" are.  Writing specifications in a formal,
compilable language is just another form of programming.)

I don't think any of these steps can ever be rendered flawless, except
possibly when they are vacuous (as, for exmaple, step 3 is when coders
write in machine code).

>> People need to understand that programs are vastly more complex than
>> any other class of man made artifact ever, and there fore can never
>> achieve the reliability of, say, steam engines.
> Same old flawed proposition.

Same old *unproven* proposition.  Again, that doesn't make it wrong
(and, again, I don't think it *is* wrong).

>> We can never solve this problem. At best we can make it better.
> We can never solve the problem of being certain that we have got the
> requirements right.

We also can never solve the problem of being certain the conversion
from high-level language ("specifications", even) to executable code is
right, either.  Ultimately, everything comes down to "a lot of smart
people have looked at this and think it's right" - whether "this" is
code, a proof, prover software, whatever - and people make mistakes.

We're still finding bugs in C compilers.  Do you really think the
(vastly more complex) compilers for very-high-level specification
languages will be any better?

/~\ The ASCII   der Mouse
\ / Ribbon Campaign
 X  Against HTML   [EMAIL PROTECTED]
/ \ Email!   7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Harvard vs. von Neumann

[Gary McGraw]

Hi all,

Though I don't quite understand computer science theory in the same way that 
Crispin does, I do think it is worth pointing out that there are two major 
kinds of security defects in software: bugs at the implementation level, and 
flaws at the design/spec level.  I think Crispin is driving at that point.

If we assumed perfection at the implementation level (through better languages, 
say), then we would end up solving roughly 50% of the software security problem.

Clearly we need to make some progress at the architecture/design level to 
attain reasonable levels of software security.  I don't hold out much hope for 
formal approaches to design (though I continue to watch the UK types with 
interest).  Our approach to analysis and design at the architecture level at 
Cigital is ad hoc and based on experience, but it works.  (For more on that, 
see "Software Security" Chapter 5 which I think you can get a free copy of if 
you poke around here [registration required] 
http://searchsoftwarequality.techtarget.com/qna/0,289202,sid92_gci1187360,00.html.)

Perfect languages won't solve the software security problem.

gem

company www.cigital.com
podcast www.cigital.com/silverbullet
blog www.cigital.com/justiceleague
book www.swsec.com


-Original Message-
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Crispin Cowan
Sent: Monday, June 11, 2007 2:33 AM
To: Blue Boar
Cc: SC-L@securecoding.org
Subject: Re: [SC-L] Harvard vs. von Neumann

IMHO, all this hand wringing is for naught. To get systems that never
fail requires total correctness. Turing tells us that total correctness
is not decidable, so you simply never will get it completely, you will
only get approximations at best.

Having humans write specifications and leaving programming to computers
is similarly a lost cause. At a sufficiently high level, that is asking
the computer to map NP to P, and that isn't going to happen. At a less
abstract level, you are just asking the human to code in a higher level
language. This will help, but will not eliminate the problem that you
just cannot have total correctness.

Programmable Turing machines are great, they do wonderful things, but
total correctness for software simply isn't feasible. People need to
understand that programs are vastly more complex than any other class of
man made artifact ever, , and there fore can never achieve the
reliability of, say, steam engines.

The complexity of software is beginning to approach living organisms.
People at least understand that living things are not totally
predictable or reliable, and s**t will happen, and so you cannot count
on a critter or a plant to do exactly what you want. When computer
complexity clearly exceeds organism complexity, perhaps people will come
to recognize software for what it is; beyond definitive analyzability.

We can never solve this problem. At best we can make it better.

Crispin

--
Crispin Cowan, Ph.D.   http://crispincowan.com/~crispin/
Director of Software Engineering   http://novell.com
AppArmor Chat: irc.oftc.net/#apparmor

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Harvard vs. von Neumann

[David Crocker]

Crispin Cowen wrote:

>>
IMHO, all this hand wringing is for naught. To get systems that never fail
requires total correctness. Turing tells us that total correctness is not
decidable, so you simply never will get it completely, you will only get
approximations at best.
<<

What Turing actually tells us is that it is possible to construct programs that
may be correct but whose correctness is not decidable. This is a far cry from
saying that it is not possible to build well-structured programs whose
correctness _is_ decidable.

>>
Having humans write specifications and leaving programming to computers is
similarly a lost cause. At a sufficiently high level, that is asking the
computer to map NP to P, and that isn't going to happen.
<<

I don't understand what you are getting at here. If you are saying that humans
can map NP to P, but that it is impossible in principle to have computers do the
same thing, then that sounds like a religious argument to me. If you are saying
that you can write a specification that is unsatisfiable (or whose
satisfiability is undecidable) and that therefore cannot be implemented as code,
then this applies equally to human programmers. Incidentally, I have heard of a
few cases in which programming teams have wasted effort trying to implement sets
of requirements which, when the requirements were formalised, turned out to be
contradictory.

>>
At a less abstract level, you are just asking the human to code in a higher
level language. This will help, but will not eliminate the problem that you just
cannot have total correctness.
<<

The higher the level in which the human "codes", the less mistakes there are to
be made, assuming equal familiarity with the language etc. And you are just
repeating the same fallacious proposition by saying "you cannot have total
correctness". Had you instead said "you can never be sure that you have
established that the requirements capture the users' needs", I would have had to
agree with you.

>>
Programmable Turing machines are great, they do wonderful things, but total
correctness for software simply isn't feasible. People need to understand that
programs are vastly more complex than any other class of man made artifact ever,
, and there fore can never achieve the reliability of, say, steam engines.
<<

Same old flawed proposition. And, in software, the behaviour of the components
we build programs out of (i.e. machine instructions) are much more well-defined
and reliable than the materials that steam engines are built out of.

>>
The complexity of software is beginning to approach living organisms. People at
least understand that living things are not totally predictable or reliable, and
s**t will happen, and so you cannot count on a critter or a plant to do exactly
what you want. When computer complexity clearly exceeds organism complexity,
perhaps people will come to recognize software for what it is; beyond definitive
analyzability.
<<

Sure, if you develop a complex software system without a good design process
that carefully refines requirements to specifications to design to code - and
propagates changes in requirements down the chain too - then it may be
impossible to meaningfully analyse that software. That is why my approach is to
formalise requirements, write specifications that are proven to satisfy them,
then refine the specification to code - automatically where possible, but with
manual assistance where e.g. a data structure or an algorithm needs to be made
more efficient.

>>
We can never solve this problem. At best we can make it better.
<<

We can never solve the problem of being certain that we have got the
requirements right. I think that one implication for security is that there may
be whole new classes of threats out there that nobody has thought of yet, and
which we therefore can't refer to in the requirements. But we _can_ solve the
problem of ensuring that software meets the stated requirements, as long as
these are well-defined.

David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com




___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] What's the next tech problem to be solved in software

[Bennett, Jason]

Lots of interesting points been raised in thread so here a few points I've
picked out:

- It's the developer's fault: A few comments were made that the lack of
security lies at the door of the developers because they implement insecure
code. True to an extent but I don't think you can blame developers unless
they been educated in the first place. The situation here seems to be slowly
improving but is far from ideal. What I would like to see is more general
education and also more integration of technologies into the standard
low-level development environment that helps educate a developer into what
they are doing wrong. So explaining why it's wrong and secondly automating
the stopping of them doing it wrong. 
 
- The low-level problems have already been solved: I always find this
difficult as has been rightly pointed out the problem has been solved from a
technical point of view for some time now. Putting a 'finger in the air' you
might suppose that 95% of low-level problems (i.e. not inherent in the
design) would just disappear. Why doesn't this happen - difficult answer but
the inertia built up by certain languages and the developers is not
something that is going to change over night and vendors are going to start
producing the right 'tools' unless there is a demand for them from
developers. To borrow a phrase from someone else you don't get fired for
choosing C/C++ as your implementation language.   

- How to specify security: This I think is the biggest challenge facing
security at present. As has already been stated the low-level problems have
been solved but at the higher levels (requirements, design etc.) the
security arena makes the software development arena look advanced. We hardly
have the techniques of defining the security policy of a system and just as
importantly how are these integrated into the software development
life-cycle as part of it and not considered just an add on?

I don't have the answer to what the challenge is let alone how you achieve
it but how you express 'security' within a software design and how you make
this and integral part of the software design and implementation seem
fundamental in the stages to make software 'secure'. Some of the attempts I
have seen although interesting always seem to have the flaw in that they are
viewed as almost a separate process to the software development. There are
many technologies that a software developer takes as second nature as part
of their toolbox but security doesn't seem to be one that features highly.


Consider the environment before printing this mail.
"Thales e-Security Limited is incorporated in England and Wales with company
registration number 2518805. Its registered office is located at 2 Dashwood
Lang Road, The Bourne Business Park, Addlestone, Nr. Weybridge, Surrey KT15
2NX.
The information contained in this e-mail is confidential. It may also be
privileged. It is only intended for the stated addressee(s) and access to it
by any other person is unauthorised. If you are not an addressee or the
intended addressee, you must not disclose, copy, circulate or in any other
way use or rely on the information contained in this e-mail. Such
unauthorised use may be unlawful. If you have received this e-mail in error
please delete it (and all copies) from your system, please also inform us
immediately on +44 (0)1844 201800 or email [EMAIL PROTECTED]
Commercial matters detailed or referred to in this e-mail are subject to a
written contract signed for and on behalf of Thales e-Security Limited". 
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Harvard vs. von Neumann

[Crispin Cowan]

IMHO, all this hand wringing is for naught. To get systems that never
fail requires total correctness. Turing tells us that total correctness
is not decidable, so you simply never will get it completely, you will
only get approximations at best.

Having humans write specifications and leaving programming to computers
is similarly a lost cause. At a sufficiently high level, that is asking
the computer to map NP to P, and that isn't going to happen. At a less
abstract level, you are just asking the human to code in a higher level
language. This will help, but will not eliminate the problem that you
just cannot have total correctness.

Programmable Turing machines are great, they do wonderful things, but
total correctness for software simply isn't feasible. People need to
understand that programs are vastly more complex than any other class of
man made artifact ever, , and there fore can never achieve the
reliability of, say, steam engines.

The complexity of software is beginning to approach living organisms.
People at least understand that living things are not totally
predictable or reliable, and s**t will happen, and so you cannot count
on a critter or a plant to do exactly what you want. When computer
complexity clearly exceeds organism complexity, perhaps people will come
to recognize software for what it is; beyond definitive analyzability.

We can never solve this problem. At best we can make it better.

Crispin

-- 
Crispin Cowan, Ph.D.   http://crispincowan.com/~crispin/
Director of Software Engineering   http://novell.com
AppArmor Chat: irc.oftc.net/#apparmor

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Harvard vs. von Neumann

[der Mouse]

> Like it or not, the Web doesn't work right without Javascript now.

Depends on what you mean by "the Web" and "work right".  Fortunately,
for at least some people's values of those, this is not true.

/~\ The ASCII   der Mouse
\ / Ribbon Campaign
 X  Against HTML   [EMAIL PROTECTED]
/ \ Email!   7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B
___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___