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

Hello, I disagree that Safe Haskell is a failed experiment, and I think with a little work could be a very valuable tool for auditing Haskell source code. The main change I think we should make is to completely remove the source code annotations, and instead expose an external mechanism (e.g. some sort of file) for specifying which potentially unsafe modules one trusts and which modules should be safe under those assumptions. Then GHC can do the checking and inference just like now, and people can make their own safety configurations depending on the threat model. Iavor On Tue, Dec 27, 2022, 17:08 Viktor Dukhovni wrote:

On Tue, Dec 27, 2022 at 09:39:22PM +0100, Hécate wrote:

...

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

Yes, this is the sort of thing that one can begin to trust, provided that the exposed capabalities are managed only by inclusion, all system calls, filesystem namespaces, network namespaces, ... that are not explicitly allowed are denied.

...

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?

Indeed, it would be simpler to leverage existing virtualisation and/or containerisation technologies, than build a new microkernel within the RTS. Consequently, I guess I am saying that "Safe Haskell" was an interesting research project, but may be a practical dead-end.

-- Viktor. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Viktor Dukhovni writes:

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. [...]

The other possibility is to break up your application into functional components, that run in separate processes and communicate through channels. That doesn't require any special RTS support, but it requires some infratructure, e.g., to automatically derive message types from function signatures, and to manage the subprocesses. (Ideally, one would also restrict the available kernel interface of each component using, e.g., seccomp on Linux or pledge on OpenBSD)

On Tue, Dec 27, 2022 at 10:31:07PM +0100, Jaro Reinders wrote:

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

No. The safety depends on careful Safe/Unsafe marking of an unmanageable and growing set of modules. How does GHC know that "Data.ByteString.Unsafe" is actually "unsafe" in the sense of "Safe" Haskell? λ> BS.index x 10 *** Exception: Data.ByteString.index: index too large: 10, length = 6 CallStack (from HasCallStack): error, called at libraries/bytestring/Data/ByteString.hs:2026:23 in bytestring-0.11.3.1:Data.ByteString moduleError, called at libraries/bytestring/Data/ByteString.hs:1232:24 in bytestring-0.11.3.1:Data.ByteString index, called at <interactive>:7:1 in interactive:Ghci3 λ> import Data.ByteString.Unsafe as UBS λ> UBS.unsafeIndex x 30000 27 λ> UBS.unsafeIndex x 1000000 162 λ> UBS.unsafeIndex x 10000000 185 λ> UBS.unsafeIndex x 100000000 Segmentation fault (core dumped) This is too brittle to be safe on an ongoing basis in practice. -- Viktor.

I hope that some effort can be expended to specifically identify what changes would be necessary to make Safe Haskell work consistent with its name. Only then can a reasoned decision about how to proceed be made. Also, rejecting the status quo implies that making a decision is a high priority. Is it really that urgent? If Safe Haskell isn't being used much, then why hurry to fix it or kill it? On Tue, 2022-12-27 at 20:33 -0700, Chris Smith wrote:

Thanks for writing this up!

I was a user of SafeHaskell briefly in 2011-2012, and it certainly has theoretical benefits.  That said, though, I agree that the balance of the cost-benefit analysis is solidly against it, and I would much rather ease the burden of GHC and library development than continue to maintain a burdensome niche feature with limited users.

That said, I think some of the comments in this thread are unnecessarily dismissive of SafeHaskell's usefulness and correctness.  So here are a few things worth keeping in mind:

1. The strict type safety aspect of SafeHaskell is, in fact, the mechanism that makes SafeHaskell effective at controlling effects through limited IO access.  You simply cannot have the latter without the former.  Generalized newtype deriving, for example, is incompatible with SafeHaskell precisely because it can be used to break restricted IO access. It looks like a lot of the responses here ignore that SafeHaskell did a lot of work to make runtime-cost-free safe execution reliable, then make hand-wavy references to other systems that don't do any of that, and use that as a basis for asserting distrust in SafeHaskell.  That's entirely unfair. 2. The assertion that safety in SafeHaskell depends on the correctness of a bunch of libraries assertions about their safety reveals a fundamental lack of understanding of how SafeHaskell works.  Safety is inferred compositionally from the source code and the safety of the modules it uses, and a source code annotation about safety can never compromise the safety guarantees of SafeHaskell.  The only thing that can compromise safety is a misplaced trust decision.  Trust decisions are not in the source code at all.  They are made outside the source by running `ghc-pkg trust`.

This conversation reminds me of a parable I encountered somewhere, in which someone declares "I don't understand why this decision was ever made, and I we should change it", and someone responds, "No, if you don't understand the decision was made, then you don't know enough to change it.  If you learn why it was decided that way in the first place, then you will have the understanding to decide whether to change it."  Just like in the parable, I am not disagreeing with the idea of deprecating SafeHaskell, but I am skeptical that the decision should be made on the basis of misrepresentations and crude analogies that completely miss what's unique and interesting about SafeHaskell in the first place. 

On Tue, Dec 27, 2022, 10:10 AM Hécate wrote:

...

Hi everyone, and happy holidays.

I am looking into whether or not Safe Haskell is still worth maintaining.

Currently there are two sides on which Safe Haskell hurts us:

1. GHC Development 2. Library development

For point n°1: You can easily take the measure of what Safe Haskell raises in GHC as of today by visiting the bug tracker¹ and see that for example Unboxed Types cannot be used because their home modules (GHC.Prim and GHC.Types) are marked as Unsafe. Moreover, interactions between GHC2021 and Safe make the latter quite unpleasant to work with².

Regarding point n°2: Safe Haskell is badly integrated within our existing frameworks for API compatibility. Neither the PVP nor the extension's documentation mention compatibility, or define what stance we should take. Thus we are bound to fight on the letter versus the spirit of the PVP (which is not an unreasonable debate since there is no formalism anywhere). This provokes debates without clear resolution beyond "Friend don't let friends use {-# Safe #-}"³

Now I am not saying that Safe Haskell does not bring any kind of good idea, far from it.

However there are two things that live inside Safe Haskell that would benefit from being separated:

1. Strict type-safety

2. Restricted IO

A lot of the public use-cases of Safe Haskell seem to be on the "Restricted IO", such as Lambdabot and other code evaluators out there.

It's a fairly reasonable feature, I'd even say it's something that we should be publicising more when speaking about GHC's more advanced  features. However, "Strict type-safety" seems to be the root of many problems that we encounter downstream. A lot of it stems from GeneralizedNewtypeDeriving being marked as unsafe (under point 1), which is fair enough, but we've had DerivingVia not marked as Safe until May 2021, which reveals a big problem: Options have to be marked as forbidden under Safe to be caught, which leaves a lot of work to the human factor of GHC development.

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?

¹ https://gitlab.haskell.org/ghc/ghc/-/issues/?label_name%5B%5D=Safe%20Haskell

² https://gitlab.haskell.org/ghc/ghc/-/issues/19605

³ https://github.com/haskell/directory/issues/147

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

The only part of Safe Haskell I ever really cared about was type safety. That's what matters, I think. I've wanted to use it a number of times and played with it, but it's never actually managed to become an important part of anything for me. So take that as you will. I'd love it if it worked well, its issues have limited what I attempt, but at the end of the day it's never hurt me too bad to not have it. -davean On Wed, Dec 28, 2022 at 7:14 AM Tom Ellis < tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> wrote:

On Tue, Dec 27, 2022 at 08:33:04PM -0700, Chris Smith wrote:

...

This conversation reminds me of a parable I encountered somewhere, in which someone declares "I don't understand why this decision was ever made, and I we should change it", and someone responds, "No, if you don't understand the decision was made, then you don't know enough to change it. If you learn why it was decided that way in the first place, then you will have the understanding to decide whether to change it."

That parable is Chesterton's fence:

https://en.wikipedia.org/wiki/G._K._Chesterton#Chesterton's_fence _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

I do agree that Safe Haskell would be useful even if it was only used for enforcing type safety and avoiding accidental use of unsafe features, but the paper [1] makes it quite clear that one of the main goals is to safely execute untrusted code: "Safe Haskell makes it possible to confine and safely execute untrusted, possibly malicious code. By strictly enforcing types, Safe Haskell allows a variety of different policies from API sandboxing to information-flow control to be implemented easily as monads. [..] We use Safe Haskell to implement an online Haskell interpreter that can securely execute arbitrary untrusted code with no overhead." Cheers, Jaro [1] https://www.scs.stanford.edu/~dm/home/papers/terei:safe-haskell.pdf On 13-01-2023 18:06, Carter Schonwald wrote:

Indeed type safety is exactly what it’s for! The other notions of safety were never part of the goals. And it was designed so that the end user could decide which codes they deem trustworthy.

On Wed, Dec 28, 2022 at 6:04 PM davean mailto:davean@xkcd.com> wrote:

The only part of Safe Haskell I ever really cared about was type safety. That's what matters, I think.

I've wanted to use it a number of times and played with it, but it's never actually managed to become an important part of anything for me. So take that as you will. I'd love it if it worked well, its issues have limited what I attempt, but at the end of the day it's never hurt me too bad to not have it.

-davean

On Wed, Dec 28, 2022 at 7:14 AM Tom Ellis mailto:tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> wrote:

On Tue, Dec 27, 2022 at 08:33:04PM -0700, Chris Smith wrote: > This conversation reminds me of a parable I encountered somewhere, in which > someone declares "I don't understand why this decision was ever made, and I > we should change it", and someone responds, "No, if you don't understand > the decision was made, then you don't know enough to change it.  If you > learn why it was decided that way in the first place, then you will have > the understanding to decide whether to change it."

That parable is Chesterton's fence:

https://en.wikipedia.org/wiki/G._K._Chesterton#Chesterton's_fence https://en.wikipedia.org/wiki/G._K._Chesterton#Chesterton's_fence _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org mailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org mailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs