[Haskell-cafe] Safe Haskell?

[Joachim Durchholz]

Am 21.04.21 um 20:24 schrieb Viktor Dukhovni:
> On the other hand, I've always been sceptical of the sandboxing in Java,
> it was much too complex to be obviously correct, and the long history of
> bugs in Java applet sandboxing justified the scepticism.  Fortunately we
> longer use Java applets, though JavaScript security in browsers
> continues to be challenging.

Same here.

> So it should not be surprising that I'd also be sceptical of any
> strong safety claims from Safe Haskell.  It seems unlikely to be
> simple enough to be "obviously correct".  This does not mean that it
> can't be a useful element of defense in depth, but it is difficult to
> envision how it would be sufficient on its own.
> 
> The challenge with Safe Haskell, unlike with safe Tcl, is that there
> is no hard separation between the untrusted and trusted components of
> the program, they're only separated by static analysis, not
> separation into distinct execution engines with a controlled
> communication channel as with Safe Tcl and slave interpreters.
For Safe Haskell, the substrate language is much easier to reason about 
- there's no way for static analysis to work well with Java (aliasing 
alone will preven that), but such a thing *is* possible with Haskell. 
Heck, ghc is doing deforestation and similar things, no such thing would 
be even remotely thinkable for any imperative language!

So while I agree in principle, I believe Safe Haskell could be safer 
than the experience with sandboxing in an imperative language would be.

The other thing is that the Java sandbox pretty obviously spent more 
time on writing enabling code than on validating that a new feature 
doesn't influence existing ones, and you need the opposite approach when 
doing sandboxes.
I.e. I believe the Java sandbox failed not just because it's inherently 
more difficult, but also because the budget was too limited.

> Haskell libraries that export safe pure interfaces, internally use
> unsafe interfaces (e.g. raw memory access) for performance reasons.
> So it is rather unclear how to expose a usable untrusted subset of the
> language except through static analysis (type level guarantess) of the
> sort that I'm reluctant to trust as a result of high complexity.

Validating that an inference chain is correct is much easier.
You need to have pretty simple axioms to make sure you don't get an 
inconsistent system, or one that doesn't prove the things you believe it 
proves. (This did indeed happen, IIRC the $ operator turned out to be 
much less safe than originally believed sometime around 2000.)

> So while I take no position on whether Safe Haskell should or should not
> be abandoned, I agree that it is a valid question because the problem is
> rather non-trivial, and it is not clear whether it is actually possible to
> implement a sufficiently robust design.

Fully agreed.
Not because the inference engine cannot be trusted, but because it's 
hard to set up a good set of axioms if you have things like unsafe 
operations and still want to prove that their use in a particular piece 
of is safe under Haskell's semantics.
OTOH this is one of the things that I would have liked to see happen two 
decades ago and it didn't materialze; quite the opposite, the attempts 
at putting up a formal semantics for Haskell, while promising initially, 
were given up because it would be too much work, and that means any 
inference engine is walking on shifting ground. I do not feel very 
confident in *that* regard, I have to say.
Still, it could be more trustworthy than syscall sandboxing, if Safe 
Haskell is usefully strict enough about its inferencing. I just don't 
have enough insight into Safe Haskell so make any predictions there :-)

Regards,
Jo