Is Safe Haskell intended to allow segfaults?

[David Terei]

Thanks for bringing this up Ryan, it's an interesting direction of thought.

It's been a while since we originally designed SafeHaskell, so I can't
remember our thinking very well with this area. I believe it came down
to the following:

* Our primary concern was to be able to 'trust the types', which is
perhaps a little weaker than 'type safety'. So IO can do ugly things,
but at least we know that, and know what something without IO, or
using a restricted IO monad can do.
* Our intuition was that offering stronger guarantees about IO would
be very difficult -- I don't remember how far we explored this
intuition.
* We were also motivated very strongly by the security use case, that
may have sadly blinded us a little to something more ambitious as you
propose.

If you have the energy, it'd be great to put some of this thinking
into a wiki page (https://ghc.haskell.org/trac/ghc/wiki/SafeHaskell)
and flesh out a first approximation of what IO API's cause issues. Is
it just Ptr not carrying bounds around with it? Maybe, but then we
need to secure how Ptr's can be created, which excludes FFI returning
Ptr's.

I imagine in Java, that I can construct an invalid pointer in foreign
code, and then cause segfaults without the Java code having any
issues. Just guessing at this, so very interested to know how it's
prevented if I can't.

Securing the memory model may be very challenging. E.g., as Russ Cox
points out, in Go one can use a data race to break type safety. Does
GHC-Haskell have any similar issues? What performance impact would
result from fixing these edge cases?

http://research.swtch.com/gorace

I think your (1) proposal is reasonable and desirable, but we'd really
want to understand the difficulty further to guide us between 1--3.

Cheers,
David

On 8 August 2016 at 13:00, Ryan Newton <rrnewton at gmail.com> wrote:
> 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:
>
> Redefine -XSafe to guarantee something about IO and its memory safety (and
> even its memory model)
> Add a fourth safety level, "SafeExceptIO", that corresponds to the current
> guarantees, while extending "Safe" to say something about IO.
> 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
>
>