Buffer overflow Article - CACM

Buffer overflow Article - CACM

[adaworks]

There is an interesting article in the current issue of the Communications
of the ACM (Vol 48, No 11, page 50) about preventing stack
buffer overflow attacks.   The authors, Kuperman, Brodley, Ozdoganoglu,
Viuakumar, and Jalote, write as if they have never heard of Ada.

In one paragraph, they criticize C as being vulnerable to such attacks
and then dismiss Pascal as being unable to address low-level issues.
As I read their solution, it became clear that simply choosing Ada for
their development language would solve the vast majority of their
concerns.

This kind of article appears every now and then. The authors of these
articles write as if it is necessary to improve C or invent new tools
when all they really have to do is discover Ada.

Richard Riehle

Re: Buffer overflow Article - CACM

[tmoran]

>In one paragraph, they criticize C as being vulnerable to such attacks
>and then dismiss Pascal as being unable to address low-level issues.
  They also say "the performance cost of bounds checking (reported in [the
'Cyclone' variant of C]) involves up to an additional 100% overhead."
I tried
      -- Lo, Hi, and A are procedure parameters, so their values
      -- and bounds are not known at compile time.
      for i in Lo .. Hi loop
        A(i) := 0;
      end loop;
with Gnat 3.15p with bounds checking on or off, -O2, and got a 65%
degradation, (Because the bounds are pushing the index out of a register?)
In the real world, my impression is that 10-15% is a more common cost of
all checking on vs all off.  Even at 65%, if the 20% of the code that
takes 80% of the time were hand checked and then compiled with checking
suppressed, 65% would change to 13% or about 3 months of CPU age by
Moore's law.

>This kind of article appears every now and then. The authors of these
>articles write as if it is necessary to improve C or invent new tools
>when all they really have to do is discover Ada.
  Sometimes one does feel like an observer watching a primitive tribe
do something the very hard way.  #.#

  They also quite fail to mention the x86's Bound instruction (does
anybody use it?) or descriptor architectures like the Burroughs machines
of 40 years ago.

Re: Buffer overflow Article - CACM

[Martin Krischik]

adaworks@sbcglobal.net wrote:

> There is an interesting article in the current issue of the Communications
> of the ACM (Vol 48, No 11, page 50) about preventing stack
> buffer overflow attacks.   The authors, Kuperman, Brodley, Ozdoganoglu,
> Viuakumar, and Jalote, write as if they have never heard of Ada.
> 
> In one paragraph, they criticize C as being vulnerable to such attacks
> and then dismiss Pascal as being unable to address low-level issues.
> As I read their solution, it became clear that simply choosing Ada for
> their development language would solve the vast majority of their
> concerns.
> 
> This kind of article appears every now and then. The authors of these
> articles write as if it is necessary to improve C or invent new tools
> when all they really have to do is discover Ada.

Is there an Online Version of that article? And if so: Would you mind if I
copy/paste your Text to /. - That's only of you have no /. user yourself.

Martin
-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Buffer overflow Article - CACM

[Georg Bauhaus]

Martin Krischik wrote:
 
> Is there an Online Version of that article? And if so: Would you mind if I
> copy/paste your Text to /. - That's only of you have no /. user yourself.

http://doi.acm.org/10.1145/1096000.1096004

The authors refer you to their site, in the final sentence of
their article. If you look at their "front page", the motivation of
their analyses will become clear. Please tr -d ' ' in
w w w . s m a s h  gu a r d .  or g

Some quotes:

"One way to prevent programs from having such vulnerabilities is
to write them using a language (such as Java or Pascal) that performs
bound checking. However, such languages often lack the low-level data
manipulation needed by some applications. Therefore, researchers have
produced "more secure" versions of C that are mostly compatible with
existing programs but add additional security features. Cyclone [5]
is one such C-language variant. Unfortunately, the performance cost
of bounds checking (reported in [5]) involves up to an additional
100% overhead."

"Dynamic protection techniques can be costly in terms of overhead,
but some researchers are trying to move that functionality into faster,
hardware-based protection schemes.
As these techniques move from academic laboratories into mainstream
software releases, computer users and software developers have become
aware of what they can do, and what they can't do."

Re: Buffer overflow Article - CACM

[Florian Weimer]

* Georg Bauhaus:

> http://doi.acm.org/10.1145/1096000.1096004
>
> The authors refer you to their site, in the final sentence of
> their article. If you look at their "front page", the motivation of
> their analyses will become clear. Please tr -d ' ' in
> w w w . s m a s h  gu a r d .  or g
>
> Some quotes:
>
> "One way to prevent programs from having such vulnerabilities is
> to write them using a language (such as Java or Pascal) that performs
> bound checking. However, such languages often lack the low-level data
> manipulation needed by some applications. Therefore, researchers have
> produced "more secure" versions of C that are mostly compatible with
> existing programs but add additional security features. Cyclone [5]
> is one such C-language variant. Unfortunately, the performance cost
> of bounds checking (reported in [5]) involves up to an additional
> 100% overhead."

The tables in that paper do not justify the 100% figure, and the paper
shows that some of the programs were incorrect, presumably because the
authors failed to include run-time bounds checks.  The "fat pointer"
approach used by Cyclone is not representative of typical compiler
implementations of bounds-checked array types, either.

> "Dynamic protection techniques can be costly in terms of overhead,

Yeah, sure.  Bounds checks are costly, so lets get rid of them and
just use obfuscation techniques to prevent code injection.  The truth
is that you have to check things at some point, and manually coded
bounds checks have been shown to be error-prone (more than
compiler-generated ones).  For most applications implicit bounds
checks are probably a win.

The authors show a profound lack of industry experience.  In
real-world Internet applications, a typical non-exploitable buffer
overflow is still a very serious defect because it affects
availability.  Shifting bugs from crash-and-control to crash-only
isn't such a tremendous improvement, especially in environments which
use multi-threading instead of multiple cooperating (but isolated)
processes.

Re: Buffer overflow Article - CACM

[Marc A. Criley]

Florian Weimer wrote:

> The authors show a profound lack of industry experience.

Said observation being one of the reasons I periodically hurl flaming 
abuse at CACM, and don't shy away from doing so in the reader surveys 
they occasionally distribute.

ACM Queue, on the other hand, is everything that CACM is not: 
interesting, thought-provoking, and relevant.

-- Marc A. Criley
-- McKae Technologies
-- www.mckae.com
-- DTraq - XPath In Ada - XML EZ Out

Re: Buffer overflow Article - CACM

[Martin Krischik]

Georg Bauhaus wrote:

> Martin Krischik wrote:
>  
>> Is there an Online Version of that article? And if so: Would you mind if
>> I copy/paste your Text to /. - That's only of you have no /. user
>> yourself.
 
> http://doi.acm.org/10.1145/1096000.1096004

Ahh, but you have to buy the article or be an subscriber :-( .

Martin

-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Buffer overflow Article - CACM

[Florian Weimer]

> In one paragraph, they criticize C as being vulnerable to such attacks
> and then dismiss Pascal as being unable to address low-level issues.
> As I read their solution, it became clear that simply choosing Ada for
> their development language would solve the vast majority of their
> concerns.

I doubt it.  Ada compilers are not designed to be secure in that
sense, and there doesn't appear to be any commercial interest to
change this.  The needs of typical safety-critical software are
completely different, and they do not help much with writing secure
code (in the "buffer overflow" sense).

Re: Buffer overflow Article - CACM

[Stephen Leake]

<adaworks@sbcglobal.net> writes:

> There is an interesting article in the current issue of the Communications
> of the ACM (Vol 48, No 11, page 50) about preventing stack
> buffer overflow attacks.   The authors, Kuperman, Brodley, Ozdoganoglu,
> Viuakumar, and Jalote, write as if they have never heard of Ada.
>
> In one paragraph, they criticize C as being vulnerable to such attacks
> and then dismiss Pascal as being unable to address low-level issues.
> As I read their solution, it became clear that simply choosing Ada for
> their development language would solve the vast majority of their
> concerns.
>
> This kind of article appears every now and then. The authors of these
> articles write as if it is necessary to improve C or invent new tools
> when all they really have to do is discover Ada.

I hope you wrote to the editor of CACM pointing out this flaw in the
article. It is up to the editor to ensure that articles are fair and
balanced! And they won't know there's a problem if nobody tells them.

There have been similar problems with articles in Dr Dobbs; the editor
has been quite gracious when I point them out. We'll have to see if
that translates into more balanced coverage in the future ...

On the other hand, I don't read CACM any more, because the articles
are so poor in general. Well, except for the legal column by Pamela
Samuelson (if I've got her name right).

-- 
-- Stephe

Re: Buffer overflow Article - CACM

[adaworks]

"Stephen Leake" <stephen_leake@acm.org> wrote in message
news:uiruwwo04.fsf@acm.org...
>
> I hope you wrote to the editor of CACM pointing out this flaw in the
> article. It is up to the editor to ensure that articles are fair and
> balanced! And they won't know there's a problem if nobody tells them.
>
I did not contact CACM.  Rather, I contacted the principal author and
informed him about this thread. Perhaps he, or one of the other authors
will find the time to post a note in this forum.
>
Further, given that their complaint was primarily focused on the languages
they do know instead of those they don't, I think the article is well-reasoned.
The problem, as I see it, is that so many academics spend so much time
solving problems while existing solutions are either ignored or unknown
to them.
>
> There have been similar problems with articles in Dr Dobbs; the editor
> has been quite gracious when I point them out. We'll have to see if
> that translates into more balanced coverage in the future ...
>
The editor of Dr. Dobbs has a long-standing invitation for articles that
describe, in depth and in detail, problems that have been solved in Ada
that could not have been just as easily solved in some other language.
Further, if someone wants to write an article about Ada 2005, I think
Dr. Dobbs will print it -- given that it is a well-written article.
>
Richard Riehle

Re: Buffer overflow Article - CACM

[Jeffrey R. Carter]

adaworks@sbcglobal.net wrote:
> There is an interesting article in the current issue of the Communications
> of the ACM (Vol 48, No 11, page 50) about preventing stack
> buffer overflow attacks.   The authors, Kuperman, Brodley, Ozdoganoglu,
> Viuakumar, and Jalote, write as if they have never heard of Ada.

I found the article quite amusing.

> In one paragraph, they criticize C as being vulnerable to such attacks
> and then dismiss Pascal as being unable to address low-level issues.
> As I read their solution, it became clear that simply choosing Ada for
> their development language would solve the vast majority of their
> concerns.

This was also the ONLY paragraph that addressed language choice in the entire 
article. Considering that language choice is the cause of buffer overflow 
vulnerabilities, you'll understand why I found the article amusing.

1st, they say languages such as Java and Pascal may not be low level enough. 
That's certainly not true of Ada, nor of most versions of Modula-2 and Pascal. 
So this is simply hand waving to justify their decision to use a C derivative.

Then they say that bounds checking adds 100% overhead. This may be true of 
trying to patch C, but it's certainly not true of all the checks Ada does, which 
is much more than simply bounds checking. In practice I have never found a case 
in which leaving checks in was too slow, nor where turning them off saved more 
than 10%.

-- 
Jeff Carter
"C++ is like giving an AK-47 to a monk, shooting him
full of crack and letting him loose in a mall and
expecting him to balance your checking account
'when he has the time.'"
Drew Olbrich
52

Re: Buffer overflow Article - CACM

[Martin Dowie]

Jeffrey R. Carter wrote:
> Then they say that bounds checking adds 100% overhead. This may be true 
> of trying to patch C, but it's certainly not true of all the checks Ada 
> does, which is much more than simply bounds checking. In practice I have 
> never found a case in which leaving checks in was too slow, nor where 
> turning them off saved more than 10%.

That's probably true now but there are loads of examples where running 
_Ada83_ on 68020/68040 with checks-on was too slow.

Cheers

-- Martin

Re: Buffer overflow Article - CACM

[Jeffrey R. Carter]

Martin Dowie wrote:
> 
> That's probably true now but there are loads of examples where running 
> _Ada83_ on 68020/68040 with checks-on was too slow.

No doubt. However, I've been using Ada since 1984 and have never encountered a 
case where the checks made the difference between success and failure in meeting 
  timing requirements.

-- 
Jeff Carter
"C++ is like giving an AK-47 to a monk, shooting him
full of crack and letting him loose in a mall and
expecting him to balance your checking account
'when he has the time.'"
Drew Olbrich
52

Re: Buffer overflow Article - CACM

[Martin Dowie]

Jeffrey R. Carter wrote:
> Martin Dowie wrote:
>>
>> That's probably true now but there are loads of examples where
>> running _Ada83_ on 68020/68040 with checks-on was too slow.
>
> No doubt. However, I've been using Ada since 1984 and have never
> encountered a case where the checks made the difference between
>   success and failure in meeting timing requirements.

Wish I could say the same! :-(

Re: Buffer overflow Article - CACM

[Pascal Obry]

Jeffrey,

> Then they say that bounds checking adds 100% overhead. This may be true
> of trying to patch C, but it's certainly not true of all the checks Ada
> does, which is much more than simply bounds checking. In practice I have
> never found a case in which leaving checks in was too slow, nor where
> turning them off saved more than 10%.

Probably because Ada can remove some checks at runtime. See recent
thread on the subject. I think this really depends on your programming
style, if your applications defines lot of types with appropriate
constraints, it will help the compiler optimize away the checks.

And then even if there was 100% overhead, what the problem ? For most
applications this is not critical and at least for debugging the
application this is invaluable. Running with a 100% overhead is
equivalent to running with a computer 18 months old. Not that bad :)
Again I understand that in some domains we are counting the CPU cycles,
but this is not the majority of applications.

Pascal.

-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|              http://www.obry.net
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver wwwkeys.pgp.net --recv-key C1082595

Re: Buffer overflow Article - CACM

[Dmitry A. Kazakov]

On Mon, 14 Nov 2005 08:09:04 +0100, Pascal Obry wrote:

>> Then they say that bounds checking adds 100% overhead. This may be true
>> of trying to patch C, but it's certainly not true of all the checks Ada
>> does, which is much more than simply bounds checking. In practice I have
>> never found a case in which leaving checks in was too slow, nor where
>> turning them off saved more than 10%.
> 
> And then even if there was 100% overhead, what the problem ? For most
> applications this is not critical and at least for debugging the
> application this is invaluable. Running with a 100% overhead is
> equivalent to running with a computer 18 months old. Not that bad :)
> Again I understand that in some domains we are counting the CPU cycles,
> but this is not the majority of applications.

This is not the whole truth. I agree that overhead caused by run-time
checks is not a big deal. But that is not the problem in my view. Let they
be 0%! The real problem is that a check may fail while program crash is not
an option. This means that there must be some error handling. More errors
may happen at run-time more complex infrastructure one would require. Add
here unit tests for these errors etc.

It is a design problem and design problems are in order of magnitude more
expensive than any hardware.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Buffer overflow Article - CACM

[Simon Wright]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> This is not the whole truth. I agree that overhead caused by
> run-time checks is not a big deal. But that is not the problem in my
> view. Let they be 0%! The real problem is that a check may fail
> while program crash is not an option. This means that there must be
> some error handling. More errors may happen at run-time more complex
> infrastructure one would require. Add here unit tests for these
> errors etc.

For information -- is your point that we should design the program
(using eg SPARK) so that there isn't any need for runtime checking?
(I don't think it likely that you want us not to bother to do any
checking!)

Re: Buffer overflow Article - CACM

[Dmitry A. Kazakov]

On Mon, 14 Nov 2005 20:57:40 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> This is not the whole truth. I agree that overhead caused by
>> run-time checks is not a big deal. But that is not the problem in my
>> view. Let they be 0%! The real problem is that a check may fail
>> while program crash is not an option. This means that there must be
>> some error handling. More errors may happen at run-time more complex
>> infrastructure one would require. Add here unit tests for these
>> errors etc.
> 
> For information -- is your point that we should design the program
> (using eg SPARK) so that there isn't any need for runtime checking?

Yes, when possible.

> (I don't think it likely that you want us not to bother to do any
> checking!)

We should draw line between "functional" and "non-functional" checks. When
checks is an artefact of program/language/environment design then its
penalty is more than just run-time overhead. Of course the distinction is
not absolute. For example End_Error might look functional, but probably in
a better OS with OO interface you will never have it working with a string
container, XML document rather than with a raw byte stream. Buffer overflow
checks is a clear "non-functional" candidate to me. This is also a reason
why I'm skeptical about the design of Unbounded_String and Ada.Container.
They don't support safe iteration constructs "for I in X'Range loop".

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Buffer overflow Article - CACM

[Georg Bauhaus]

Dmitry A. Kazakov wrote:

> Ada.Container.
> They don't support safe iteration constructs "for I in X'Range loop".
> 

Ada.Container does provide safe iteration construct, be
suitably defining and/or suggesting what is meant by "safe".

OTOH, for I in X'Range loop alone doesn't imply that
iteration will be safe.

Re: Buffer overflow Article - CACM

[Dmitry A. Kazakov]

On Tue, 15 Nov 2005 15:03:11 +0100, Georg Bauhaus wrote:

> Dmitry A. Kazakov wrote:
> 
>> Ada.Container.
>> They don't support safe iteration constructs "for I in X'Range loop".
> 
> Ada.Container does provide safe iteration construct, be
> suitably defining and/or suggesting what is meant by "safe".
>
> OTOH, for I in X'Range loop alone doesn't imply that
> iteration will be safe.

As you said, it depends on the definition. Clearly it isn't safe against
shelling the computer.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Buffer overflow Article - CACM

[Georg Bauhaus]

Dmitry A. Kazakov wrote:
> On Tue, 15 Nov 2005 15:03:11 +0100, Georg Bauhaus wrote:
> 
> 
>>Dmitry A. Kazakov wrote:
>>
>>
>>>Ada.Container.
>>>They don't support safe iteration constructs "for I in X'Range loop".
>>
>>Ada.Container does provide safe iteration construct, be
>>suitably defining and/or suggesting what is meant by "safe".
>>
>>OTOH, for I in X'Range loop alone doesn't imply that
>>iteration will be safe.
> 
> 
> As you said, it depends on the definition. Clearly it isn't safe against
> shelling the computer.
> 

For sure you can get Constrain_Error using the library,
and this isn't alwas pleasant. Yet, in which ways is any of the
following more safe than the other?

   for I in X'Range loop
      Modify_Element(X(I));
   end loop;

   Iterate(X, Modify_Element'Access);

Re: Buffer overflow Article - CACM

[Robert A Duff]

Georg Bauhaus <bauhaus@futureapps.de> writes:

> For sure you can get Constrain_Error using the library,
> and this isn't alwas pleasant. Yet, in which ways is any of the
> following more safe than the other?
> 
>    for I in X'Range loop
>       Modify_Element(X(I));
>    end loop;
> 
>    Iterate(X, Modify_Element'Access);

I'd say the second is less error-prone.  You can't accidentally type
X(J) or B(I) -- the extraneous and irrelevant "I" is not present in the
second example, which is a good thing.  It seems silly in a small
example, but if the loop had a dozen or more lines of code,
or were nested inside another loop, well....

- Bob

Re: Buffer overflow Article - CACM

[Dmitry A. Kazakov]

On Tue, 15 Nov 2005 23:32:37 +0100, Georg Bauhaus wrote:

> Dmitry A. Kazakov wrote:
>> On Tue, 15 Nov 2005 15:03:11 +0100, Georg Bauhaus wrote:
>> 
>>>Dmitry A. Kazakov wrote:
>>>
>>>>Ada.Container.
>>>>They don't support safe iteration constructs "for I in X'Range loop".
>>>
>>>Ada.Container does provide safe iteration construct, be
>>>suitably defining and/or suggesting what is meant by "safe".
>>>
>>>OTOH, for I in X'Range loop alone doesn't imply that
>>>iteration will be safe.
>> 
>> As you said, it depends on the definition. Clearly it isn't safe against
>> shelling the computer.
> 
> For sure you can get Constrain_Error using the library,
> and this isn't alwas pleasant. Yet, in which ways is any of the
> following more safe than the other?
> 
>    for I in X'Range loop
>       Modify_Element(X(I));
>    end loop;
> 
>    Iterate(X, Modify_Element'Access);

You are comparing apples and oranges. The first is a language construct,
the second is a call to procedure. They could be made comparable if Ada had
subroutines as first class objects:

   Iterate (X, procedure (E : in out Element_Type) is begin ... end);

Or at least:

   Iterate (X, Modify_Element);

But that is aside. What would you say about the same written in Assembly:

MOV $Modify_Element, R1
MOV $X, R2
JMP $Iterate   ; Isn't this safe?

The question is not how iteration and element processing are composed:
using procedural decomposition or language constructs. The question is how
iteration is expressed. These are not directly related issues and there is
not much choice here: loop vs. recursion.

Note also that your example is based on a trick. You bring a black horse
Modify_Element into consideration. Nothing is known about it. So whatever
the enclosing construct does and how it does this, safety is 0.

As for Robert's note about explicit indices, it would be nice to have

   for E in X loop ...

for array types as well. I think it would be quite easy to implement in an
Ada compiler.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Buffer overflow Article - CACM

[adaworks]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:1wclw5pmb787b$.1srcn4xk9xxr5.dlg@40tude.net...
>
> As for Robert's note about explicit indices, it would be nice to have
>
>    for E in X loop ...
>
You are correct.  Consider,

     procedure Array_Loop is
          type Index is range 1..10;
          X : array (Index) of Integer;
    begin
          for I in Index loop
             null;
         end loop;
    end Array_Loop;

No overflow.  No indexing off the end of the array.   Easy to
compose.   Easy to read.    As for X'Range, I have never seen
a case where it ran off the end of an array.   In any case, once my
program, as shown above, is compiled and linked, it would
be diffcult for an attacker to exploit it.

Richard Riehle

Re: Buffer overflow Article - CACM

[Martin Dowie]

adaworks@sbcglobal.net wrote:
> You are correct.  Consider,
>
>      procedure Array_Loop is
>           type Index is range 1..10;
>           X : array (Index) of Integer;
>     begin
>           for I in Index loop
>              null;
>          end loop;
>     end Array_Loop;
>
> No overflow.  No indexing off the end of the array.   Easy to
> compose.   Easy to read.    As for X'Range, I have never seen
> a case where it ran off the end of an array.   In any case, once my
> program, as shown above, is compiled and linked, it would
> be diffcult for an attacker to exploit it.

The problem with the above example is that there are compilers that will
_not_ remove superfluous checks, e.g. if the "null;" was instead "Y := X
(I);". Change "for I in Index loop" to "for I in X'Range loop" and the
checks go...

Re: Buffer overflow Article - CACM

[Jeffrey R. Carter]

Pascal Obry wrote:

> And then even if there was 100% overhead, what the problem ? For most
> applications this is not critical and at least for debugging the
> application this is invaluable. Running with a 100% overhead is
> equivalent to running with a computer 18 months old. Not that bad :)
> Again I understand that in some domains we are counting the CPU cycles,
> but this is not the majority of applications.

Even in cases where it is critical, how fast does an incorrect program have to 
be in order to be acceptable? If a really fast, incorrect program is better than 
a slow, correct program, then I submit the following as the solution to all 
problems:

procedure Solution is
    -- null;
begin -- Solution
    null;
end Solution;

Compile with all checks suppressed for maximum acceptability.

-- 
Jeff Carter
"C++ is like giving an AK-47 to a monk, shooting him
full of crack and letting him loose in a mall and
expecting him to balance your checking account
'when he has the time.'"
Drew Olbrich
52

Re: Buffer overflow Article - CACM

[Larry Kilgallen]

In article <0f4ef.1413$s14.1261@newsread2.news.pas.earthlink.net>, "Jeffrey R. Carter" <spam@spam.com> writes:

> Even in cases where it is critical, how fast does an incorrect program have to 
> be in order to be acceptable? If a really fast, incorrect program is better than 
> a slow, correct program,

Well, the slow correct program must run quickly enough to beat the
Mean Time Between Failure of the hardware.  Otherwise it is not
actually producing a correct answer.

Re: Buffer overflow Article - CACM

[Christopher Browne]

> Pascal Obry wrote:
>
>> And then even if there was 100% overhead, what the problem ? For most
>> applications this is not critical and at least for debugging the
>> application this is invaluable. Running with a 100% overhead is
>> equivalent to running with a computer 18 months old. Not that bad :)
>> Again I understand that in some domains we are counting the CPU cycles,
>> but this is not the majority of applications.
>
> Even in cases where it is critical, how fast does an incorrect program
> have to be in order to be acceptable? If a really fast, incorrect
> program is better than a slow, correct program, then I submit the
> following as the solution to all problems:
>
> procedure Solution is
>     -- null;
> begin -- Solution
>     null;
> end Solution;
>
> Compile with all checks suppressed for maximum acceptability.

Reality does *NOT* lie there.

Something that is only approximately correct but that is super-fast
may, in cases where time or computational effort *are* at a premium,
be preferable to a slower "correct all the time" program.

The trouble with formal verification methods is that they consume time
(for the analysis work) when you may well discover that the problem
wasn't specified well enough in the first place for formal
verification to actually do any material good.

Having super-well-specified problems is extremely necessary when doing
"rocket science;" if it costs $1B to fire off a rocket, and you don't
get a second chance, it's necessary to do whatever up-front effort is
required to make sure the problem is super-well-specified.

But there are a lot of cases where that level of effort is not
warranted, and it's NOT worth getting "super-detailed, super-correct"
specifications, and it's NOT worth various of the efforts.

Where the CACM article has some things *right* is that there are
plenty of systems where it would be way too costly to reimplement them
in a buffer-overflow-immune language.  People are not going to redo
everything in PL/1 or Ada just because they have better specified
string types.  They don't have time.
-- 
(format nil "~S@~S" "cbbrowne" "ntlug.org")
http://cbbrowne.com/info/linuxdistributions.html
Rules of the Evil Overlord  #220. "Whatever my one vulnerability is, I
will fake a  different one. For example, ordering  all mirrors removed
from the palace, screaming and flinching whenever someone accidentally
holds up a mirror, etc. In the climax when the hero whips out a mirror
and thrusts it at my face,  my reaction will be ``Hmm...I think I need
a shave.''"  <http://www.eviloverlord.com/>

Re: Buffer overflow Article - CACM

[Jeffrey R. Carter]

Christopher Browne wrote:

> Where the CACM article has some things *right* is that there are
> plenty of systems where it would be way too costly to reimplement them
> in a buffer-overflow-immune language.  People are not going to redo
> everything in PL/1 or Ada just because they have better specified
> string types.  They don't have time.

Good point, if they're willing to pay for the losses of others whose systems are 
hijacked because of buffer-overflow errors injected by their poor language 
choices. If that were required, I suspect they would suddenly have time.

-- 
Jeff Carter
"Alms for an ex-leper!"
Monty Python's Life of Brian
75

Re: Buffer overflow Article - CACM

[adaworks]

"Christopher Browne" <cbbrowne@acm.org> wrote in message
news:m3psop8e45.fsf@mobile.int.cbbrowne.com...
>
> Where the CACM article has some things *right* is that there are
> plenty of systems where it would be way too costly to reimplement them
> in a buffer-overflow-immune language.  People are not going to redo
> everything in PL/1 or Ada just because they have better specified
> string types.  They don't have time.
> -- 
I am reminded of the well-known comment that "We always have time to
do it over but never time to do it right."

In the case of Ada, there is no need to "redo everything."   The language is
rather friendly to other languages.    As for PL/I, there are entirely too many
other problems with that language to use it for dependable software.

Richard Riehle

Re: Buffer overflow Article - CACM

[Simon Clubley]

In article <5Fpif.25167$Zv5.13092@newssvr25.news.prodigy.net>, <adaworks@sbcglobal.net> writes:
> 
> In the case of Ada, there is no need to "redo everything."   The language is
> rather friendly to other languages.
> 

Of course, with some of those other languages, you (or more accurately your
Ada programs) are no longer in control if code written in that language
trashes the address space allocated to your Ada code due to a programming bug.

This is something that I am currently very aware of while designing a current
project...

Simon.

-- 
Simon Clubley, clubley@remove_me.eisner.decus.org-Earth.UFP       
Scientific Theory: A testable hypothesis that is supported by a body of evidence

Re: Buffer overflow Article - CACM

[robin]

adaworks@sbcglobal.net wrote in message <5Fpif.25167$Zv5.13092@newssvr25.news.prodigy.net>...
>
>"Christopher Browne" <cbbrowne@acm.org> wrote in message
>news:m3psop8e45.fsf@mobile.int.cbbrowne.com...
>>
>> Where the CACM article has some things *right* is that there are
>> plenty of systems where it would be way too costly to reimplement them
>> in a buffer-overflow-immune language.  People are not going to redo
>> everything in PL/1 or Ada just because they have better specified
>> string types.  They don't have time.
>> --
>I am reminded of the well-known comment that "We always have time to
>do it over but never time to do it right."
>
>In the case of Ada, there is no need to "redo everything."   The language is
>rather friendly to other languages.    As for PL/I, there are entirely too many
>other problems with that language to use it for dependable software.


What you say is not true; PL/I is perfectly capable, reliable,
and robust for all kinds of projects, including real-time projects,
just as Ada is.
As well, PL/I interfaces to other languages.

>Richard Riehle

Re: Buffer overflow Article - CACM

[adaworks]

"robin" <robin_v@bigpond.com> wrote in message
news:6ktjf.8048$ea6.3571@news-server.bigpond.net.au...
>
> What you say is not true; PL/I is perfectly capable, reliable,
> and robust for all kinds of projects, including real-time projects,
> just as Ada is.
> As well, PL/I interfaces to other languages.
>
Sorry Robin but PL/I is simply not up to the level of reliability
and capability as you might think it is.

It was a nice attempt when it was first designed, but it has been
surpassed by new languages.  The exception handling model is
inadequate,  simple things such as getting out of a loop require
dangerous statements,  and lots of other things that simply fall
short of what one would expect of a more robust language
design.

Richard Riehle

Re: Buffer overflow Article - CACM

[robin]

adaworks@sbcglobal.net wrote in message ...
>
>"robin" <robin_v@bigpond.com> wrote in message
>news:6ktjf.8048$ea6.3571@news-server.bigpond.net.au...
>>
>> What you say is not true; PL/I is perfectly capable, reliable,
>> and robust for all kinds of projects, including real-time projects,
>> just as Ada is.
>> As well, PL/I interfaces to other languages.
>>
>Sorry Robin but PL/I is simply not up to the level of reliability
>and capability as you might think it is.

Indeed it is both capable and reliable, and then some.

>It was a nice attempt when it was first designed, but it has been
>surpassed by new languages.

You seem to be unaware that PL/I has evolved since
it was "first designed".

>  The exception handling model is
>inadequate,

Exception handling is excellent, as is the model.

>  simple things such as getting out of a loop require
>dangerous statements,

You're talking rot.

>  and lots of other things that simply fall
>short of what one would expect of a more robust language
>design.

You really don't know what you are talking about.

>Richard Riehle

Re: Buffer overflow Article - CACM

[adaworks]

"robin" <robin_v@bigpond.com> wrote in message
news:9hhkf.10004$ea6.5952@news-server.bigpond.net.au...
>
> You seem to be unaware that PL/I has evolved since
> it was "first designed".
>
It would have to have evolved quite a lot to be anywhere
close to the capabilities or reliability of a language such as Ada.

Perhaps you can provide a reference to some resources that
would help us enlighten ourselves.

Richard Riehle

Re: Buffer overflow Article - CACM

[robin]

<adaworks@sbcglobal.net> wrote in message
news:3klkf.25509$dO2.19240@newssvr29.news.prodigy.net...
>
> "robin" <robin_v@bigpond.com> wrote in message
> news:9hhkf.10004$ea6.5952@news-server.bigpond.net.au...
> >
> > You seem to be unaware that PL/I has evolved since
> > it was "first designed".
> >
> It would have to have evolved quite a lot to be anywhere
> close to the capabilities or reliability of a language such as Ada.

Then this may interest you.  It's part of the source to the
PL/I compiler (which is compiled).

MATRIX (
   GET (A);
   GET (B);
   C = A x B;
   PUT ('Matrix multiplication of A by B yields:');
   PRINT (C, 8);

   F = M random N;
   PRINT (F, 7);
   G = N random M;
   print (g, 8);
   H = F dot_prod G;
   put ('dot product=');
   print (h, 8);
);
END;

> Perhaps you can provide a reference to some resources that
> would help us enlighten ourselves.

IBM VA PL/I for Windows Language Reference.

> Richard Riehle

Re: Buffer overflow Article - CACM

[robin]

<adaworks@sbcglobal.net> wrote in message
news:3klkf.25509$dO2.19240@newssvr29.news.prodigy.net...
>
> "robin" <robin_v@bigpond.com> wrote in message
> news:9hhkf.10004$ea6.5952@news-server.bigpond.net.au...
> >
> > You seem to be unaware that PL/I has evolved since
> > it was "first designed".
> >
> It would have to have evolved quite a lot to be anywhere
> close to the capabilities or reliability of a language such as Ada.
>
> Perhaps you can provide a reference to some resources that
> would help us enlighten ourselves.

Here's another example (I notice that you did not respond
to the previous example):

PL/I can compile and execute the following source.  Can Ada do the same for
PL/I?

Mixed: procedure options (main);
    ...
ADA(
StringReverse (S: Text) return Text is
begin
    if Length(S) <= 1
       then return S;
       else return StringReverse(Tail(S)) & Head(S);
end StringReverse;
);
end mixed;

[I have not written here the PL/I code for TAIL and HEAD,
nor the declarations for the variables corresponding
to S and Text.]

Re: Buffer overflow Article - CACM

[Georg Bauhaus]

On Sat, 2005-12-31 at 07:39 +0000, robin wrote:
> <adaworks@sbcglobal.net> wrote in message
> news:3klkf.25509$dO2.19240@newssvr29.news.prodigy.net...
> >
> > "robin" <robin_v@bigpond.com> wrote in message
> > news:9hhkf.10004$ea6.5952@news-server.bigpond.net.au...
> > >
> > > You seem to be unaware that PL/I has evolved since
> > > it was "first designed".
> > >
> > It would have to have evolved quite a lot to be anywhere
> > close to the capabilities or reliability of a language such as Ada.
> >
> > Perhaps you can provide a reference to some resources that
> > would help us enlighten ourselves.
> 
> Here's another example 

I've found the earlier references (to IBM's PL/1 e.g.) more
informative in that they show what is available with recent
PL/1s. Have you had a look at Ada, for comparison?


-- Georg 

Re: Buffer overflow Article - CACM

[Martin Krischik]

robin wrote:

> <adaworks@sbcglobal.net> wrote in message
> news:3klkf.25509$dO2.19240@newssvr29.news.prodigy.net...
>>
>> "robin" <robin_v@bigpond.com> wrote in message
>> news:9hhkf.10004$ea6.5952@news-server.bigpond.net.au...
>> >
>> > You seem to be unaware that PL/I has evolved since
>> > it was "first designed".
>> >
>> It would have to have evolved quite a lot to be anywhere
>> close to the capabilities or reliability of a language such as Ada.
>>
>> Perhaps you can provide a reference to some resources that
>> would help us enlighten ourselves.
> 
> Here's another example (I notice that you did not respond
> to the previous example):
> 
> PL/I can compile and execute the following source.  Can Ada do the same
> for PL/I?
> 
> Mixed: procedure options (main);
>     ...
> ADA(
> StringReverse (S: Text) return Text is
> begin
>     if Length(S) <= 1
>        then return S;
>        else return StringReverse(Tail(S)) & Head(S);
> end StringReverse;
> );
> end mixed;
> 
> [I have not written here the PL/I code for TAIL and HEAD,
> nor the declarations for the variables corresponding
> to S and Text.]

From the top of my head

package PL_1

  function String_Reverse (S : in String) return String is
  begin
     if S'Lenght <= 1 then
       return S;
     else
       return String_Reverse (Tail(S)) & Head(S);
     end if
  end String_Reverse;
end PL_1;

Almost identical - so what's you point then.

Martin

-- 
mailto://krischik@users.sourceforge.net
Ada programming at: http://ada.krischik.com

Re: Buffer overflow Article - CACM

[robin]

"Martin Krischik" <krischik@users.sourceforge.net> wrote in message
news:4626568.XPZCFmT196@linux1.krischik.com...
> robin wrote:
>
> > <adaworks@sbcglobal.net> wrote in message
> > news:3klkf.25509$dO2.19240@newssvr29.news.prodigy.net...
> >>
> >> "robin" <robin_v@bigpond.com> wrote in message
> >> news:9hhkf.10004$ea6.5952@news-server.bigpond.net.au...
> >> >
> >> > You seem to be unaware that PL/I has evolved since
> >> > it was "first designed".
> >> >
> >> It would have to have evolved quite a lot to be anywhere
> >> close to the capabilities or reliability of a language such as Ada.
> >>
> >> Perhaps you can provide a reference to some resources that
> >> would help us enlighten ourselves.
> >
> > Here's another example (I notice that you did not respond
> > to the previous example):
> >
> > PL/I can compile and execute the following source.  Can Ada do the same
> > for PL/I?
> >
> > Mixed: procedure options (main);
> >     ...
> > ADA(
> > StringReverse (S: Text) return Text is
> > begin
> >     if Length(S) <= 1
> >        then return S;
> >        else return StringReverse(Tail(S)) & Head(S);
> > end StringReverse;
> > );
> > end mixed;
> >
> > [I have not written here the PL/I code for TAIL and HEAD,
> > nor the declarations for the variables corresponding
> > to S and Text.]
>
> From the top of my head
>
> package PL_1
>
>   function String_Reverse (S : in String) return String is
>   begin
>      if S'Lenght <= 1 then
>        return S;
>      else
>        return String_Reverse (Tail(S)) & Head(S);
>      end if
>   end String_Reverse;
> end PL_1;

This is Ada code, not PL/I code.  I already supplied
Ada code in the PL/I source example above.

> Almost identical - so what's you point then.

The point is that Ada code can be compiled direct by a
PL/I compiler.

Re: Buffer overflow Article - CACM

[jimmaureenrogers]

robin wrote:
> "Martin Krischik" <krischik@users.sourceforge.net> wrote in message
> news:4626568.XPZCFmT196@linux1.krischik.com...

> > > PL/I can compile and execute the following source.  Can Ada do the same
> > > for PL/I?
> > >
> > > Mixed: procedure options (main);
> > >     ...
> > > ADA(
> > > StringReverse (S: Text) return Text is
> > > begin
> > >     if Length(S) <= 1
> > >        then return S;
> > >        else return StringReverse(Tail(S)) & Head(S);
> > > end StringReverse;
> > > );
> > > end mixed;
> > >
> > > [I have not written here the PL/I code for TAIL and HEAD,
> > > nor the declarations for the variables corresponding
> > > to S and Text.]
> >
> > From the top of my head
> >
> > package PL_1
> >
> >   function String_Reverse (S : in String) return String is
> >   begin
> >      if S'Lenght <= 1 then
> >        return S;
> >      else
> >        return String_Reverse (Tail(S)) & Head(S);
> >      end if
> >   end String_Reverse;
> > end PL_1;
>
> This is Ada code, not PL/I code.  I already supplied
> Ada code in the PL/I source example above.

I was just as confused as Martin. Your "Ada" code is not correct Ada
code.

There is no standard Ada type named "text".
Your Ada example will not compile under any Ada compiler as written.
You indicate that TAIL and HEAD are PL/I routines.
They will not compile in any Ada compiler given the code segment
you presented.

Where is the Length function defined? It is certainly not defined in
any of the code you present.

If your example compiles in a PL/I compiler with the assumption
that it is Ada code, then I marvel at the usefulness. Why would
you want a compiler that does not identify serious syntax errors?

Jim Rogers

Re: Buffer overflow Article - CACM

[robin]

<jimmaureenrogers@worldnet.att.net> wrote in message
news:1136173025.947352.25110@g44g2000cwa.googlegroups.com...
> robin wrote:
> > "Martin Krischik" <krischik@users.sourceforge.net> wrote in message
> > news:4626568.XPZCFmT196@linux1.krischik.com...
>
> > > > PL/I can compile and execute the following source.  Can Ada do the same
> > > > for PL/I?
> > > >
> > > > Mixed: procedure options (main);
> > > >     ...
> > > > ADA(
> > > > StringReverse (S: Text) return Text is
> > > > begin
> > > >     if Length(S) <= 1
> > > >        then return S;
> > > >        else return StringReverse(Tail(S)) & Head(S);
> > > > end StringReverse;
> > > > );
> > > > end mixed;
> > > >
> > > > [I have not written here the PL/I code for TAIL and HEAD,
> > > > nor the declarations for the variables corresponding
> > > > to S and Text.]
> > >
> > > From the top of my head
> > >
> > > package PL_1
> > >
> > >   function String_Reverse (S : in String) return String is
> > >   begin
> > >      if S'Lenght <= 1 then
> > >        return S;
> > >      else
> > >        return String_Reverse (Tail(S)) & Head(S);
> > >      end if
> > >   end String_Reverse;
> > > end PL_1;
> >
> > This is Ada code, not PL/I code.  I already supplied
> > Ada code in the PL/I source example above.
>
> I was just as confused as Martin. Your "Ada" code is not correct Ada
> code.
>
> There is no standard Ada type named "text".

The Ada code presented is obviously an extract, part of an Ada program.
I wasn't about to type the whole Ada program; that would be a WOT.
It's sufficient to give an extract.

> Your Ada example will not compile under any Ada compiler as written.

Obviously, it would need the missing elements that I mentioned.

> You indicate that TAIL and HEAD are PL/I routines.
> They will not compile in any Ada compiler given the code segment
> you presented.

The PL/I routines will compile with a PL/I compiler.

> Where is the Length function defined? It is certainly not defined in
> any of the code you present.
>
> If your example compiles in a PL/I compiler with the assumption
> that it is Ada code, then I marvel at the usefulness. Why would
> you want a compiler that does not identify serious syntax errors?

There are no Ada errors in the code.

Re: Buffer overflow Article - CACM

[Georg Bauhaus]

On Sun, 2006-01-01 at 23:12 +0000, robin wrote:


> The point is that Ada code can be compiled direct by a
> PL/I compiler.

Even though it wasn't strictly Ada code, as pointed out,
what's the point? For sure, Ada can compile C statements,
Eiffel statements, and Lisp expressions. And I don't mean
via the standardized Interfaces.* mechanism. Consider

	do
		x.foo(42);
	end;

which language is that? It is both Ada, and Eiffel, and
maybe some more. Though it is not clear that the meaning
of the translated code will be the same in both languages.

	(foo (bar (thr)))

Is this a piece of CommonLISP, or is it C,
Ada, Algol, Pascal, Modula, Oberon, C++, D, PL/1, ...

The point here is that you are trying to praise
your language by showing that there is a
small overlap, mostly syntactically, with some other
language. That doesn't help much in comparing languages,
and how they can help achieving project goals better
than some other languages.

It will be interesting to learn which definitions of
some interesting PL/1 features can be reworked into
the LRM framework of Ada as an improvement, and how,
specifically.

Re: Buffer overflow Article - CACM

[robin]

"Georg Bauhaus" <bauhaus@futureapps.de> wrote in message
news:1136281961.9673.21.camel@sonnenregen...
> On Sun, 2006-01-01 at 23:12 +0000, robin wrote:
>
> > The point is that Ada code can be compiled direct by a
> > PL/I compiler.
>
> Even though it wasn't strictly Ada code, as pointed out,
> what's the point? For sure, Ada can compile C statements,
> Eiffel statements, and Lisp expressions. And I don't mean
> via the standardized Interfaces.* mechanism. Consider
>
> do
> x.foo(42);
> end;
>
> which language is that? It is both Ada, and Eiffel, and
> maybe some more. Though it is not clear that the meaning
> of the translated code will be the same in both languages.
>
> (foo (bar (thr)))
>
> Is this a piece of CommonLISP, or is it C,
> Ada, Algol, Pascal, Modula, Oberon, C++, D, PL/1, ...
>
> The point here is that you are trying to praise
> your language by showing that there is a
> small overlap, mostly syntactically, with some other
> language.

No I'm not trying to do that.
    I'm saying that Ada code can be compiled by a PL/I
compiler, illustrating the versatility of the language.
    I'm not relying on any similarity of statements to achieve that.

Re: Buffer overflow Article - CACM

[Georg Bauhaus]

On Thu, 2006-01-12 at 22:10 +0000, robin wrote:

>     I'm saying that Ada code can be compiled by a PL/I
> compiler, illustrating the versatility of the language.

OK. C++ code can be compiled by a C compiler, illustrating
the versatility of the C language.

I should hope that this kind of argument isn't used in
evaluations of programming languages for programming
projects.

-- Georg 

Re: Buffer overflow Article - CACM

[Keith Thompson]

"robin" <robin_v@bigpond.com> writes:
> "Georg Bauhaus" <bauhaus@futureapps.de> wrote in message
> news:1136281961.9673.21.camel@sonnenregen...
[...]
>> The point here is that you are trying to praise
>> your language by showing that there is a
>> small overlap, mostly syntactically, with some other
>> language.
>
> No I'm not trying to do that.
>     I'm saying that Ada code can be compiled by a PL/I
> compiler, illustrating the versatility of the language.
>     I'm not relying on any similarity of statements to achieve that.

For context, here's the sample PL/I code you posted upthread:

] Mixed: procedure options (main); 
]     ... 
] ADA( 
] StringReverse (S: Text) return Text is 
] begin 
]     if Length(S) <= 1 
]        then return S; 
]        else return StringReverse(Tail(S)) & Head(S); 
] end StringReverse; 
] ); 
] end mixed;

Presumably the Ada type "Text" and the various functions are defined
elsewhere.

So PL/I, or some particular PL/I implementation, has a mechanism to
include Ada code inline.  Presumably this wasn't originally a feature
of the language, since PL/I substantially predates Ada.

Please keep in mind that you're posting in a forum where most of us
don't know PL/I.  Posting a code fragment isn't very useful unless you
provide some more information.

Is this "ADA( ... );" construct a feature of the standard PL/I
language (is there a standard?), or is it an extension provided by one
particular implementation?  Are languages other than Ada supported?
Does the PL/I compiler itself actually compile the Ada code (that
seems unlikely), or does it invoke a separate Ada compiler?  What are
the semantics and restrictions of the construct?  What advantages, if
any, does this give you over compiling the Ada code separately and
linking the Ada and PL/I code together?

Without this information, the code fragment you posted doesn't seem
very illuminating.

-- 
Keith Thompson (The_Other_Keith) kst-u@mib.org  <http://www.ghoti.net/~kst>
San Diego Supercomputer Center             <*>  <http://users.sdsc.edu/~kst>
We must do something.  This is something.  Therefore, we must do this.

Re: Buffer overflow Article - CACM

[Dan Nagle]

Hello,

Keith Thompson wrote:

<snip>

> Is this "ADA( ... );" construct a feature of the standard PL/I
> language (is there a standard?), or is it an extension provided by one
> particular implementation?

The most recent PL/I standard published by ANSI is dated 1979.
There is a "real-time extensions" standard published in the mid '80s,
and a subset PL/I published in the early '90s.

The SC22 WG for PL/I is no more, and the INCITS J TC for PL/I
is begging to be left in "inactive" status (presumably, rather
than being disbanded).

Check http://www.incits.org/tc_home/j1.htm et seq. for details.

<snip>

-- 
Cheers!

Dan Nagle
Purple Sage Computing Solutions, Inc.

Re: Buffer overflow Article - CACM

[Björn Persson]

Keith Thompson wrote:
> For context, here's the sample PL/I code you posted upthread:
> 
> ] Mixed: procedure options (main); 
> ]     ... 
> ] ADA( 
> ] StringReverse (S: Text) return Text is 
> ] begin 
> ]     if Length(S) <= 1 
> ]        then return S; 
> ]        else return StringReverse(Tail(S)) & Head(S); 
> ] end StringReverse; 
> ] ); 
> ] end mixed;
> 
> Presumably the Ada type "Text" and the various functions are defined
> elsewhere.
> 
> So PL/I, or some particular PL/I implementation, has a mechanism to
> include Ada code inline.

Or rather code in some vaugely Ada-like language, apparently, as 
"function" and "end if;" would have to be inserted in Robin's code to 
turn it into Ada.

-- 
Bj�rn Persson                              PGP key A88682FD
                    omb jor ers @sv ge.
                    r o.b n.p son eri nu

Re: Buffer overflow Article - CACM

[robin]

"Dennis Lee Bieber" <wlfraed@ix.netcom.com> wrote in message
news:12ces1lv5dvm6pifdapj11o1hrtlm6ec7q@4ax.com...
> On Thu, 12 Jan 2006 22:10:34 GMT, "robin" <robin_v@bigpond.com>
> declaimed the following in comp.lang.ada:
>
> > No I'm not trying to do that.
> >     I'm saying that Ada code can be compiled by a PL/I
> > compiler, illustrating the versatility of the language.
> >     I'm not relying on any similarity of statements to achieve that.
> >
> Does that illustrate the versatility of PL/1 OR just the fact that
> the specific compiler incorporates multiple language parsers within it.

It illustrates the former.  The compiler does not have
an ADA language parser embedded in it.

Re: Buffer overflow Article - CACM

[robin]

Christopher Browne wrote in message ...

>Something that is only approximately correct but that is super-fast
>may, in cases where time or computational effort *are* at a premium,
>be preferable to a slower "correct all the time" program.
>
>The trouble with formal verification methods is that they consume time
>(for the analysis work) when you may well discover that the problem
>wasn't specified well enough in the first place for formal
>verification to actually do any material good.
>
>Having super-well-specified problems is extremely necessary when doing
>"rocket science;" if it costs $1B to fire off a rocket, and you don't
>get a second chance, it's necessary to do whatever up-front effort is
>required to make sure the problem is super-well-specified.
>
>But there are a lot of cases where that level of effort is not
>warranted, and it's NOT worth getting "super-detailed, super-correct"
>specifications, and it's NOT worth various of the efforts.
>
>Where the CACM article has some things *right* is that there are
>plenty of systems where it would be way too costly to reimplement them
>in a buffer-overflow-immune language.  People are not going to redo
>everything in PL/1 or Ada just because they have better specified
>string types.  They don't have time.

Perhaps the message of the article is that for future
projects those languages would provide better outcomes.

>--
>(format nil "~S@~S" "cbbrowne" "ntlug.org")

Re: Buffer overflow Article - CACM

[Peter Amey]

Jeffrey R. Carter wrote:
> adaworks@sbcglobal.net wrote:
> 
[snip]
> 
> Then they say that bounds checking adds 100% overhead. This may be true 
> of trying to patch C, but it's certainly not true of all the checks Ada 
> does, which is much more than simply bounds checking. In practice I have 
> never found a case in which leaving checks in was too slow, nor where 
> turning them off saved more than 10%.
> 

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

Re: Buffer overflow Article - CACM

[Harald Korneliussen]

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?

Re: Buffer overflow Article - CACM

[Peter Amey]

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

Re: Buffer overflow Article - CACM

[Brian May]

>>>>> "Harald" == Harald Korneliussen <vintermann@gmail.com> writes:

    Harald> I though that with SPARK, you have to write your program
    Harald> with no moving parts (or dynamic data structures) and then
    Harald> supply a suite of proofs, which may be quite hard, even
    Harald> with the assistant? How often is this practical?

Another issue with SPARK is that it appears to be non-free software
(unless you can meet the criteria for academic use where you can use
it for 0 cost), and no prices are given online the website.

This makes me suspect it will be out of reach for average free
software authors, and most of the software I use falls into this
category.

On the other hand, please correct me if I am wrong...
-- 
Brian May <bam@snoopy.apana.org.au>

Re: Buffer overflow Article - CACM

[Jeffrey R. Carter]

Brian May wrote:

> Another issue with SPARK is that it appears to be non-free software
> (unless you can meet the criteria for academic use where you can use
> it for 0 cost), and no prices are given online the website.
> 
> This makes me suspect it will be out of reach for average free
> software authors, and most of the software I use falls into this
> category.
> 
> On the other hand, please correct me if I am wrong...

Free versions of the SPARK tools are available at

http://www.praxis-his.com/sparkada/sparkbook.asp

These are intended for those who have read Barnes' book. All versions of the 
SPARK tools are written in SPARK and thus have static-sized internal structures; 
the structures in the free versions are relatively small, so the size of 
projects that they may be used for is fairly small.

-- 
Jeff Carter
"Crucifixion's a doddle."
Monty Python's Life of Brian
82

Re: Buffer overflow Article - CACM

[Harald Korneliussen]

Jeffrey R. Carter wrote:
> Brian May wrote:
>
> > Another issue with SPARK is that it appears to be non-free software
> > (unless you can meet the criteria for academic use where you can use
> > it for 0 cost), and no prices are given online the website.
> >
> > This makes me suspect it will be out of reach for average free
> > software authors, and most of the software I use falls into this
> > category.
> >
> > On the other hand, please correct me if I am wrong...
>
> Free versions of the SPARK tools are available at
>
> http://www.praxis-his.com/sparkada/sparkbook.asp
>
> These are intended for those who have read Barnes' book. All versions of the
> SPARK tools are written in SPARK and thus have static-sized internal structures;
> the structures in the free versions are relatively small, so the size of
> projects that they may be used for is fairly small.
>
Thank you, that's very interesting. I'm still a bit sceptical about
this static-sized internal structures thing, though. Isn't programming
without dynamic allocation difficult? Last time I did it was in
Commodore Basic, and that's because I didn't know how to do it then :-)

I would think that some software (for instance the browser and
windowing system I'm using now) would be practically impossible to
write in SPARK or similar languages?

Re: Buffer overflow Article - CACM

[Martin Dowie]

Harald Korneliussen wrote:
> Thank you, that's very interesting. I'm still a bit sceptical about
> this static-sized internal structures thing, though. Isn't programming
> without dynamic allocation difficult? Last time I did it was in
> Commodore Basic, and that's because I didn't know how to do it then

Not at all - if anything it is easier!

SPARK is typically found in "embedded, real-time" systems, where the number
of things the software has to deal with is fixed and known at compilation
time.

Re: Buffer overflow Article - CACM

[Jeffrey R. Carter]

Harald Korneliussen wrote:
> 
> Thank you, that's very interesting. I'm still a bit sceptical about
> this static-sized internal structures thing, though. Isn't programming
> without dynamic allocation difficult? Last time I did it was in
> Commodore Basic, and that's because I didn't know how to do it then :-)
> 
> I would think that some software (for instance the browser and
> windowing system I'm using now) would be practically impossible to
> write in SPARK or similar languages?

SPARK is primarily for critical SW, where max sizes for things are typically 
known at compile time. But one can use SPARK for only the critical parts of a 
system, hiding the rest of the system from the SPARK tools.

Consider a stack of Integers:

package Integer_Stack
--# own State;
--# initializes State;
is
    function Is_Empty return Boolean;
    --# global State;

    procedure Clear;
    --# global out State;
    --# derives State from ;
    --
    --# post Is_Empty (State);

    procedure Push (Item : in Integer);
    --# global in out State;
    --# derives State from State, Item;
    --
    --# post not Is_Empty (State);

    procedure Pop (Item : out Integer);
    --# global in out State;
    --# derives State, Item from State;
    --
    --# pre not Is_Empty (State);
end Integer_Stack;

Now you can implement Integer_Stack in SPARK. Or you could hide the 
implementation from SPARK. In that case, it could use an instantiation of 
PragmARC.Stack_Bounded, adhering to the spirit of SPARK (static size) but not 
the letter (no generics). Or it could use an instantiation of 
PragmARC.Stack_Unbounded and have a dynamic size. (I deliberately omitted 
Is_Full and pre/post-conditions about fullness to allow such an implementation.)

SPARK puts 2 kinds of restrictions on Ada. There are restrictions that are 
needed to allow the kinds of analysis SPARK does, and there are restrictions to 
ensure everything is sized statically (of course, some fall into both 
categories). When you're writing SW for a PC, you generally can assume lots of 
storage and might be willing to allow dynamic sizing. It would be nice to still 
be able to do the SPARK analysis and be more confident that your SW is correct. 
That would entail an option to the tools that turns off the 2nd kind of 
restriction checking. I'm not even sure that would be possible, but I'd find it 
useful if it were.

-- 
Jeff Carter
"You tiny-brained wipers of other people's bottoms!"
Monty Python & the Holy Grail
18