isaacdupree:
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
Donald Bruce Stewart wrote:
Lambdabot uses 1) type guarantee of no-IO at the top level, along with 2) a trusted module base (pure module only, that are trusted to not export evil things), as well as 3) restricting only to H98-language only (things like TH can, and have been, exploited, for example).
And lambdabot's only allowing _expressions_, so GHC's (former?) vulnerability to instances of Ix that return out-of-bounds indexes did not affect it.
Oh yes, it only allows expressions (how could I forget that?), meaning also that, for example, crafty newtype recursion is disallowed. And of course, no evil Ix instances. Oh, also, there's another exploit using a variety crafty expressions that trigger pathological type inference behaviour, causing the type checker to effectively lock up the system. (One is particularly easy to come up with...). There's really a lot of things to watch out for, actually. We should document all the interesting exploits that have been found over the years!
There are some extensions that are safe... explicit forall, rank-N types, etc... which can be enabled on an "opt-in" basis so that only safe ones are chosen?
We could do that (explicit forall is probably the most requested). Currently we only allow -fextended-defaulting, (giving ghci like defaulting). -- Don