Changes to Safe Haskell documentation from feedback (#10140).
authorDavid Terei <code@davidterei.com>
Tue, 10 Mar 2015 03:55:52 +0000 (20:55 -0700)
committerDavid Terei <code@davidterei.com>
Tue, 10 Mar 2015 03:55:52 +0000 (20:55 -0700)
docs/users_guide/safe_haskell.xml

index 634482a..f0d3bde 100644 (file)
@@ -7,23 +7,23 @@
   Safe Haskell is an extension to the Haskell language that is implemented in
   GHC as of version 7.2. It allows for unsafe code to be securely included in a
   trusted code base by restricting the features of GHC Haskell the code is
-  allowed to use. Put simply, it makes the types of programs trustable. Safe
-  Haskell is aimed to be as minimal as possible while still providing strong
-  enough guarantees about compiled Haskell code for more advance secure systems
-  to be built on top of it.
+  allowed to use. Put simply, it makes the types of programs trustable.
   </para>
 
   <para>
-  While this is the use case that Safe Haskell was motivated by it is important
-  to understand that what Safe Haskell is tracking and enforcing is a stricter
-  form of type safety than is usually guaranteed in Haskell. As part of this,
-  Safe Haskell is run during every compilation of GHC, tracking safety and
-  inferring it even for modules that don't explicitly use Safe Haskell. Please
-  refer to section <xref linkend="safe-inference"/> for more details of this.
-  This also means that there are some design choices that from a security point
-  of view may seem strange but when thought of from the angle of tracking type
-  safety are logical. Feedback on the current design and this tension between
-  the security and type safety view points is welcome.
+  While a primary use case of Safe Haskell is running untrusted code, Safe
+  Haskell doesn't provide this directly. Instead, Safe Haskell provides strict
+  type safety. Without Safe Haskell, GHC allows many exceptions to the type
+  system which can subvert any abstractions. By providing strict type safety,
+  Safe Haskell enables developers to build from their own library level sandbox
+  mechanisms to run untrusted code.
+  </para>
+
+  <para>
+  While Safe Haskell is an extension, it actually runs in the background for
+  every compilation with GHC. It does this to infer the type violations of
+  modules, even when they aren't explicitly using Safe Haskell. Please refer to
+  section <xref linkend="safe-inference"/> for more details of this.
   </para>
 
   <para>
@@ -48,7 +48,7 @@
   Safe Haskell, however, <emphasis>does not offer</emphasis> compilation
   safety. During compilation time it is possible for arbitrary processes to be
   launched, using for example the <link linkend="pre-processor">custom
-    pre-processor</link> flag. This can be manipulated to either compromise a
+  pre-processor</link> flag. This can be manipulated to either compromise a
   users system at compilation time, or to modify the source code just before
   compilation to try to alter set Safe Haskell flags. This is discussed further
   in section <xref linkend="safe-compilation"/>.
       <title>Strict type-safety (good style)</title>
 
       Haskell offers a powerful type system and separation of pure and
-      effectual functions through the <literal>IO</literal> monad. There are
-      several loop holes in the type system though, the most obvious offender
-      being the <literal>unsafePerformIO :: IO a -> a</literal> function. The
-      safe language dialect of Safe Haskell disallows the use of such
-      functions. This can be useful for a variety of purposes as it makes
+      effectual functions through the <literal>IO</literal> monad. However,
+      there are several loop holes in the type system, the most obvious
+      offender being the <literal>unsafePerformIO :: IO a -> a</literal>
+      function. The safe language dialect of Safe Haskell disallows the use of
+      such functions. This can be useful for a variety of purposes as it makes
       Haskell code easier to analyse and reason about. It also codifies an
       existing culture in the Haskell community of trying to avoid using such
       unsafe functions unless absolutely necessary. As such using the safe
       <para>
       Systems such as information flow control security, capability based
       security systems and DSLs for working with encrypted data.. etc can be
-      built in the Haskell language simply as a library. However they require
-      guarantees about the properties of the Haskell language that aren't true
-      in the general case where uses of functions like <literal>unsafePerformIO
-      </literal> are allowed. Safe Haskell is designed to give users enough
-      guarantees about the safety properties of compiled code so that such
-      secure systems can be built.
+      built in the Haskell language as a library. However they require
+      guarantees about the properties of Haskell that aren't true in general
+      due to the presence of functions like <literal>unsafePerformIO
+      </literal>. Safe Haskell gives users enough guarantees about the type
+      safety of compiled code so that they can build such secure systems.
       </para>
 
       <para>
-      As an example lets define an interface for a plugin system where the
+      As an example, lets define an interface for a plugin system where the
       plugin authors are untrusted, possibly malicious third-parties. We do
       this by restricting the plugin interface to pure functions or to a
-      restricted <literal>IO</literal> monad that we have defined that only
-      allows a safe subset of <literal>IO</literal> actions to be executed. We
-      define the plugin interface here so that it requires the plugin module,
+      restricted <literal>IO</literal> monad that we have defined. The
+      restricted <literal>IO</literal> monad will only allow a safe subset of
+      <literal>IO</literal> actions to be executed. We define the plugin
+      interface so that it requires the plugin module,
       <literal>Danger</literal>, to export a single computation,
       <literal>Danger.runMe</literal>, of type <literal>RIO ()</literal>, where
       <literal>RIO</literal> is a new monad defined as follows:
       </para>
 
       <programlisting>
-        -- Either of the following Safe Haskell pragmas would do
-        {-# LANGUAGE Trustworthy #-}
+        -- While we use `Safe', the `Trustworthy' pragma would also be
+        -- fine. We simply want to ensure that:
+        -- 1) The module exports an interface that untrusted code can't
+        --    abuse.
+        -- 2) Untrusted code can import this module.
+        --
         {-# LANGUAGE Safe #-}
 
         module RIO (RIO(), runRIO, rioReadFile, rioWriteFile) where
           if ok then writeFile file contents else return ()
       </programlisting>
 
-      We compile Danger using the new Safe Haskell <option>-XSafe</option> flag:
+      We compile <literal>Danger</literal> using the new Safe Haskell
+      <option>-XSafe</option> flag:
 
       <programlisting>
         {-# LANGUAGE Safe #-}
       </programlisting>
 
       <para>
-      Before going into the Safe Haskell details, lets point out some of
-      the reasons this design would fail without Safe Haskell:
+      Before going into the Safe Haskell details, lets point out some of the
+      reasons this security mechanism would fail without Safe Haskell:
       </para>
 
       <itemizedlist>
           Unfortunately Template Haskell can be used to subvert module
           boundaries and so could be used to gain access to this constructor.
         </listitem>
-        <listitem>There is no way to place restrictions on the modules that
-          the untrusted Danger module can import. This gives the author of
-          Danger a very large attack surface, essentially any package
-          currently installed on the system. Should any of these packages
-          have a vulnerability then the Danger module can exploit this. The
-          only way to stop this would be to patch or remove packages with
-          known vulnerabilities even if they should only be used by
-          trusted code such as the RIO module.
+        <listitem>There is no way to place restrictions on the modules that the
+          untrusted Danger module can import. This gives the author of Danger a
+          very large attack surface, essentially any package currently
+          installed on the system. Should any of these packages have a
+          vulnerability then the Danger module can exploit this.
         </listitem>
       </itemizedlist>
 
       <para>
       To stop these attacks Safe Haskell can be used. This is done by compiling
-      the RIO module with the <option>-XTrustworthy</option> flag and compiling
-      the Danger module with the <option>-XSafe</option> flag.
+      the RIO module with the <option>-XSafe</option> or
+      <option>-XTrustworthy</option> flag and compiling the Danger module with
+      the <option>-XSafe</option> flag.
       </para>
 
       <para>
       </para>
 
       <para>
-      This is why the RIO module is compiled with
-      <option>-XTrustworthy</option>, to allow the Danger module to import it.
+      This is why the RIO module is compiled with <option>-XSafe</option> or
+      <option>-XTrustworthy</option>>, to allow the Danger module to import it.
       The <option>-XTrustworthy</option> flag doesn't place any restrictions on
       the module like <option>-XSafe</option> does. Instead the module author
       claims that while code may use unsafe features internally, it only
       exposes an API that can used in a safe manner. The use of
       <option>-XTrustworthy</option> by itself marks the module as trusted.
+      </para>
+
+      <para>
       There is an issue here as <option>-XTrustworthy</option> may be used by
       an arbitrary module and module author. To control the use of trustworthy
       modules it is recommended to use the <option>-fpackage-trust</option>
       flag. This flag adds an extra requirement to the trust check for
       trustworthy modules, such that for trustworthy modules to be considered
-      trusted, and allowed to be used in <option>-XSafe</option> compiled
-      code, the client C compiling the code must tell GHC that they trust the
-      package the trustworthy module resides in. This is essentially a way of
-      for C to say, while this package contains trustworthy modules that can be
-      used by untrusted modules compiled with <option>-XSafe </option>, I trust
-      the author(s) of this package and trust the modules only expose a safe
-      API. The trust of a package can be changed at any time, so if a
-      vulnerability found in a package, C can declare that package untrusted so
-      that any future compilation against that package would fail. For a more
-      detailed overview of this mechanism see <xref linkend="safe-trust"/>.
+      trusted, and allowed to be used in <option>-XSafe</option> compiled code,
+      the client C compiling the code must tell GHC that they trust the package
+      the trustworthy module resides in. This is essentially a way of for C to
+      say, while this package contains trustworthy modules that can be used by
+      untrusted modules compiled with <option>-XSafe</option>, I trust the
+      author(s) of this package and trust the modules only expose a safe API.
+      The trust of a package can be changed at any time, so if a vulnerability
+      found in a package, C can declare that package untrusted so that any
+      future compilation against that package would fail. For a more detailed
+      overview of this mechanism see <xref linkend="safe-trust"/>.
       </para>
 
       <para>
-      In the example, Danger can import module RIO because RIO is marked
-      trustworthy. Thus, Danger can make use of the rioReadFile and
-      rioWriteFile functions to access permitted file names. The main
-      application then imports both RIO and Danger. To run the plugin, it calls
-      RIO.runRIO Danger.runMe within the IO monad. The application is safe in
-      the knowledge that the only IO to ensue will be to files whose paths were
-      approved by the pathOK test.
+      In the example, <literal>Danger</literal> can import module
+      <literal>RIO</literal>because <literal>RIO</literal> is marked
+      trustworthy. Thus, <literal>Danger</literal> can make use of the
+      <literal>rioReadFile</literal> and <literal>rioWriteFile</literal>
+      functions to access permitted file names. The main application then
+      imports both <literal>RIO</literal> and <literal>Danger</literal>. To run
+      the plugin, it calls <literal>RIO.runRIO Danger.runMe</literal> within
+      the <literal>IO</literal> monad. The application is safe in the knowledge
+      that the only IO to ensue will be to files whose paths were approved by
+      the <literal>pathOK</literal> test.
       </para>
     </sect3>
   </sect2>
     following features:
 
     <itemizedlist>
-      <listitem><emphasis>TemplateHaskell</emphasis> &mdash; Is particularly
-        dangerous, as it can cause side effects even at compilation time and
-        can be used to access constructors of abstract data types.</listitem>
+      <listitem><emphasis>TemplateHaskell</emphasis> &mdash; Can be used to
+        gain access to constructors and abstract data types that weren't
+        exported by a module, subverting module boundaries.</listitem>
    </itemizedlist>
 
     In the safe language dialect we restrict the following features:
         <link linkend="deriving-typeable"><option>-XDeriveDataTypeable</option>
         </link> extension). Hand crafted instances of the Typeable type class
         are not allowed in Safe Haskell as this can easily be abused to 
-        unsafely coerce between types.</listitem>
+        unsafely coerce between types. Since GHC 7.8.1, this became a rule in
+        regular GHC Haskell as well, so going forward, Typeable can only be
+        derived both in and outside of the Safe language.</listitem>
     </itemizedlist>
   </sect2>
 
       <listitem><emphasis>-XSafe</emphasis> &mdash; Enables the safe language
         dialect, asking GHC to guarantee trust. The safe language dialect
         requires that all imports be trusted or a compilation error will
-        occur.</listitem>
+        occur. Safe Haskell will also infer this safety type for modules
+        automatically when possible. Please refer to section
+        <xref linkend="safe-inference"/> for more details of this.
+  </listitem>
       <listitem><emphasis>-XTrustworthy</emphasis> &mdash; Means that while
         this module may invoke unsafe functions internally, the module's author
         claims that it exports an API that can't be used in an unsafe way. This
     </itemizedlist>
 
     <para>
+    While these are flags, they also correspond to Safe Haskell module types
+    that a module can have. You can think of using these as declaring an
+    explicit contract (or type) that a module must have. If it is invalid, then
+    compilation will fail. Just like with regular Haskell types, GHC will also
+    infer the correct type for Safe Haskell. Please refer to section
+    <xref linkend="safe-inference"/> for more details of this.
+    </para>
+
+    <para>
     The procedure to check if a module is trusted or not depends on if the
     <option>-fpackage-trust</option> flag is present. The check is very similar
     in both cases with the presence of the <option>-fpackage-trust</option>
           <itemizedlist>
             <listitem>The module was compiled with
               <option>-XTrustworthy</option></listitem>
-            <listitem>All of M's direct safe imports are trusted by C</listitem>
+            <listitem>All of M's direct <emph>safe imports</emph>are trusted by
+              C</listitem>
           </itemizedlist>
         </listitem>
       </itemizedlist>
       properly turn on Safe Haskell while without it, it's operating in a
       covert fashion.
       </para>
-
-      <para>
-      Having the <option>-fpackage-trust</option> flag also nicely unifies the
-      semantics of how Safe Haskell works when used explicitly and how modules
-      are <ulink linkend="safe-inference">inferred as safe</ulink>.
-      </para>
     </sect3>
 
     <sect3 id="safe-trust-example">
     <para>
     When should you use Safe Haskell inference and when should you use an
     explicit <option>-XSafe</option> flag? The later case should be used when
-    you have a hard requirement that the module be safe. That is, the
-    <ulink linkend="safe-use-cases">use cases</ulink> outlined and the purpose
-    for which Safe Haskell is intended: compiling untrusted code. Safe
-    inference is meant to be used by ordinary Haskell programmers. Users who
-    probably don't care about Safe Haskell. 
+    you have a hard requirement that the module be safe. This is most useful
+    for the security <xref linkend="safe-use-cases">use case</xref> of Safe
+    Haskell: running untrusted code. Safe inference is meant to be used by
+    ordinary Haskell programmers. Users who probably don't care about Safe
+    Haskell. 
     </para>
 
     <para>
-    Say you are writing a Haskell library. Then you probably just want to use
-    Safe inference. Assuming you avoid any unsafe features of the language then
-    your modules will be marked safe. This is a benefit as now a user of your
-    library who may want to use it as part of an API exposed to untrusted code
-    can use the library without change. If there wasn't safety inference then
-    either the writer of the library would have to explicitly use Safe Haskell,
-    which is an unreasonable expectation of the whole Haskell community. Or the
-    user of the library would have to wrap it in a shim that simply re-exported
-    your API through a trustworthy module, an annoying practice.
+    Haskell library authors have a choice. Most should just use Safe inference.
+    Assuming you avoid any unsafe features of the language then your modules
+    will be marked safe. Inferred vs. Explicit has the following trade-offs:
+    </para>
+
+    <itemizedlist>
+      <listitem><emphasis>Inferred</emphasis> &mdash; This may work well and
+        adds no dependencies on the Safe Haskell type of any modules in other
+        packages. It does mean that the Safe Haskell type of your own modules
+        could change without warning if a dependency changes. One way to deal
+        with this is through the use of <xref linkend="safe-flag-summary">Safe
+        Haskell warning flags</xref> that will warn if GHC infers a Safe
+        Haskell type different from expected.</listitem>
+      <listitem><emphasis>Explicit</emphasis> &mdash; This gives your library a
+        stable Safe Haskell type that others can depend on. However, it may
+        increase the rate of compilation failure when your package dependencies
+        change.</listitem>
+    </itemizedlist>
+
+    <para>
+    This is a benefit as now a user of your library who may want to use it as
+    part of an API exposed to untrusted code can use the library without
+    change. If there wasn't safety inference then either the writer of the
+    library would have to explicitly use Safe Haskell, which is an unreasonable
+    expectation of the whole Haskell community. Or the user of the library
+    would have to wrap it in a shim that simply re-exported your API through a
+    trustworthy module, an annoying practice.
     </para>
   </sect2>
 
         <term>-fwarn-unsafe</term>
         <indexterm><primary>-fwarn-unsafe</primary></indexterm>
         <listitem>Issue a warning if the module being compiled is regarded
-          to be unsafe. Should be used to check the safety status of modules
+          to be unsafe. Should be used to check the safety type of modules
           when using safe inference.
         </listitem>
       </varlistentry>
         <term>-fwarn-safe</term>
         <indexterm><primary>-fwarn-safe</primary></indexterm>
         <listitem>Issue a warning if the module being compiled is regarded
-          to be safe. Should be used to check the safety status of modules
+          to be safe. Should be used to check the safety type of modules
           when using safe inference.
         </listitem>
       </varlistentry>
 
     <para>
     GHC includes a variety of flags that allow arbitrary processes to be run at
-    compilation time. One such example is the <link
-      linkend="pre-processor">custom pre-processor</link> flag. Another is the
-    ability of Template Haskell to execute Haskell code at compilation time,
-    including IO actions. Safe Haskell <emphasis>does not address this
-      danger</emphasis> (although, Template Haskell is a disallowed feature).
+    compilation time. One such example is the
+    <link linkend="pre-processor">custom pre-processor</link> flag. Another is
+    the ability of Template Haskell to execute Haskell code at compilation
+    time, including IO actions. Safe Haskell <emphasis>does not address this
+    danger</emphasis> (although, Template Haskell is a disallowed feature).
     </para>
 
     <para>