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 itself 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. These include techniques such as information flow control security or encrypted computations.
The design of Safe Haskell covers the following aspects:IO
monad. There are
several loop holes in the type system though, the most obvious offender
being the unsafePerformIO :: IO a -> a
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 analyze 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
language (through the -XSafe
flag) can be thought of as a
way of enforcing good style, similar to the function of
-Wall
.
Safe Haskell is designed to give users enough guarantees about the safety
properties of compiled code so that secure systems can be built using
Haskell. A lot of work has been done with Haskell, building such systems
as information flow control security, capability based security, DSLs for
working with encrypted data... etc. These systems all rely on properties
of the Haskell language that aren't true in the general case where uses
of functions like unsafePerformIO
are allowed.
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 IO
monad that we have defined that only
allows a safe subset of IO
actions to be executed. We
define the plugin interface here so that it requires the plugin module,
Danger
, to export a single computation,
Danger.runMe
, of type RIO ()
, where
RIO
is a new monad defined as follows:
-- Either of the following Safe Haskell pragmas would do {-# LANGUAGE Trustworthy #-} {-# LANGUAGE Safe #-} module RIO (RIO(), runRIO, rioReadFile, rioWriteFile) where -- Notice that symbol UnsafeRIO is not exported from this module! newtype RIO a = UnsafeRIO { runRIO :: IO a } instance Monad RIO where return = UnsafeRIO . return (UnsafeRIO m) >>= k = UnsafeRIO $ m >>= runRIO . k -- Returns True iff access is allowed to file name pathOK :: FilePath -> IO Bool pathOK file = {- Implement some policy based on file name -} rioReadFile :: FilePath -> RIO String rioReadFile file = UnsafeRIO $ do ok <- pathOK file if ok then readFile file else return "" rioWriteFile :: FilePath -> String -> RIO () rioWriteFile file contents = UnsafeRIO $ do ok <- pathOK file if ok then writeFile file contents else return ()We compile Danger using the new Safe Haskell
-XSafe
flag:
{-# LANGUAGE Safe #-} module Danger ( runMe ) where runMe :: RIO () runMe = ...Before going into the Safe Haskell details, lets point out some of the reasons this design would fail without Safe Haskell:
RIO
type wrapper around IO
. The author of Danger can
subvert this though by simply writing arbitrary
IO
actions and using unsafePerformIO ::
IO a -> a
to execute them as pure functions.
UnsafeRIO
constructor.
Unfortunately Template Haskell can be used to subvert module
boundaries and so could be used gain access to this constructor.
To stop these attacks Safe Haskell can be used. This is done by compiling
the RIO module with the -XTrustworthy
flag and compiling
the Danger module with the -XSafe
flag.
The use of the -XSafe
flag to compile the Danger module
restricts the features of Haskell that can be used to a
safe subset. This includes
disallowing unsafePerfromIO
, Template Haskell, pure
FFI functions, Generalized Newtype Deriving, RULES and restricting the
operation of Overlapping Instances. The -XSafe
flag also
restricts the modules can be imported by Danger to only those that are
considered trusted. Trusted modules are those compiled with
-XSafe
, where GHC provides a mechanical guarantee that
the code is safe. Or those modules compiled with
-XTrustworthy
, where the module author claims that the
module is Safe.
This is why the RIO module is compiled with
-XTrustworthy
, to allow the Danger module to import it.
The -XTrustworthy
flag doesn't place any restrictions on
the module like -XSafe
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. There is an issue here as
-XTrustworthy
may be used by an arbitrary module and
module author. Because of this for trustworthy modules to be considered
trusted, and so allowed to be used in -XSafe
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 -XSafe
, 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 Section 7.20.4, “Trust”.
So 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.
IO
monad
are still allowed and behave as usual. Any pure function though, as
according to its type, is guaranteed to indeed be pure. This property
allows a user of the safe language to trust the types. This means,
for example, that the unsafePerformIO :: IO a -> a
function is disallowed in the safe language.
These three properties guarantee that you can trust the types in the safe language, can trust that module export lists are respected in the safe language and can trust that code that successfully compiles using the safe language has the same meaning as it normally would.
Lets now look at the details of the safe language. In the safe language dialect (enabled by-XSafe
) we disable completely the
following features:
-XSafe
are
dropped. RULES defined in trustworthy modules that M imports are still
valid and will fire as usual.-XSafe
but restricted. While M
can define overlapping instance declarations, they can only overlap
other instance declaration defined in M. If in a module N that imports
M, at a call site that uses a type-class function there is a choice of
which instance to use (i.e. an overlap) and the most specific instances
is from M, then all the other choices must also be from M. If not, a
compilation error will occur. A simple way to think of this is a
same origin policy for overlapping instances
defined in Safe compiled modules.-XDeriveDataTypeable
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.impdecl -> import [safe] [qualified] modid [as modid] [impspec]When used, the module being imported with the safe keyword must be a trusted module, otherwise a compilation error will occur. The safe import extension is enabled by either of the
-XSafe
,
-XTrustworthy
, or -XSafeImports
flags and corresponding PRAGMA's. When the -XSafe
flag
is used, the safe keyword is allowed but meaningless, every import
is required to be safe regardless.
Whether or not a module is trusted depends on a notion of trust for packages, which is determined by the client C invoking GHC (i.e. you). A package P is trusted when either C's package database records that P is trusted (and no command-line arguments override this), or C's command-line flags say to trust it regardless of what is recorded in the package database. In either case, C is the only authority on package trust. It is up to the client to decide which packages they trust.
So a module M in a package P is trusted by a client C if and only if:-XSafe
-XTrustworthy
-XTrustworthy
compiled modules.
Package Wuggle: {-# LANGUAGE Safe #-} module Buggle where import Prelude f x = ...blah... Package P: {-# LANGUAGE Trustworthy #-} module M where import System.IO.Unsafe import safe Buggle
Suppose a client C decides to trust package P. Then does C trust module
M? To decide, GHC must check M's imports — M imports
System.IO.Unsafe. M was compiled with -XTrustworthy
, so
P's author takes responsibility for that import. C trusts P's author, so
C trusts M to only use its unsafe imports in a safe and consistent
manner with respect to the API M exposes. M also has a safe import of
Buggle, so for this import P's author takes no responsibility for the
safety, so GHC must check whether Buggle is trusted by C. Is it? Well,
it is compiled with -XSafe
, so the code in Buggle
itself is machine-checked to be OK, but again under the assumption that
all of Buggle's imports are trusted by C. Prelude comes from base, which
C trusts, and is compiled with -XTrustworthy
(While
Prelude is typically imported implicitly, it still obeys the same rules
outlined here). So Buggle is considered trusted.
Notice that C didn't need to trust package Wuggle; the machine checking
is enough. C only needs to trust packages that contain
-XTrustworthy
modules.
import safe Untrusted.ModuleAs the safe import keyword is a feature of Safe Haskell and not Haskell98 this would fail though unless you enabled Safe imports through on the of the Safe Haskell language flags. Three flags enable safe imports,
-XSafe, -XTrustworthy
and
-XSafeImports
. However -XSafe
and
-XTrustworthy
do more then just enable the keyword which
may be undesirable. Using the -XSafeImports
language
flag allows you to enable safe imports and nothing more.
-XTrustworthy
has no effect on the accepted range
of Haskell programs or their semantics, except that they allow the
safe import keyword.