Deprecating Safe Haskell, or heavily investing in it?

[Jaro Reinders]

The bytestring package does have run time bounds checks. So maybe Safe Haskell is safer than you think?

On December 27, 2022 9:12:44 PM GMT+01:00, Viktor Dukhovni <ietf-dane at dukhovni.org> wrote:
>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.
>
>-- 
>    Viktor.
>_______________________________________________
>ghc-devs mailing list
>ghc-devs at haskell.org
>http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs