Re: Is Safe Haskell intended to allow segfaults?

* Mikhail Glushenkov: > Hi, > > On 9 August 2016 at 01:32, David Terei wrote: >> 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

Re: Is Safe Haskell intended to allow segfaults?

On 2016-08-12 20:37, Edward Kmett wrote: > What about consuming Storable Vectors carefully, or simply working > parameterized over vector type, where Storable vectors are one of the > options? > There was actually a great paper about a very similar thing (i.e. "here's the usual interface" vs.

Re: Is Safe Haskell intended to allow segfaults?

What about consuming Storable Vectors carefully, or simply working parameterized over vector type, where Storable vectors are one of the options? -Edward On Fri, Aug 12, 2016 at 12:58 PM, Ryan Newton wrote: > Yes, it is peek and poke that are dangerous. It was

Re: Is Safe Haskell intended to allow segfaults?

Yes, it is peek and poke that are dangerous. It was Foreign.Storable that I wanted to mark as Unsafe. But we do sometimes run into examples where there's an A and a B, and if you import both, you can make A+B which blows up. So preventing access to A+B may mean arbitrarily marking one or the

Re: Is Safe Haskell intended to allow segfaults?

As for a sample list of modules, let's just start with your very first example, Foreign.Ptr: In and of itself nothing in Foreign.Ptr is unsafe! It allows a bit of arithmetic on a type you can't actually use with anything, and provides an IO action mixed into an otherwise pure module that happens

Re: Is Safe Haskell intended to allow segfaults?

Hi Simon, On Wed, Aug 10, 2016 at 4:24 AM, Simon Marlow > wrote: > 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 >

Re: Is Safe Haskell intended to allow segfaults?

Hi Ryan, I have similar concerns with safety and STM. In particular, lazy validation allows for execution after inconsistent reads from TVars. The obvious problem to avoid is falling into an infinite loop. As long as -fno-omit-yields is used (on every module?) and maybe some other conditions

Re: Is Safe Haskell intended to allow segfaults?

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

Re: Is Safe Haskell intended to allow segfaults?

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

Re: Is Safe Haskell intended to allow segfaults?

Heh, ok, segfaults themselves are a red herring. More precisely: The operational semantics for a SafeIO language should always accurately model its memory state. The application should not compute (take a step in the semantics) in a way that exposes corrupt memory or arbitrary undefined

Re: Is Safe Haskell intended to allow segfaults?

On Tue, Aug 9, 2016 at 4:19 PM, Edward Z. Yang wrote: > If you can execute subprocesses, you could always spawn gdb to > attach via ptrace() to the parent process and then poke around > memory. > Don't even need that if you're just talking segfaults, you can always spawn a

Re: Is Safe Haskell intended to allow segfaults?

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

Re: Is Safe Haskell intended to allow segfaults?

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

Re: Is Safe Haskell intended to allow segfaults?

If you can execute subprocesses, you could always spawn gdb to attach via ptrace() to the parent process and then poke around memory. Yes this is a "dumb" example but I think it goes to show how important it is to correctly characterize what the threat model is. A "no-segfault" fragment of

Re: Is Safe Haskell intended to allow segfaults?

On Mon, Aug 8, 2016 at 8:46 PM, Mikhail Glushenkov wrote: > > Yes, this can be done with JNI, see e.g. [1]. Additionally, by using > sun.misc.Unsafe [2], one can cause segfaults even from pure Java. > [1] https://www.cs.princeton.edu/~appel/papers/safejni.pdf > [2]

Re: Is Safe Haskell intended to allow segfaults?

Hi, On 9 August 2016 at 01:32, David Terei wrote: > 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

Re: Is Safe Haskell intended to allow segfaults?

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',

Re: Is Safe Haskell intended to allow segfaults?

I think what you are proposing is reasonable. I wasn't present when Safe Haskell's design was originally fleshed out so I don't know why this route wasn't taken. Edward Excerpts from Ryan Newton's message of 2016-08-08 16:00:38 -0400: > Hi Ed, > > Thanks, I went back to the paper and read

Re: Is Safe Haskell intended to allow segfaults?

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

Re: Is Safe Haskell intended to allow segfaults?

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

Re: Is Safe Haskell intended to allow segfaults?

> > Pretty sure it's impossible to allow IO without enabling all of it one way > or another. And as soon as you allow *any* IO, you're open to various kinds > of failures including segfaults. The only way you will get your type system > to prevent that is fully specified dependent typing both in

Re: Is Safe Haskell intended to allow segfaults?

On Mon, Aug 8, 2016 at 1:27 PM, Ryan Newton wrote: > 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. Pretty sure