Safe Haskellは、バージョン7.2でGHCに実装された言語拡張である。これは、コードが使うことが許されるGHC Haskellの機能を限定することによって、unsafeなコードを信頼されたコードベースに安全な形で含めることができるようにする。単純化して言うと、これはプログラム内の型を信頼に足るものにする。Safe Haskellは最小限のものであることを目標としていて、その上により高度な安全システムを構築するのに必要十分な強さの保証を提供する。
これがSafe Haskellの動機となる使用例であるものの、Safe Haskellが追跡し強制するものが、通常のHaskellで保証されるよりも厳格な型安全性であるということを理解するのは重要である。これの一環として、Safe HaskellはGHCによるコンパイルのたびに実行され、明示的にSafe Haskellを使っていないモジュールについてさえ安全性を追跡し推論する。これについてのさらなる詳細は7.23.5. Safe Haskellの推論を参照して欲しい。これはまた、セキュリティの観点からは奇妙に見えるが型安全性を追跡するという角度からは論理的な設計判断があることも意味する。現在の設計について、またこのセキュリティと型安全性の間の緊張関係について、フィードバックを歓迎する。
Safe Haskellの設計は以下の面にわたっている。
Safe Haskellは以下の二つの利用例を念頭に置いて設計されている。
IO
モナドを通した純粋な関数と作用のある関数の分離を提供している。しかし、この型システムには抜け穴がいくつかある。最も分かり易いのは関数unsafePerformIO :: IO a -> a
である。Safe Haskellのsafe language方言はこのような関数の利用を禁止する。これによってHaskellコードを分析したり論証したりし易くなるので、色々の目的のために便利である。また、このようなunsafeな関数はどうしても必要でない限り使うべきでないという既存のHaskellコミュニティの文化を成文化するものでもある。こういう訳で、(-XSafe
を使った)safe languageの利用は、-Wall
の機能と似て、良いスタイルを強制する手段だととらえることができる。
情報フロー制御、capability-basedセキュリティ、暗号化されたデータを扱うためのDSL、といったシステムは、単に一つのライブラリとしてHaskell言語に組み込むことができる。しかしこれらのシステムは、unsafePerformIO
のような関数が許される一般の場合には成り立たないようなHaskell言語の性質が保証されることを要求する。Safe 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なしではうまく行かない理由の一部を指摘しておこう。
IO
のラッパであるRIO
によって制限している。Dangerの作者は、単にunsafePerformIO :: IO a -> a
を使って任意のIO
アクションを純粋関数として実行することでこの制限を覆すことができる。
UnsafeRIO
構築子にアクセスできないことを前提としている。残念なことにTemplate Haskellを使うとモジュール境界を破壊することができ、この構築子へのアクセスを得ることもできるだろう。
これらの攻撃を止めるために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
自体が、そのモジュールを信頼されたものにするのである。ここで、問題が一つある。あらゆるモジュールのあらゆる作者が-XTrustworthy
を使えるのである。trustworthyモジュールの利用を制御するため、-fpackage-trust
フラグを使うことが推奨される。このフラグは、trustworthyモジュールの信頼検査へ条件を追加する。その場合、Trustworthyとされたモジュールが信頼され、-XSafe
でコンパイルされるコードから使うことを許されるためには、コードをコンパイルしているクライアントCが、このTrustworthyとされたモジュールが所属するパッケージを信頼する旨をGHCに伝えなければならない。これは実質的に、「このパッケージは-XSafe
でコンパイルされる信頼されないモジュールによって使えるTrustworthyモジュールを含んでいるが、私はこのパッケージの作者を信頼し、このモジュールが安全なAPIしか露出しないことを信頼する」と言う手段をCに与える。パッケージへの信頼はいつでも変えられるので、もしパッケージに脆弱性が見付かったら、Cはそのパッケージが信頼されないと宣言し、そのパッケージに対する将来のいかなるコンパイルも失敗するようにできる。この機構についてのより詳細な概観は7.23.4. 信頼とSafe Haskellのモードを見よ。
例では、RIOはTrustworthyと標示されているのでDangerはRIOをインポートできる。よって、DangerはrioReadFileとrioWriteFileの各関数を使って許可されたファイル名にアクセスできる。次に主アプリケーションがRIOとDangerの両方をインポートし、RIO.runRIO Danger.runMeをIOモナド中で呼ぶことでプラグインを走らせる。pathOKの検査によって認められたパスを持つファイルにしかIOできないと分かっているので、このアプリケーションは安全である。
IO
モナドの関数は通常通りに振る舞うことが許される。しかし、純粋な関数は全て、その型に従って実際に純粋であることが保証される。この性質によって、safe languageの利用者は型を信頼することが可能になる。これは、例えばunsafePerformIO :: IO a -> a
がsafe languageにおいて禁止されることを意味している。
これらの三つの性質は、safe languageにおいて、型を信頼できること、コードがモジュールのエクスポートリストに従うこと、コンパイルに成功したコードが通常持つべき意味と同じ意味を持つこと、を保証する。
ではsafe languageの詳細を見ていこう。safe lauguage方言(-XSafe
によって有効になる)においては、以下の機能は完全に無効になる。
-XSafe
でコンパイルされたモジュールMで定義されたRULESは全て捨てられる。MがインポートするTrustworthyモジュールで定義されたRULESはなお有効であり、通常通り発火する。-XSafe
でコンンパイルされたモジュールMにおいて、この拡張は無効されないが制限を受ける。Mは重複インスタンス宣言を定義できるが、それらはMで定義された別のインスタンス宣言としか重複できない。MをインポートするモジュールNの中、型クラス関数を使う呼び出し地点で、どのインスタンスを使うかの選択肢(つまり重複)があり、最も特殊性の高いインスタンスがM由来の場合、他の全ての選択肢もM由来でなければならない。これについての簡単な考え方は、Safeコンパイルされたモジュールで定義された重複インスタンスに関する同一生成元ポリシー(same origin policy)だと思うことである。-XDeriveDataTypeable
拡張を介して提供されている)されたもののみに制限している。Typeable型クラスの手書きインスタンスは、unasfeに型変換を行うように簡単に悪用できるので、Safe Haskellでは許されていない。impdecl -> import [safe] [qualified] modid [as modid] [impspec]使われると、safeキーワード付きでインポートされるモジュールは信頼されたものでなければならず、そうでなければコンパイルエラーが発生する。このsafeインポート拡張は
-XSafe
、-XTrustworthy
、-XUnsafe
のいずれか、あるいは対応するプラグマによって有効になる。-XSafe
フラグが使われている場合、このsafeキーワードは許されるが無意味である。いずれにせよ全てのインポートが安全でなければならない。
-XSafe
を使ってコンパイルされているモジュールからインポートできないことを標示する。
あるモジュールが信頼されるかどうかの検査の手続きは、-fpackage-trust
フラグが与えられているかどうかに依存する。どちらの場合の検査も良く似ており、-fpackage-trust
の存在は、trustworthyモジュールが信頼されているとみなされるための要件を一つ追加するのみである。
-fpackage-trust
が無効の場合)-XSafe
付きでコンパイルされている
-XTrustworthy
付きでコンパイルされている
信頼を上のように定義することには問題がある。どんなモジュールでも-XTrustworthy付きでコンパイルすることができ、そうするとそれが何をするかにかかわらず信頼されるのである。これを制御するために、パッケージへの信頼についての追加的定義がある(-fpackage-trust
で有効になる)。パッケージへの信頼の要点は、どのパッケージがtrustworthyモジュールを含めるかをクライアントCが明示的に言うことである。つまり、Cは、パッケージPとその作者を信頼するのでP内の-XTrustworthy
を使ったモジュールを信頼する、と決める。パッケージへの信頼が有効の場合、trustworthyだとみなされるものの信頼されていないパッケージにあるモジュールは信頼されていないとみなされる。より形式的な定義は次の節で与えられる。
-fpackage-trust
が有効の場合)-fpackage-trust
が有効なら、あるモジュールが信頼されるかどうかは、パッケージへの信頼という概念に依存する。これはGHCを起動するクライアントC(つまり、あなたである)によって決定される。パッケージPが信頼されるのは、以下のどれかが成立する場合である。
どちらの場合でも、パッケージの信頼に関して決定権はCにしかない。どのパッケージを信頼するかはクライアントによる。
-fpackage-trust
フラグが使われているとき、パッケージPのモジュールMがクライアントCに信頼されるのは、以下の条件が満されるとき、かつそのときに限る。
-XSafe
付きでコンパイルされている
-XTrustworthy
付きでコンパイルされている
一番目の信頼の定義については、信頼の保証は、safe languageによって課される制約を通してGHCによって与えられる。二番目の定義については、この保証はまずモジュール作者によって与えられる。次にクライアントCが、このモジュールを含むパッケージを信頼することを示すことによって、モジュール作者への信頼を明示する。この信頼の連鎖が必要なのは、-XTrustworthy
でコンパイルされたモジュールに関してGHCはいかなる保証も提供しないからである。
信頼検査に二つのモードがある理由は、-fpackage-trust
によって有効になる追加の要件が、Safe Haskellの設計を侵襲的なものにするからである。このフラグが有効な場合、Safe Haskellを使っているパッケージは、ユーザの機械上のパッケージの信頼状態によってコンパイルが通ったり通らなかったりする。パッケージfoo
のメンテナが、セキュリティ意識のあるHaskellerがfoo
を使えるようにSafe Haskellを使うと、Safe Haskellを知りも構いもしないユーザに、fooが必要とするパッケージbar
が彼らの機械上で信頼されていないために、foo
がコンパイルできないと文句を言われることになる。この意味で、-fpackage-trust
はSafe Haskellを正式に有効にするフラグだと思うことができる。これなしでは、Safe Haskellはこっそりとしたやりかたで動作する。
Having the -fpackage-trust
flag also nicely unifies the
semantics of how Safe Haskell works when used explicitly and how modules
are inferred as safe.(訳注: 訳せません。助けて)
パッケージ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
なモジュールを含むパッケージだけを信頼すれば良い。
-XTrustworthy
を使うモジュールMの作者は、Mの公開API(エクスポートリストによって露出されているシンボル群)が安全でない方法で使えないことを保証するべきである。これは、エクスポートされているシンボルが型安全性と参照透明性に従うべきだということである。
-XSafe
、-XTrustworthy
、-XUnsafe
のどれもが使われずにモジュールがコンパイルされる場合、GHCはそのモジュールが安全だとみなせるかを自分で見出そうとする。この安全性の推論はモジュールを決してtrustworthyだとは標示せず、unsafeかsafeだとする。これをモジュールMについて決定するために、GHCは以下の単純な方法を使う。すなわち、Mが-XSafe
フラグの下でもエラーなしでコンパイルできるなら、Mはsafeであると標示する。Mが-XSafe
フラグの下ではコンパイルに失敗するなら、unsafeであると標示する。
Safe Haskellの推論を使うべきなのは何時で、明示的な-XSafe
フラグを使うべきなのは何時か?そのモジュールが安全でなければならないという動かせない要求があるなら、後者を使うべきである。つまり、概観した利用例や、Safe Haskellが意図している目的、すなわち信頼されていないコードをコンパイルする場合である。安全性の推論はふつうのHaskellプログラマに使われることを意図している。通常Safe Haskellを気にかけないユーザである。
Haskellライブラリを書いているとしよう。その場合、あなたは単に安全性推論を使いたいと思うだろう。安全でない言語機能を避けるなら、あなたのモジュールはsafeと標示される。これは良いことである。なぜなら、あなたのライブラリを信頼されないコードに露出されるAPIの一部として使いたいユーザが、ライブラリを変更なしで使えるからである。安全性の推論がなかったら、ライブラリの書き手が明示的にSafe Haskellを使わなければならないだろうが、これをHaskellコミュニティ全体に期待するのは合理的でない。そうでなければ、ライブラリのユーザがあなたのAPIをtrustworthyモジュールから再エクスポートするだけのラッパを書かなければならないが、これは鬱陶しい作業である。
-XTrustworthy
はどのようなHaskellプログラムが受理されるかについて、およびそれらの意味について影響を与えない。例外は、safeインポートキーワードを許すことである。
-fpackage-trust
が有効の場合) — されるが、モジュールのあるパッケージが信頼されている場合に限る。-XSafe
でコンパイルされたモジュールからインポートできないようにする。またsafeインポート拡張を有効にし、依存関係が信頼されていることをモジュールが要求できるようにする。