[Haskell-cafe] More on the random idea

[Claus Reinke]

> The #haskell people have been working on this for about 3 years now.
> The result is the 'runplugs' program, which I've talked about in
> previous mails.
>
>    http://www.cse.unsw.edu.au/~dons/code/lambdabot/scripts/RunPlugs.hs
>
> It uses hs-plugins for the evaluation, along with the points about IO
> prevention via type checking, resource limits controlled by the OS,
> language extension preventions, and a trusted (audited) module base.

great! and since it is presumably in daily use, there is both pressure to
fix holes as soon as they are discovered, and ongoing discovery in a
safe (or at least friendly) environment.

still, that only gives us a box. how about some more sand?-) for instance,
one could try to provide a safe redefinition of some basic IO operations,
such as reading and writing a limited amount of files below a local
directory? of course, permitting some IO is trickier than ruling out all IO
(standard example: i really meant 'below', as in prefixing all paths and
ruling out upward links like '..', not just 'relative to';).

> The security mechanisms were briefly described in the 2004 hs-plugins
> paper, if I recall, but otherwise, I don't think we've documented the
> techniques. Maybe we should, as many issues have been encountered over
> the years, further and further constraining the kinds of things that are
> allowed.

documenting the techniques would ease verification, and make it
easier to check what you've already covered and what might yet
be missing. for instance, i assume that hs-plugins, unlike ghci, does
not permit direct access to qualified names (in ghci, i can refer to
'System.IO.Unsafe.unsafePerformIO' without 'import' or ':m +')?
and i assume that even though you only limit time, there is no way
to use up all space in no time?

you do seem to be protected against this simple one, but it might
give others something to think about (no explicit i/o, no imports,
no recursion, only expressions):

    let {p x y f = f x y; f x = p x x}
    in f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f 
f)))))))))))))))))) f

claus