Difference between revisions of "Safely running untrusted Haskell code"

From HaskellWiki
Jump to navigation Jump to search
Line 1: Line 1:
 
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...
  
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,
  +
#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, <hask>eval :: String -> IO
  +
String</hask>, 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:
  +
  +
* [http://www.cse.unsw.edu.au/~dons/code/lambdabot/Plugin/Eval.hs Driver/simple verifier]
  +
* [http://www.cse.unsw.edu.au/~dons/code/lambdabot/scripts/RunPlugs.hs 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 also ==

Revision as of 05:33, 27 May 2007

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:

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

Retrieved from "https://wiki.haskell.org/index.php?title=Safely_running_untrusted_Haskell_code&oldid=13236"