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
Precisely.
'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?
ulimits, from the shell, yes. Though ...
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
Exactly. This will trigger a timeout, when ghc fails to typecheck it in 3 seconds. -- Don