Re: [Lit.] Buffer overruns

newstome_at_comcast.net
Date: 02/05/05 

Date: Fri, 04 Feb 2005 17:51:35 -0600

David Wagner <daw@taverner.cs.berkeley.edu> wrote:
>>Here's a reduction from the halting problem to checking for buffer
>>overflows: Say you've got a function f(x) and you want to see if it
>>halts. Now add the following function:
>>
>> void g(whatever x) {
>> int b[2];
>> f(x);
>> b[2] = 0;
>> }
>>
>>You get a buffer overflow on b[] iff f(x) returns (halts).
>>
>>Maybe that's a silly example, but it shows the undecidability of
>>determining whether a program has a buffer overflow.
>
> Solution: You build a conservative tool. In case of doubt (i.e., if
> you cannot prove the program/construct safe), you output a warning.
> You might get false positives -- indeed, for buffer overrun analysis
> of large C programs, you will surely get false positives, and lots of
> them -- but you don't have the undecidability problem any further.
>
> For instance, a conservative tool would output a warning about a possible
> buffer overrun in the code you gave, unless it could prove that f(x)
> never returns.

OK, but that's answering a different question. Or maybe I didn't
understand the original issue. I think it's provably impossible to
produce an analyzer that will output "yes" or "no" precisely if the
program is free from or contains buffer overflows. No "maybe"
allowed.

Whether you can produce a *useful* tool that works on a substantial
and usable subset is a different question.

> It turns out that there is a general theorem, called Rice's theorem,
> which roughly speaking says that checking any non-trivial property
> is undecidable. (The definition of non-trivial is pretty broad, and
> primarily serves to exclude properties that are either true for all
> programs or false for all programs.) This is sometimes jokingly known
> as the "full-employment theorem for programming language folks". The way
> you get around undecidability is almost always the same; you allow to err
> in one direction or the other. For instance, almost any kind of program
> optimization is undecidable; nonetheless, a good optimizer will only apply
> the optimization if it can prove that the optimization won't alter program
> behavior, and otherwise won't apply the optimization in case of doubt.

Yes, I'm well aware of that. I'm certainly not saying that analysis
tools are a waste of time because a perfect solution can't be
obtained. I'm just saying that if you build an analysis tool for
arbitrary programs there will *always* be instances that your tool
will not correctly decide.

An example, if you want one with a security flavor: HRU showed that
whether a system leaks a particular right is undecidable. But the HRU
model is extremely general, so it makes sense to ask if useful results
for useful systems possible? Of course -- Bell-LaPadula is a model
that you can prove never allows access to information by unauthorized
subjects. It's just a more restricted model.

So maybe there's a useful subset of C that can be accurately
analyzed. Or maybe there are version with hints given to the theorem
prover that allows analysis of a useful subset of programs. All these
are great research questions. 

-- 
That's News To Me!
newstome@comcast.net

Relevant Pages

  • Re: [Lit.] Buffer overruns
    ... >overflows: Say you've got a function fand you want to see if it ... >determining whether a program has a buffer overflow. ... them -- but you don't have the undecidability problem any further. ... optimization is undecidable; nonetheless, a good optimizer will only apply ...
    (sci.crypt)
  • Re: Direct Copying To Share Memory In NDIS ProtocolReceive
    ... WaitXXX() functions that involve user-to-kernel transition before they can ... access the buffer. ... and see how it all works - I wold start thinking about optimization ...
    (microsoft.public.development.device.drivers)
  • Re: Is there a STL equivalent of sprintf
    ... number of conversions. ... Have you considered ostrstream or istrstream with a fixed size buffer? ... I've played around with various optimization before and I think I've tested fix buffers too. ... Since sprintf is used internally in stringstreams I don't see a performance advantage to prefer the stream library for string conversion of integers. ...
    (microsoft.public.vc.stl)
  • Re: Performance of lists vs. list comprehensions
    ... buffer after its last expansion and no saved tuple). ... As near as I can determine, the CPython optimization you are referring to ... The optimization patch is here: ... algorithm is, ...
    (comp.lang.python)