[Haskell-cafe] Safe Haskell?
jo at durchholz.org
Thu Apr 22 19:35:07 UTC 2021
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
> continues to be challenging.
> 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
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.
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 :-)
More information about the Haskell-Cafe