Safe Haskell

Safe Haskellは、バージョン7.2でGHCに実装された言語拡張である。これは、コードが使うことが許されるGHC Haskellの機能を限定することによって、unsafeなコードを信頼されたコードベースに安全な形で含めることができるようにする。単純化して言うと、これはプログラム内の型を信頼に足るものにする。Safe Haskell自体は最小限のものであることを目標としていて、その上により高度な安全システム(例えば情報フロー制御によるセキュリティや、暗号化計算)を構築するのに必要十分な強さの保証を提供する。

Safe Haskellの設計は以下の面にわたっている。

Safe Haskellの用途

Safe Haskellは以下の二つの利用例を念頭に置いて設計されている。
  • 厳格な型安全性をコンパイル時に強制する
  • 信頼されていないコードをコンパイルし、実行する

厳格な型安全性(良いスタイル)

Haskellは、強力な型システムと、IOモナドを通した純粋な関数と作用のある関数の分離を提供している。しかし、この型システムには抜け穴がいくつかある。最も分かり易いのは関数unsafePerformIO :: IO a -> aである。Safe Haskellのsafe language方言はこのような関数の利用を禁止する。これによってHaskellコードを分析したり論証したりし易くなるので、色々の目的のために便利である。また、このようなunsafeな関数はどうしても必要でない限り使うべきでないという既存のHaskellコミュニティの文化を成文化するものでもある。こういう訳で、(-XSafeを使った)safe languageの利用は、-Wallの機能と似て、良いスタイルを強制する手段だととらえることができる。

セキュアなシステムを構築する(制約付きIOモナド)

Safe Haskellは、コンパイルされたコードの性質に関して、Haskellを使ってセキュアなシステムを構築するのに十分なだけの保証を与えるように設計されている。情報フロー制御、capability-basedセキュリティ、暗号化されたデータを扱うためのDSL、といったシステムをHaskellで構築するための作業が大量に為されてきた。これらのシステムは全て、unsafePerformIOのような関数が許される一般の場合には成り立たないようなHaskell言語の性質に依拠している。

例として、プラグイン作者が信用されず、悪意のある第三者かもしれないようなプラグインシステムのためのインタフェースを定義してみよう。このために、プラグインのインタフェースを純粋な関数にするか、IO動作の安全なサブセットしか実行することを許されないような制限されたIOモナドにする。ここではプラグインのインタフェースを以下のようにする。すなわち、プラグインモジュールDangerは、型RIO ()を持つ単一の計算Danger.runMeを定義することを要求される。ただしRIOは以下のように定義された新しいモナドである。

        -- 以下のSafe Haskellのプラグマはどちらでも良い
        {-# LANGUAGE Trustworthy #-}
        {-# LANGUAGE Safe #-}

        module RIO (RIO(), runRIO, rioReadFile, rioWriteFile) where

        -- UnsafeRIOシンボルがこのモジュールからエクスポートされていないのに注意!
        newtype RIO a = UnsafeRIO { runRIO :: IO a }

        instance Monad RIO where
            return = UnsafeRIO . return
            (UnsafeRIO m) >>= k = UnsafeRIO $ m >>= runRIO . k

        -- ファイル名にアクセスが許可されている場合、かつその場合に限りTrue
        pathOK :: FilePath -> IO Bool
        pathOK file = {- ファイル名についての何らかのポリシーの実装 -}

        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 ()
      
Dangerを、新しいSafe Haskellのフラグである-XSafe付きでコンパイルする
        {-# LANGUAGE Safe #-}
        module Danger ( runMe ) where

        runMe :: RIO ()
        runMe = ...
      
Safe Haskellの詳細に入る前に、この設計がSafe Haskellなしではうまく行かない理由の一部を指摘しておこう。
  • この設計は、Dangerが実行することのできる操作を型によって、具体的にはIOのラッパであるRIOによって制限している。Dangerの作者は、単にunsafePerformIO :: IO a -> aを使って任意のIOアクションを純粋関数として実行することでこの制限を覆すことができる。
  • またこの設計はDangerモジュールがUnsafeRIO構築子にアクセスできないことを前提としている。残念なことにTemplate Haskellを使うとモジュール境界を破壊することができ、この構築子へのアクセスを得ることもできるだろう。
  • 信用されていないDangerモジュールがインポートできるモジュールに制限を掛ける方法がない。これによって非常に広いattack surface(実質的に、システムにインストールされている全てのパッケージ)をDangerの作者に与えることになる。仮にこれらのパッケージのいずれかに脆弱性があれば、Dangerモジュールはそれを利用できる。これを防ぐ唯一の方法は、既知の脆弱性のあるモジュールにパッチを当てるか削除することである。それらがRIOモジュールなどの信頼されたモジュールからのみ使われるべきものであったとしても。

これらの攻撃を止めるためにSafe Haskellを使うことができる。これには、RIOモジュールを-XTrustworthyフラグ付きでコンパイルし、Dangerモジュールを-XSafeフラグ付きでコンパイルする。

-XSafeフラグを使うことで、利用可能なHaskellの機能を安全なサブセットに限定してDangerモジュールをコンパイルすることができる。これには、unsafePerfromIO、Template Haskell、純粋なFFI関数、一般化newtype deriving、RULESを禁止し、重複インスタンスの操作に制限を加えることを含む。さらに、-XSafeは、Dangerがインポートできるモジュールを信頼されているとみなされるもののみに制限する。信頼されるモジュールは、-XSafe付きでコンパイルされたもの(この場合、コードが安全であることをGHCが機械的に保証する)または、-XTrustworthy付きでコンパイルされたもの(この場合、モジュール作者がこのモジュールが安全だと主張する)である。

これが、RIOモジュールがDangerモジュールからインポートできるように-XTrustworthy付きでコンパイルされている理由である。-XTrustworthyは、-XSafeと異なり、モジュールについていかなる制限も課さない。代わりに、コードが内部的にunsafeな機能を使っていても、安全に使えるAPIしか露出していないということをモジュール作者が主張する。ここで、問題が一つある。あらゆるモジュールのあらゆる作者が-XTrustworthyを使えるのである。このため、Trustworthyとされたモジュールが信頼され、-XSafeでコンパイルされるコードから使うことを許されるためには、コードをコンパイルしているクライアントCが、このTrustworthyとされたモジュールが所属するパッケージを信頼する旨をGHCに伝えなければならない。これは実質的に、「このパッケージは-XSafeでコンパイルされる信頼されないモジュールによって使えるTrustworthyモジュールを含んでいるが、私はこのパッケージの作者を信頼し、このモジュールが安全なAPIしか露出しないことを信頼する」と言う手段をCに与える。パッケージへの信頼はいつでも変えられるので、もしパッケージに脆弱性が見付かったら、Cはそのパッケージが信頼されないと宣言し、そのパッケージに対する将来のいかなるコンパイルも失敗するようにできる。この機構についてのより詳細な概観は7.20.4. 信頼を見よ。

以上により、RIOはTrustworthyと標示されているのでDangerはRIOをインポートできる。よって、DangerはrioReadFileとrioWriteFileの各関数を使って許可されたファイル名にアクセスできる。次に主アプリケーションがRIOとDangerの両方をインポートし、RIO.runRIO Danger.runMeをIOモナド中で呼ぶことでプラグインを走らせる。pathOKの検査によって認められたパスを持つファイルにしかIOできないと分かっているので、このアプリケーションは安全である。

safe language

Safe Haskellのsafe languageは以下の性質を保証する。
  • 参照透明性 — safe languageの関数は決定的であり、それらを評価することはいかなる副作用も引き起こさない。IOモナドの関数は通常通りに振る舞うことが許される。しかし、純粋な関数は全て、その型に従って実際に純粋であることが保証される。この性質によって、safe languageの利用者は型を信頼することが可能になる。これは、例えばunsafePerformIO :: IO a -> aがsafe languageにおいて禁止されることを意味している。
  • モジュール境界の制御 — safe languageを使ってコンパイルされたHaskellコードは、他のモジュールのエクスポートリストから公的に利用可能なシンボルにしかアクセスできないことが保証される。このうち重要な点として、safeでコンパイルされたコードは、自分がインポートできない構築子を使ってデータ値を検査したり作ったりすることができない。モジュールMが、エクスポートリストを注意深く使うことである不変条件を確立しているなら、safe languageを使ってコンパイルされたコードでMをインポートするものは、これらの不変条件を守ることが保証される。このために、Template HaskellGeneralizedNewtypeDerivingはsafe languageにおいてはどちらも無効にされる。これらを使ってこの性質に違反することができるからである。
  • 意味的な整合性 — safe languageはHaskellのGHC実装の厳密なサブセットである。safe languageでコンパイル可能なあらゆる式は、通常のHaskellでコンパイルされた場合と全く同じ意味を持つ。さらに、safe languageモジュールをインポートするあらゆるモジュールにおいて、このsafe importを付けても付けなくてもコンパイル可能なあらゆる式は、どちらの場合でも同じ意味を持つ。つまり、safe languageを使ってモジュールをインポートすることで、そのモジュールに依存していない既存コードの意味を変えることはできない。よって例えば、重複インスタンス拡張はこの性質に違反できるので、いくらかの制限が課される。

これらの三つの性質は、safe languageにおいて型を信頼できること、safe languageのコードがモジュールのエクスポートリストに従うこと、safe languageを使ってコンパイルに成功したコードは通常持つべき意味と同じ意味を持つこと、を保証する。

ではsafe languageの詳細を見ていこう。safe lauguage方言(-XSafeによって有効になる)においては、以下の機能は完全に無効になる。
  • GeneralizedNewtypeDeriving — これは構築子のアクセス制御に違反するために使うことができる。信頼されていないコードが、保護されたデータ型をデータ型の作者が意図しない方法で操作することを可能にすることによる。例えばこれを使ってデータ構造の不変条件を破ることができる。
  • TemplateHaskell — これは、コンパイル時に副作用を起こすことを可能にし、抽象データ型にアクセスするために使えるので特に危険である。THを使うと非常に簡単にモジュール境界を壊すことができる。
safe language方言では以下の機能に制限が加えられる。
  • ForeignFunctionInterface — これは大部分において安全であるが、関数をIOでない型でインポートするforeign import宣言は禁止される。全てのFFIインポートはIOモナドに生息しなければならない。
  • RULES — 信頼されたコードの振る舞いを予測不可能な形で変更し、意味上の整合性に違反することができるので、機能が制限される。具体的には、-XSafeでコンパイルされたモジュールMで定義されたRULESは全て捨てられる。MがインポートするTrustworthyモジュールで定義されたRULESはなお有効であり、通常通り発火する。
  • OverlappingInstances — この拡張は意味上の整合性に違反するために使うことができる。悪意のあるコードは、この信頼されていないモジュールをインポートしているコードの振る舞いを変えるようなインスタンスを再定義できるかもしれない(より特殊性の高いインスタンス宣言を持つことで)からである。-XSafeでコンンパイルされたモジュールMにおいて、この拡張は無効されないが制限を受ける。Mは重複インスタンス宣言を定義できるが、それらはMで定義された別のインスタンス宣言としか重複できない。MをインポートするモジュールNの中、型クラス関数を使う呼び出し地点で、どのインスタンスを使うかの選択肢(つまり重複)があり、最も特殊性の高いインスタンスがM由来の場合、他の全ての選択肢もM由来でなければならない。これについての簡単な考え方は、Safeコンパイルされたモジュールで定義された重複インスタンスに関する同一生成元ポリシー(same origin policy)だと思うことである。
  • Data.Typeable — Typeableインスタンスを自動導出(GHCによって-XDeriveDataTypeable拡張を介して提供されている)されたもののみに制限している。Typeable型クラスの手書きインスタンスは、unasfeに型変換を行うように簡単に悪用できるので、Safe Haskellでは許されていない。

safeインポート

Safe Haskellは、Haskellの通常のインポート構文に対する小さな拡張を有効にする。次のようにsafeキーワードを加える。
      impdecl -> import [safe] [qualified] modid [as modid] [impspec]
    
使われると、safeキーワード付きでインポートされるモジュールは信頼されたものでなければならず、そうでなければコンパイルエラーが発生する。このsafeインポート拡張は-XSafe-XTrustworthy-XSafeImportsのいずれか、あるいは対応するプラグマによって有効になる。-XSafeフラグが使われている場合、このsafeキーワードは許されるが無意味である。いずれにせよ全てのインポートが安全でなければならない。

信頼

Safe Haskell拡張は以下の二つの新しい言語フラグを導入する。
  • -XSafe — safe language方言を有効にし、GHCに信頼を保証するように頼む。safe language方言は全てのインポートが信頼されていることを要求し、そうでなければコンパイルエラーが発生する。
  • -XTrustworthy — このモジュールは内部的にunsafeな関数を呼びかもしれないが、unsafeな形で使うことのできないAPIしかエクスポートしないとモジュールの作者が主張していることを意味する。これはsafe languageを有効にせず、どんなHaskellコードが許されるかについて制限を加えることもない。信頼の保証はGHCによってではなくモジュール作者によって与えられる。safeキーワードの付いたインポート文は、インポート先モジュールが信頼されていない場合にコンパイルエラーになる。このキーワードの付いていないインポート文は通常通りに振る舞い、信頼されているかどうかにかかわらず、あらゆるモジュールをインポートできる。

あるモジュールが信頼されるかどうかは、パッケージへの信頼という概念に依存する。これはGHCを起動するクライアントC(つまり、あなたである)によって決定される。パッケージPが信頼されるのは、CのパッケージデータベースのレコードがPが信頼されていると記録している(しかも、コマンド行引数によって再定義されていない)場合、あるいはCのコマンド行フラグが、パケージデータベースの記録に関係なく信頼しろと言っている場合である。どちらの場合でも、パッケージの信頼に関して決定権はCにしかない。どのパッケージを信頼するかはクライアントによる。

よって、パッケージPのモジュールMがクライアントCに信頼されるのは、以下の条件が満されるとき、かつそのときに限る。
  • 以下が両方とも成り立つ
    • このモジュールが-XSafe付きでコンパイルされている
    • Mが直接インポートしているモジュールが全てCに信頼されている
  • あるいは以下が全て成り立つ
    • このモジュールが-XTrustworthy付きでコンパイルされている
    • Mが直接safeインポートしているモジュールが全てCに信頼されている
    • パッケージPがCに信頼されている
一番目の信頼の定義については、信頼の保証は、safe languageによって課される制約を通してGHCによって与えられる。二番目の定義については、この保証はまずモジュール作者によって与えられる。次にクライアントCが、このモジュールを含むパッケージを信頼することを示すことによって、モジュール作者への信頼を明示する。この信頼の連鎖が必要なのは、-XTrustworthyでコンパイルされたモジュールに関してGHCはいかなる保証も提供しないからである。

        パッケージWuggle:
           {-# LANGUAGE Safe #-}
           module Buggle where
             import Prelude
             f x = ...blah...

        パッケージP:
           {-# LANGUAGE Trustworthy #-}
           module M where
             import System.IO.Unsafe
             import safe Buggle
      

クライアントCがパッケージPを信頼することを決めたとしよう。ではCはモジュールMを信用するか?これを決めるために、GHCはMのインポートを検査しなければいけない。MはSystem.IO.Unsafeをインポートしている。Mは-XTrustworthy付きでコンパイルされているから、このインポートについてはMの作者が責任を負う。CはPの作者を信頼しているので、CはMがunsafeなインポートを安全かつMが露出するAPIに整合的な形でしか使わないということを信頼している。Mには、BuggleへのSafeインポートもある。safeインポートなのでPの作者はこれの安全性について責任を負わないため、BuggleがCに信頼されているかをGHCが検査しないといけない。どうか?うーん、これは-XSafe付きでコンパイルされているので、Buggle自体のコードは問題ないことが機械的に検査されている。ただしこれもBuggleのインポートが全てCに信頼されていることが条件である。Preludeはbase由来であり、Cはこれを信頼しており、-XTrustworthy付きでコンパイルされている。(Preludeは典型的には暗黙にインポートされるが、その場合でもここで述べた規則に沿う)。よってBuggleは信頼されているとみなされる。

CはパッケージWuggleを信頼する必要がなかったことに注意。機械による検査だけで十分である。Cは、-XTrustworthyなモジュールを含むパッケージだけを信頼すれば良い。

パッケージの信頼

Safe Haskellは各パッケージに新しい真偽値のプロパティを与える。信頼プロパティである。GHCのコマンド行でパッケージの信頼プロパティを指定するためのオプションがいくつか新たに利用可能である。
  • -trust P — パッケージPを隠されているなら露出し、パッケージデータベースに関係なく、信頼されているとみなす。
  • -distrust P — パッケージPを隠されているなら露出し、パッケージデータベースに関係なく、信頼されていないとみなす。
  • -distrust-all-packages — 後続のコマンド行オプションで明示的に信頼されていると指定されていない限り、全てのパッケージを信頼されていないとみなす。
パッケージの信頼プロパティをパッケージデータベース中で設定するには、4.9. パッケージ を参照してほしい。

信頼なしのsafeインポート

モジュールを書いていて、信頼できない作者によるモジュールをインポートしたいなら、次のように書くだろう。
        import safe Untrusted.Module
      
safeインポートキーワードはSafe Haskellの機能であってHaskell98ではないので、Safe Haskelの言語フラグのどれかを指定しないとこれは失敗する。safeインポートを有効にするフラグは-XSafe-XTrustworthy-XSafeImportsの三つである。しかし、-XSafe-XTrustworthyは単にこのキーワードを有効にする以上のことをするので、望ましくないことがある。-XSafeImportsを使うとsafeインポートを有効にしつつ、その他にはなにもしないということができる。

Safe Haskellのフラグまとめ

まとめると、Safe Haskellは以下の言語フラグからなる。
-XSafe
信頼されるためには全ての直接のインポート先が信頼されていなければならないが、モジュール自体は信頼済みパッケージに存在している必要はない。これが信頼に足るものであることはコンパイラが保証するからである。インポート文において"safe"キーワードは許されるが無意味であり、いずれにせよ全てのインポートが安全でなければならない。
  • モジュールが信頼されるか — される
  • Haskell言語 — safe languageに制限される
  • インポートされるモジュール — 全て強制的にsafeインポートになり、全てが信頼されていなければならない。
-XTrustworthy
これはモジュールが信頼されることを定めるが、その保証はモジュール作者によって与えられる。このモジュールのクライアントは次に、モジュールが含まれるパッケージを信頼すると指定することにより、このモジュール作者への信頼を指定する。-XTrustworthyはどのようなHaskellプログラムが受理されるかについて、およびそれらの意味について影響を与えない。例外は、safeインポートキーワードを許すことである。
  • モジュールが信頼されるか — されるが、モジュールのあるパッケージが信頼されている場合に限る。
  • Haskell言語 — 制限されない
  • インポートされるモジュール — どれが信頼されていなければいけないかは、モジュール作者に制御される。
-XSafeImport
safeインポート拡張を有効にする。モジュールが、自身の信用について何も述べることなく、依存関係が信頼されていることを要求できる。
  • モジュールが信頼されるか — されない
  • Haskell言語 — 制限されない
  • インポートされるモジュール — どれが信頼されていなければいけないかは、モジュール作者に制御される。