[Haskell-cafe] More on the random idea

[Donald Bruce Stewart]

claus.reinke:
> >>Oh, but there is the *minor* detail that I am literally allowing
> >>unauthenticated users to perform arbitrary code execution. For example,
> ..
> >>AFAIK, Lambdabot dissalows any expression that performs IO. In Haskell,
> >>this is beautifully easy: reject any expression having an IO type.
> ..
> >Don't use parsing for security, use the type checker. By using 'show',
> >you can write an instance for IO a that renders all IO harmless. Then
> >just wrap your user's arbitrary expression in 'show.
> 
> careful please!-) we've had enough of that kind of issues in scripts, CGI, 
> ..
> sandboxes, etc. to have learned the lesson that *this is not a minor 
> detail*,
> and requires full attention to details, especially, but not only if, meta-
> programming is involved (interpreting input strings as programs, or using
> hs-plugins, template haskell).
> 
> two obvious exceptions: 'unsafePerformIO' and FFI. even expressions
> not involving IO might use it internally (also, you want to disallow both
> write and read access). less obvious: DOS-style issues, eg, filling the
> process table or claiming all memory. least obvious: things we've missed.
> 
> it would really be nice if someone would sit down and sort this all out
> in detail. there'd still be no guarantee that such a Haskell sandbox was
> totally safe, but at least all issues and solutions could be shared, making
> it as safe as the community  knows how.

Claus is right. You need type guarantees, and more!

Lambdabot uses 1) type guarantee of no-IO at the top level, along with
2) a trusted module base (pure module only, that are trusted to not
export evil things), as well as 3) restricting only to H98-language only
(things like TH can, and have been, exploited, for example).

So, no-IO type, trusted base of no FFI, no unsafe*, resource limits, and
no extensions beyond H98, then , hopefully, we're ok.

-- Don