Safely running untrusted Haskell code

Obviously, don't run code in the IO monad, just show pure results (or possibly make your own monad that is a restricted subset of IO). But it's a lot more complicated than that...

Verifying safety : lambdabot's approach

Since 2004, lambdabot has executed arbitrary strings of Haskell provided by user's of various [IRC_channel|IRC channels], in particular,

1. haskell. In order to do this, a particular security policy is required.

The policy, and its implementation, is described here.

The policy

Only allow execution of pure Haskell expressions.

The implementation

The evaluator is essentially a function, eval :: String -> IO String, which takes a random Haskell string, verifies it, compiles it, and evaluates the result, returning a String representing the result, back over the network.

This function is implemented as two separate processes:

• Driver/simple verifier
• Evaluator binary

The driver reads a String from the network, and then subjects it to a simple test:

• parse the expression to check it is a Haskell 98 expression

If the string parses as a Haskell 98 expression, the 'runplugs' process is then forked to evaluate the string, and the following checks are put in place:

• Only a trusted module set is imported, avoiding unsafePerformIO and stToIO and such like.
• Module imports are disallowed
• Time and space limitations on the runplugs process are set by the OS
• The expression is bound to a random top level identifier (harmless to guess)
• The expression is wrapped in 'show', and must be an instance of Show
• An instance of Show IO is defined, which prints "<IO>", rendering IO impossible.
• The expression is type checked, with the show constraint, enforcing purity
• If it type checks, and the type checker doesn't time out, it is compiled to native code with -fasm
• Only -fextended-default-rules are allowed, as language extensions over H98.
• The resulting .o file is dynamically linked into the throw-away runplugs instance
• The value is evaluated inside an exception handler.
• If an exception is thrown, only the first 1024 bytes of the exception string are returned.
• If all went well, the first 2048 bytes of the shown string are returned to the caller.

Exploits

A variety of interesting exploits have been found over the years. Those we remember are listed below:

• using newtype recursion to have the typechecker not terminate
• using pathological type inference cases to have the type checker not terminate
• code injection of code fragments that arne't haskell expressions
• Template Haskell used to run IO actions during type checking
• stToIO to convert a safe ST action, into an IO action that is run
• large strings returned in exceptions

See also

• See a long discussion in Haskell Cafe.
• The GHC ticket for -fsafe