How safe is Safe Haskell?

Question

I was thinking about Safe Haskell and I wonder how much I can trust it?

---

Some fictional scenarios:

1. I am a little hacker writing a programmable game (think Robocode) where I allow others to program their own entities to compete against each other. Most of the time users will run some untrusted programs on private machines. Untrusted code would probably be inspected before running it.

2. I am the programmer of an application that is used by several clients. I provide an api so they can extend the functionality and encourage my users to share their plugins. The user community is small and most of the time there is mutual trust, but occasionally someone is working on a top-secret client project and any dataleaks would prove disastrous.

3. I am ... Google (or Facebook,Yahoo,etc) and want to allow my clients to script their email accounts. Scripts are uploaded and are run on my servers. Any access violations would be fatal.

---

Given these scenarios:

• would Safe Haskell be appropriate to ensure sandboxing and access restriction?
• Should someone in the given situations be able to trust the promises made?

Answer 1

As a rule of thumb, I'd say safe Haskell tries to get roughly where the safe subset of C# is. For your scenarios:

1. Can use safe haskell because you are inspecting code.
2. Cannot really use safe haskell alone to avoid disastrous data leaks.
3. I wouldn't recommend Google or Yahoo relying on safe haskell alone to run untrusted code. For one thing, it doesn't manage excessive resource consumption (CPU,memory,disk) or bottoms (undefined or while true). Use an OS sandbox for that.

A note on undefined: operationally, it stops the function returning a value by throwing an exception, as does the error function. Denotationally, it's considered to be the 'bottom' value. Now, even if safe Haskell disallowed undefined and error, a function could still fail to return, just by looping endlessly. And an endless loop is bottom too. So safe Haskell guarantees type and memory safety but doesn't try to guarantee that functions terminate. Safe Haskell is, of course, Turing complete, so it's not possible in general to prove termination. Furthermore, since out-of-memory throws an exception, functions may terminate with them. Finally, pattern match errors throw exceptions. So safe Haskell cannot eliminate bottoms of any kind and may as well allow explicit undefined and error.