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
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs