[Haskell-cafe] Safe Haskell?

[Askar Safin]

Hi. Let me describe two hypothetical use cases for safe Haskell.

1. Isabelle ( http://isabelle.in.tum.de ) is written in SML. Input for Isabelle (theory files) are allowed to contain embedded SML source code for extending Isabelle. If someone sends you Isabelle theory and you open it in your Isabelle IDE, this embedded code starts to automatically execute. I don't know whether Isabelle authors put some restrictions to deny arbitrary code execution. So, as you probably guessed, I think this is possible to write similar prover in Haskell. Its theory files will be allowed to contain embedded Haskell code to extend prover. And SafeHaskell will be used to deny arbitrary code execution.

2. Imagine OS entirely written in Haskell. Both kernel and user space programs. In such OS we don't need any hardware methods of restriction of user programs, i. e. we don't need MMU, context switches, separation of ring 0 and ring 3. Security will be achieved by using SafeHaskell. User will be allowed to run code in user space only if it is compiled using trusted Haskell compiler with SafeHaskell enabled. After compilation the code is loaded directly into kernel address space and executed in ring 0. It will be very easy to implement capability-based security. Benefits of such model:

a) We don't have MMU and context switch overhead. System call is just function call
b) User space programs will not be able to read/write memory directly, so they will not be able to exploit Spectre/Meltdown, so there is no need in costly mitigations for this vulnerabilities (I'm not sure in b))
c) Programs live in one address space, so they can just pass each other data directly. IPC is just function call
d) Speed up caused by a), b) and c) can be so huge that it will be bigger than slow down caused by using Haskell instead of C, so usual arguments "Haskell is too slow" will go away

==
Askar Safin
https://github.com/safinaskar