Deprecating Safe Haskell, or heavily investing in it?

[Hécate]

Thanks for your input Viktor!

I came across the nsjail system from Google a little while after posting 
this thread: https://github.com/google/nsjail/#overview

Perhaps we could get the most value for our buck if we externalise the 
solution to work with OS-level mechanisms?
What do you think of that? Something based upon eBPF would certainly 
incur less modifications to the RTS?

Le 27/12/2022 à 21:12, Viktor Dukhovni a écrit :
> On Tue, Dec 27, 2022 at 06:09:59PM +0100, Hécate wrote:
>
>> Now, there are two options (convenient!) that are left to us:
>>
>> 1. Deprecate Safe Haskell: We remove the Safe mechanism as it exists
>> today, and keep the IO restriction under another name. This will
>> certainly cause much joy amongst maintainers and GHC developers alike.
>> The downside is that we don't have a mechanism to enforce "Strict
>> type-safety" anymore.
>>
>> 2. We heavily invest in Safe Haskell: This is the option where we amend
>> the PVP to take changes of Safety annotations into account, invest in
>> workforce to fix the bugs on the GHC side. Which means we also invest in
>> the tools that check for PVP compatibility to check for Safety. This is
>> not the matter of a GSoC, or a 2-days hackathon, and I would certainly
>> have remorse sending students to the salt mines like that.
>>
>> I do not list the Status Quo as an option because it is terrible and has
>> led us to regularly have complaints from both GHC & Ecosystem libraries
>> maintainers. There can be no half-measures that they usually tend to
>> make us slide back into the status quo.
>>
>> So, what do you think?
> I think that "Restricted IO" would in principle be the more sensible
> approach.  HOWEVER, for robust "sandboxing" of untrusted code what's
> required is more than just hiding the raw IO Monad from the sandboxed
> code.  Doing that securely is much too difficult to do correctly, as
> evidenced by the ultimate failure (long history of bypass issues) of
> similar efforts for enabling restricted execution of untrusted code in
> Java (anyone still using Java "applets", or running Flash in their
> browser???).
>
> The only way to do this correctly is to provide strong memory separation
> between the untrusted code and the TCB.  The only mainstream working
> examples of this that I know of are:
>
>      * Kernel vs. user space memory separation.
>
>      * Tcl's multiple interpreters, where untrusted code runs in
>        slave interpreters stripped of most verbs, with aliases
>        added to wrappers that call back into the parent interpreter
>        for argument validation and restricted execution.
>
> Both systems provide strong memory isolation of untrusted code, only
> data passes between the untrusted code and the TCB through a limited
> set of callbacks (system calls if you like).
>
> For "Safe Haskell" to really be *safe*, memory access from untrusted
> code would need to be "virtualised", with a separate heap and foreign
> memory allocator for evaluation of untrusted code, and the RTS rewriting
> and restricting all direct memory access.  This means that "peek" and
> "poke" et. al. would not directly read memory, but rather be restricted
> to specific address ranges allocated to the untrusted task.
>
> Essentially the RTS would have to become a user-space microkernel.
>
> This is in principle possible, but it is not clear whether this is worth
> doing, given limited resources.
>
> To achieve "safe" execution, restricted code needs to give up some
> runtime performance, just compile-time safety checks are not
> sufficiently robust in practice.  For example, the underlying byte
> arrays (pinned or not) behind ByteString and Text when used from
> untrusted code would not allow access to data beyond the array bounds
> (range checked on every access), ...  which again speaks to some
> "virtualisation" of memory access by the RTS, at least to the extent of
> always performing range checks when running untrusted code.
>
> Bottom line, I don't trust systems like Safe Haskell, or Java's
> type-system-based sandboxing of untrusted code, ... that try to perform
> sandboxing in a shared address space by essentially static analysis
> alone.  We've long left shared address space security systems DOS and
> MacOS 9 behind... good riddance.
>
-- 
Hécate ✨
🐦: @TechnoEmpress
IRC: Hecate
WWW: https://glitchbra.in
RUN: BSD