[Gllug] (no subject)

[Richard Jones]

On Fri, Nov 07, 2003 at 01:12:13PM +0000, t.clarke wrote:
> Richard Jones <rich at annexia.org>  wrote:-
> >On Fri, Nov 07, 2003 at 12:27:09PM +0000, Richard wrote:
> >[Bill [Gates?] waffle about "securotics".]
> >
> >I think the point Mr Gates might be making is a valid one: languages,
> >compilers, operating systems and hardware should be performing more
> >automatic checks.
> >
> >There's really no excuse in 2003 to be writing critical infrastructure
> >in a language which doesn't support bounds checking, strong typing and
> >data tainting. There's not much more excuse for using a system which
> >doesn't have strong security mechanisms such as capabilities or ACLs,
> >all enforced by the hardware.
>
> Not being a computer-science graduate I am not at all sure what
> strong typing and data tainting is, although I can have a fair guess
> at 'bounds checking'.  How does one in the compiler prevent the
> program at runtime from using a value in an index which is out of
> range, other than detecting the error and bombing out ?

I'm not going to claim to be an expert on this!

Strong typing: read my OCaml tutorial,
http://www.merjis.com/richj/computers/ocaml/tutorial/ . If you want
the short story, http://perl.plover.com/yak/typing/ .

Data tainting: Perl has a good implementation of tainting. In fact,
correct me if I'm wrong, but isn't it about the only mainstream
language which implements tainting? Read
http://gunther.web66.com/FAQS/taintmode.html

Bounds checking: There are two ways to achieve this. The best, but
hardest way is to go for some sort of formal proof. eg. If I have
a program like this:

  let a = Array.create 10 0 in
  for i = 0 to 9 do
    a.(i) = i
  done

then there's some hope that you can prove /mathematically/ this is
correct. "But that's a stupid trivial example!", I hear you
shout. Well, yes it is, and that's because stupid trivial examples
like this are about the only ones that we currently have any hope of
formally proving :-)

Formal proofs don't help much either when you want to prove things
about programs which interact with other parties - ie. servers. The
formal proof would most of the time just tell you that a user could
overflow your fixed size buffer. Well, duh.

So the more normal way is that your compiler adds checking code which
checks array references at runtime, and then you write your program to
fail predictably when a bounds error is encountered (ie. don't turn a
simple bounds error into a denial of service attack). So:

  try
    (* Read in data from the user. *)
  with
    Invalid_argument "Array.set" ->
      (* Attempted buffer overflow. Close the connection and begin serving
       * the next user.
       *)

Notice that fixed size buffers (or at least, having fixed limits on
how much data you will attempt to process) can be a good thing if your
compiler is doing bounds checking. They avoid another type of denial
of service where someone opens a connection to your server and keeps
writing and writing until you eventually allocate all memory and swap,
and the machine crashes.

Bounds checking has a bad rap because it is incorrectly perceived to
be slow. It is slow if you implement it naively, but compilers from
since 70s have been able to make optimisations which reduce the impact
to a few percent. In particular if you're writing your programs in
Objective CAML, you may be able to *beat* C performance.

> On a more general point, Rich's sentiments would seem very laudable,
> but bearing in mind M$'s record to date, I would have grave doubts
> that shoving more responsibility on the O-S is at all a good idea.
> To me, the concept appears to be more about locking people in to the
> O-S.  I take the view, rightly or wrongly and probbaly from the
> perspective of the ill-educated in these matters, that the OS should
> stick to talking to the hardware, scheduling, managing filesystems
> etc and leave the applications to do all the other clever stuff
> mentioned.  That might well mean less 'interoperability' as M$ sees
> it, but it also leaves users free to run what software they like,
> rather than software expensively produced to interface to an
> over-complex and probably fragile O-S.

That's right. I wasn't going to claim that MS was actually going to do
any of the above :-)

Rich.

-- 
Richard Jones. http://www.annexia.org/ http://freshmeat.net/users/rwmj
Merjis Ltd. http://www.merjis.com/ - improving website return on investment
MAKE+ is a sane replacement for GNU autoconf/automake. One script compiles,
RPMs, pkgs etc. Linux, BSD, Solaris. http://www.annexia.org/freeware/makeplus/

-- 
Gllug mailing list  -  Gllug at linux.co.uk
http://list.ftech.net/mailman/listinfo/gllug