Is Safe Haskell intended to allow segfaults?

[Ryan Newton]

Hi Ed,

Thanks, I went back to the paper and read those sections.

It sounds like this design heavily reflects the untrusted-code use case.  I
believe ceding the entire IO monad is too pessimistic, and it's also
against the *spirit* of the type safety guarantee mentioned in the paper:

"Type safety. In Milner’s famous phrase, well-typed programs do not go
wrong. "
There's not really very much discussion of this "punting on IO" decision in
the paper.  The paper mentions not deleting users files as an example of a
higher level security policy -- and a reason not  to try to lock down IO --
but that's not really the issue here.

Sure, there are many use cases that require an RIO newtype, but the memory
model and memory protection are really internal to the language.  My
interest is in a type safe language with a memory model *in the IO monad*.
I think it's quite *reasonable to expect Safe Haskell to be as safe as
Java! * There are hundreds of thousands or millions of lines of code
written in the IO monad [1], and a lot of that code could probably be
memory safe by construction.

One question I have for people is which of the following they would favor:

   1. Redefine -XSafe to guarantee something about IO and its memory safety
   (and even its memory model)
   2. Add a fourth safety level, "SafeExceptIO", that corresponds to the
   current guarantees, while extending "Safe" to say something about IO.
   3. Leave safe Haskell as it is.

(2) sounds a bit clunky to me, and I favor (1) most of all.

Best,
  -Ryan

[1] 17M lines on hackage total, hard to count how much is in an IO monad or
related monad.


On Mon, Aug 8, 2016 at 2:05 PM, Edward Z. Yang <ezyang at mit.edu> wrote:

> Hello Ryan,
>
> The guarantee that Safe Haskell gives with regards to IO is a little
> subtle and is mentioned in Section 3.1 of the paper, and detailed
> in Section 5.1. Essentially, to use Safe Haskell, you are responsible
> for defining the type at which untrusted code is to be called.
> Using an untrusted value at type IO a in main imposes no safety
> restrictions by design--it's up to the user of Safe Haskell to
> decide what kind of security properties it needs out of user code.
>
> Edward
>
> Excerpts from Ryan Newton's message of 2016-08-08 13:27:16 -0400:
> > 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160808/71531420/attachment-0001.html>