[Haskell-cafe] Safe Haskell?

[Sven Panne]

Am Mi., 21. Apr. 2021 um 15:57 Uhr schrieb Joachim Durchholz <
jo at durchholz.org>:

> Actually Sandboxes have a just as complicated attack surface as languages.
>

Perhaps we are talking about different kinds of sandboxes: I'm talking
about sandboxes at the syscall level. Compared to higher level stuff they
are relatively simple. They are not small (tons of syscalls exist
nowadays), but each syscall is relatively simple compared to stuff built
upon it. Size != complexity. And the SW engineering point is: You program
your sandbox SW once and can use it for every language/program, without any
need to follow the latest and greatest hype in languages, compilers, type
systems etc. This means a *much* higher ROI compared to a language-specific
solution. Of course you won't get a PhD for a syscall sandbox...


> I also believe they are different domains.
> Secure languages deal with making guarantees about what a program does
> and, more importantly, what it does not do. So you can control things
> like IO effects, Capabilities, and the language can even make these
> guarantees statically.
>

Only if you trust your language itself, your implementation and its RTS.
And given the complexity of each of these aspects, basically any language
has security holes (see e.g. the recent discussion here about various GHC
bugs). A sandbox has a much easier job, it can e.g. always err on the safe
side.


> A sandbox deals more with API objects. This is a much more complicated
> surface because today's APIs tend to be large, complex, and interact in
> unexpected fashions; on the other hand, it is much nearer to the actual
> objects being protected.
> I.e. I believe the two approaches, while they have some overlap, they
> serve different purposes and need to complement each other.
>

A syscall sandbox needs no help whatsoever from a language.


> I believe the opposite is true.APIs change over time.


The syscall interface is extremely stable, at least compared to the rest of
all APIs in existence.


> Languages do that, too, but to a much lesser
> extent, and type system guarantees tend to hold for decades.
>

There is no such thing as a type system in the machine code actually
running, so you can't trust any higher-level guarantees.


> Even filesystem APIs are less stable than that (think NFS, or
> filesystem-dependent ACLs).
>

Do you really see the filesystem implementation on the syscall level?
Unless you're doing serious fcntl()/ioctl()-Kung-Fu or stuff like that, I
don't think so, but that's just a guess.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210421/2559128a/attachment.html>