Re: [Caml-list] Rewriting UNIX in Caml and getting rid of the C disease

[Mark Seaborn <mrs35@cam.ac.uk>]

Berke Durak <berke@altern.org> writes:

[...]
> An appropriate sublanguage of Caml should be isolated, and a given,
> well-accepted brand of UNIX should be reimplemented in that language.
> Binary compatibility must be retained as far as possible. Basic system
> utilities (including a shell) should also be translated (into full
> Ocaml). Since the use of Caml will, a) divide the source code size by,
> say, ten and b) automatically remove, say, 95% of all bugs and
> security holes (since most are illnesses resulting from pointer
> manipulation), success is guaranteed.
[...]

You may be interested in a project I am implementing at the moment:
The idea is to automatically translate any C program into a
memory-safe language.  This can be done by assuming that a block of
memory should only be accessed through values that depend on the
block's address.  The blocks that a value is dependent on can be
tracked at run time, but static analysis can be used to eliminate this
cost hopefully in most cases.  This scheme can be applied to turn
filenames, as well as pointers, into unforgable capabilities.

I've written a draft paper explaining this which is at:
<http://www.srcf.ucam.org/~mrs35/comp/safe-c/making-c-programs-safe.txt>

-- 
         Mark Seaborn
   - mseaborn@bigfoot.com - http://www.srcf.ucam.org/~mrs35/ -

  ``Every revolutionary opinion draws part of its strength from a secret 
      conviction that nothing can be changed'' -- George Orwell
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr