Re: OT: Re: Secure popen

[[EMAIL PROTECTED] (Ryan Russell)]

On Sun, 1 Jul 2001, Crispin Cowan wrote:

> Now we're back to Turing Completeness.  Any language that is Turing Complete
> allows the coder to write bad logic, creating a vulnerability.

Logic problems are a somewhat different category than unsafe library
calls.  I'd prefer a language that requires logic errors to make security
holes, versus one that allows logic problems AND library problems.  I.e. I
think it might be possible to make a language with no library problems,
after enough language code review.  I agree with you that Turing complete
languages will always allow for logic problems.

>  More over,
> Turing's Halting Problem proves that, in general, it is undecidable whether a
> given program is secure, because it is undecidable whether a given program,
> when given some input, will halt or not.  Here, "undecidable" means "you
> can't write a static analyzer that will do a perfect job."

You can't write a program with a Turing machine (equivalent to any
computer so far) that can automatically determine if every other program
will halt by examining their code.  For a computer to spot security
problems in every case won't ever be possible, because some of the are
logic problems, and the computer can't read the programmers mind to figure
out what they meant to do.

> Humans most often
> can analyze code and decide,

I think humans can always determine halting, no?  My comp-sci professors
also claimed that it is possible to "prove" a program does what it is
supposed to.  I don't know if this extends to proving a program is secure
or not.  It's probably a moot point anyway.  None of the professors were
willing to demonstrate a proof of corectness at any point, they said it
was too hard.  Considering the proofs they WERE willing to go over,
proving correctness much be a huge pain.


> and heuristic analyzers often can give a
> definitive answer for restricted cases.  Static type checking is a restricted
> case.  But you cant do a totally automatic, static, "this code is secure"
> check.

They won't ever be able to catch logic problems.  You can write checkers
for unsafe calls (I think the current code review tools all do this?).
This works for all known unsafe calls, with enough work.  You can also
create a langauge or compiler that just doesn't have the unsafe calls.

>
> Which is what makes security particularly challenging :-)
>

Hmm...  May you live in interesting times. :)

					Ryan