<div dir="ltr"><div>I do find it scary, but I personally am in no position to express opinion on what should happen (I'm not on any committee and I'm not even a regular Haskell user).</div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, 9 Jul 2018 at 05:08, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">That's a very scary, albeit contrived, example. I wonder if there are more realistic functions that are susceptible to this attack from "safe" Haskell. In light of your exploit, I'm leaning toward saying we probably *should* fix this, but I'd like to hear your opinion.</div><br><div class="gmail_quote"><div dir="ltr">On Sun, Jul 8, 2018, 6:51 PM Arseniy Alekseyev <<a href="mailto:arseniy.alekseyev@gmail.com" target="_blank">arseniy.alekseyev@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><font face="arial, helvetica, sans-serif">This might be just me expecting too much guarantees from ST monad, but it seems to me that this is a potential violation of memory-safety.</font></div><div><font face="arial, helvetica, sans-serif">Consider the program below.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">The use of [</font><font face="monospace, monospace">unsafeWrite</font><font face="arial, helvetica, sans-serif">] in [<span style="font-family:monospace,monospace;font-size:small;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">silly_function</span>] is guarded by the code above (we know we wrote [sz] so we should read back [</font><font face="monospace, monospace">sz</font><font face="arial, helvetica, sans-serif">]). It ought to be safe if you can rely on sequential execution of ST monad with no preemption.</font></div><div><font face="arial, helvetica, sans-serif">However, it does end up preempted due to the use of [mfix] elsewhere in the program, which leads to a segmentation fault.</font></div><div><br></div><div><div><font face="monospace, monospace">import <a href="http://Data.Array.ST" rel="noreferrer" target="_blank">Data.Array.ST</a></font></div><div><font face="monospace, monospace">import Data.Array.Base</font></div><div><font face="monospace, monospace">import Control.Monad.ST.Strict</font></div><div><font face="monospace, monospace">import Control.Monad.Fix</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">silly_function :: STArray s Int Int -> Int -> ST s ()</font></div><div><font face="monospace, monospace">silly_function arr a = do</font></div><div><font face="monospace, monospace"> (0, sz) <- getBounds arr</font></div><div><font face="monospace, monospace"> writeArray arr 0 sz</font></div><div><font face="monospace, monospace"> let !res = a</font></div><div><font face="monospace, monospace"> sz <- readArray arr 0</font></div><div><font face="monospace, monospace"> unsafeWrite arr sz res</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">foo :: ST s Int</font></div><div><font face="monospace, monospace">foo = do</font></div><div><font face="monospace, monospace"> arr <- newArray (0, 10) 0</font></div><div><font face="monospace, monospace"> mfix $ \res -> do</font></div><div><font face="monospace, monospace"> n <- readArray arr 0</font></div><div><font face="monospace, monospace"> writeArray arr 0 1000000000</font></div><div><font face="monospace, monospace"> if n > 0</font></div><div><font face="monospace, monospace"> then</font></div><div><font face="monospace, monospace"> return 666</font></div><div><font face="monospace, monospace"> else do</font></div><div><font face="monospace, monospace"> silly_function arr res</font></div><div><font face="monospace, monospace"> readArray arr 10</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">main = print $ runST foo</font></div></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Sun, 8 Jul 2018 at 22:26, Levent Erkok <<a href="mailto:erkokl@gmail.com" rel="noreferrer" target="_blank">erkokl@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi David,<div><br></div><div>Wonderful example. I'm afraid no-eager-blackholing also breaks the "no spooky action at a distance" rule. Since `x` is not used recursively, we should be able to pull it out of the `mfix` call, transforming the original to:</div><div><br></div><div><div>foo :: ST s Int</div><div>foo = do</div><div> ref <- newSTRef True</div><div> x <- readSTRef ref</div><div> mfix $ \res -> do</div><div> if x</div><div> then do</div><div> writeSTRef ref False</div><div> return $! res + 5 -- force the final result</div><div> else return 10</div></div><div><br></div><div>I believe this variant will produce <<loop>> with or without eager-blackholing, as it should. By this argument alone, I'd say the no-eager-blackholing breaks mfix axioms for strict-state.</div><div><br></div><div>This example is also interesting from a pure termination point of view: Moving things "out-of" mfix usually improves termination. In this case, the opposite is happening.</div><div><br></div><div>Strictly speaking, this is in violation of the mfix-axioms. But I doubt it's worth losing sleep over. I suggest we add this as an example in the value-recursion section on how eager-blackholing can change things.</div><div><br></div><div>Cheers,</div><div><br></div><div>-Levent.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jul 8, 2018 at 9:40 AM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" rel="noreferrer" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">I filed a ticket[*] for this, but I think maybe the libraries list should weigh in on whether it is something that should be fixed. In general, fixST f is supposed to bottom out if f forces its argument. However, the lazy way GHC blackholes thunks under evaluation sometimes leads to the computation being run again. In certain contrived situations, this can allow the computation to succeed!<div dir="auto"><br></div><div dir="auto">The example I give in the ticket:</div><div dir="auto"><br></div><div dir="auto"><div dir="auto">import Control.Monad.ST.Strict</div><div dir="auto">import Control.Monad.Fix</div><div dir="auto">import Data.STRef</div><div dir="auto"><br></div><div dir="auto">foo :: ST s Int</div><div dir="auto">foo = do</div><div dir="auto"> ref <- newSTRef True</div><div dir="auto"> mfix $ \res -> do</div><div dir="auto"> x <- readSTRef ref</div><div dir="auto"> if x</div><div dir="auto"> then do</div><div dir="auto"> writeSTRef ref False</div><div dir="auto"> return $! res + 5 -- force the final result</div><div dir="auto"> else return 10</div><div dir="auto"><br></div><div dir="auto">main = print $ runST foo</div><div dir="auto"><br></div><div dir="auto">Here, the computation writes to an STRef before forcing the final result. Forcing the final result causes the computation to run again, this time taking the other branch. The program prints 15. When compiled with -O -feager-blackholing, however, the expected <<loop>> exception occurs.</div><div dir="auto"><br></div><div dir="auto">As far as I know, this weirdness never changes the value produced by a non-bottoming computation, and never changes a non-bottoming computation into a bottoming one. The fix (defining fixST the way fixIO is currently defined) would have a slight performance impact. Is it worth it?</div></div><div dir="auto"><br></div><div dir="auto"><div dir="auto"><div dir="auto">[*] <a href="https://ghc.haskell.org/trac/ghc/ticket/15349" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/ticket/15349</a></div></div></div></div>
<br>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>
</blockquote></div>
</blockquote></div>