Difference between revisions of "Safely running untrusted Haskell code"
DonStewart (talk | contribs) |
DonStewart (talk | contribs) |
||
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,
- 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
- See a long discussion in Haskell Cafe.
- The GHC ticket for -fsafe