Deprecating Safe Haskell, or heavily investing in it?

[b.gohla]

I have implemented something like that actually: https://github.com/cgohla/pledgeWorking out a portable API could be difficult.Sent from my Galaxy
-------- Original message --------From: Hécate <hecate at glitchbra.in> Date: 27/12/22  20:39  (GMT+00:00) To: ghc-devs at haskell.org Subject: Re: Deprecating Safe Haskell, or heavily investing in it? 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/#overviewPerhaps 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 ✨🐦: @TechnoEmpressIRC: HecateWWW: https://glitchbra.inRUN: BSD_______________________________________________ghc-devs mailing listghc-devs at haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20221228/ac3339f0/attachment.html>