Is Safe Haskell intended to allow segfaults?

Wed Aug 10 08:24:21 UTC 2016

Right - Safe Haskell provides the minimum that you need to be able to
safely run untrusted code: the ability to trust the type system and the
module system.  Definining a safe subset of IO is usually  an
application-specific decision, e.g. do you want to allow access to the
filesystem but without allowing openFile "/dev/mem"?  It's a minefield.

Ryan, if you want to give an operational semantics for memory in IO, why
not start from the subset of IO that you can accurately model - the basic
IO structure together with a set of primitives - and define the semantics
for that?  That's typically what we do when we're talking about something
in the IO monad.

Cheers
Simon

On 10 August 2016 at 04:58, Edward Kmett <ekmett at gmail.com> wrote:

> I see three major stories here:
>
> 1.) If you remove IO from being able to be compiled inside Safe code _at
> all_ most packages I have that bother to expose Safe information will have
> to stop bothering. I'd have to cut up too many APIs into too many
> fine-grained pieces. This would considerably reduce the utility of Safe
> Haskell to me. Many of them expose a few combinators here and there that
> happen to live in IO and I can view offering Safe or Trustworthy to users
> as a 'the pure stuff looks really pure' guarantee. For the most part it
> 'just works' and Trustworthy annotations can be put in when I know the
> semantics of the hacks I'm using under the hood.
>
> 2.) Assuming instead that you're talking about a stronger-than-Safe
> additional language extension, say ReallySafe or SafeIO, it all comes down
> to what the user is allowed to do in IO, doesn't it? What effects are users
> granted access to? We don't have a very fine-grained system for IO-effect
> management, and it seems pretty much any choice you pick for what to put in
> the sandbox will be wrong for some users, so you'd need some sort of pragma
> for each IO operation saying what bins it falls into and to track that
> while type checking, etc. At least then you could say what you are safe
> with respect to. That all seems to be rather a big mess, roughly equivalent
> to modeling an effect system for IO operations, and then retroactively
> categorizing everything, putting a big burden on maintainers and requiring
> a lot of community buy-in, sight unseen.
>
> 3.) On the other hand, someone could _build_ an effect system in Haskell
> that happens to sit on top of IO, holding effects in an HList, undischarged
> nullary class constraint, etc. then pull a couple of Trustworthy modules
> around it for embedding the effects they want to permit and build this
> today without any compiler support, they'd just have to make a final
> application-specific Trustworthy wrapper to run whatever effects they want
> to permit into their program. It is more invasive to the code in question,
> but it requires zero community organizing and we've already got all the
> compiler mojo we need. The downside is the Trustworthy wrappers at the
> bottom of the heap and that it doesn't interoperate with basically anything
> already written.
>
> -Edward
>
> On Tue, Aug 9, 2016 at 10:45 PM, Ryan Newton <rrnewton at gmail.com> wrote:
>
>> I'm hearing that Safe Haskell is great for pure use cases (lambda bot).
>> But that doesn't depend on being able to write arbitrary IO code inside the
>> Safe bubble, does it?  In fact *all* of IO could be outside the safe
>> boundary for this use case, could it not?  Are there any existing cases
>> where it is important to be able to build up unsafe IO values inside -XSafe
>> code?
>>
>> Edward, why does it seem like a losing proposition?  Are there further
>> problems that come to mind?  ezyang mentioned the subprocess problem.  I
>> don't have a strong opinion on that one.  But I tend to think the safe IO
>> language *should* allow subprocess calls, and its a matter of
>> configuring your OS to not allow ptrace in that situation.  This would be
>> part of a set of requirements for how to compile and launch a complete
>> "Safe Haskell" *program* in order to get a guarantee.
>>
>> My primary interest is actually not segfault-freedom, per-se, but being
>> able to define a memory model for Safe Haskell (for which I'd suggest
>> sequential consistency).  FFI undermines that, and peek/poke seems like it
>> should cluster with FFI as an unsafe feature.  I'm not inclined to give a
>> memory model to peek or FFI -- at that level you get what the architecture
>> gives you -- but I do want a memory model for IORefs, IOVectors, etc.
>>
>> We're poking at the Stackage package set now to figure out what pressure
>> point to push on to increase the percentage of Stackage that is Safe.  I'll
>> be able to say more when we have more data on dependencies and problem
>> points.  Across all of hackage, Safe Haskell has modest use: of the ~100K
>> modules on Hackage, ~636 are marked Safe, ~874 trustworthy, and ~118
>> Unsafe.  It should be easy to check if any of this Safe code is currently
>> importing "Foreign.*" or using FFI.
>>
>> My general plea is that we not give the imperative partition of Haskell
>> too much the short end of the stick [1]. There is oodles of code in IO (or
>> MonadIO), and probably relatively little in "RIO".  To my knowledge, we
>> don't have great ways to coin "RIO" newtypes without having to wrap and
>> reexport rather a lot of IO functions.  Maybe if APIs like MVars or files
>> were overloaded in a class then GND could do some of the work...
>>
>>   -Ryan
>>
>> [1] In safety guarantees, in optimizations, primops, whatever...  For
>> instance, I find in microbenchmarks that IO code still runs 2X slower than
>> pure code, even if no IO effects are performed.
>>
>>
>>
>> On Tue, Aug 9, 2016 at 5:13 PM, Edward Kmett <ekmett at gmail.com> wrote:
>>
>>> I've always treated Safe Haskell as "Safe until you allow IO" -- in that
>>> all 'evil' things get tainted by an IO type that you can't get rid of by
>>> the usual means. So if you go to run pure Safe Haskell code in say,
>>> lambdabot, which doesn't give the user a means to execute IO, it can't
>>> segfault if all of the Trustworthy modules you depend upon actually are
>>> trustworthy.
>>>
>>> Trying to shore up segfault safety under Safe in IO seems like a losing
>>> proposition.
>>>
>>> -Edward
>>>
>>> On Mon, Aug 8, 2016 at 1:27 PM, Ryan Newton <rrnewton at gmail.com> wrote:
>>>
>>>> We're trying to spend some cycles pushing on Safe Haskell within the
>>>> stackage packages.  (It's looking like a slog.)
>>>>
>>>> But we're running up against some basic questions regarding the core
>>>> packages and Safe Haskell guarantees.  The manual currently says:
>>>> <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/safe_haskell.html#safe-language>
>>>>
>>>>
>>>> *Functions in the IO monad are still allowed and behave as usual. *
>>>> As usual?  So it is ok to segfault GHC?  Elsewhere it says "in the safe
>>>> language you can trust the types", and I'd always assumed that meant Safe
>>>> Haskell is a type safe language, even in the IO fragment.
>>>>
>>>> Was there an explicit decision to allow segfaults and memory
>>>> corruption?  This can happen not just with FFI calls but with uses of Ptrs
>>>> within Haskell, for example the following:
>>>>
>>>>
>>>> ```
>>>>
>>>> {-# LANGUAGE Safe #-}
>>>>
>>>> module Main where
>>>>
>>>> import Foreign.Marshal.Alloc
>>>>
>>>> import Foreign.Storable
>>>>
>>>> import Foreign.Ptr
>>>>
>>>> import System.Random
>>>>
>>>>
>>>> fn :: Ptr Int -> IO ()
>>>>
>>>> fn p = do
>>>>
>>>>   -- This is kosher:
>>>>
>>>>   poke p 3
>>>>
>>>>   print =<< peek p
>>>>
>>>>   -- This should crash the system:
>>>>
>>>>   ix <- randomIO
>>>>
>>>>   pokeElemOff p ix 0xcc
>>>>
>>>>
>>>>
>>>> main = alloca fn
>>>>
>>>> ```
>>>>
>>>>
>>>>   -Ryan
>>>>
>>>> _______________________________________________
>>>> ghc-devs mailing list
>>>> ghc-devs at haskell.org
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>>>
>>>>
>>>
>>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://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/20160810/43e4e685/attachment-0001.html>