在Haskell中复制“Fortify静态检查工具”中的“污点模式”

Question

我阅读了Fortify静态检查工具的一些文档。该工具使用的一个概念被称为taints。某些来源（例如Web请求）提供的数据在一个或多个方面上都是不可信的，而某些汇（例如Web响应）需要数据是可信的。

Fortify的好处在于可以有几种类型的taints。例如，您可以使用 NON_CRYPTO_RAND 标记 srand 输出，然后要求在用于加密目的时不存在这种taint。其他示例包括未经绑定检查的数字等。

在Haskell或其他使用更复杂类型系统的编程语言中是否可能使用更强的静态类型系统对taints进行建模？

在Haskell中，我可以定义这样的类型：Tainted [BadRandom,Unbounded] Int，但与它们一起计算似乎非常困难，因为这种新类型也会限制不限制taints的操作。

是否有更好的方法来完成这项工作？是否有关于此主题的任何现有工作？

- aleator

---

在Haskell中，IO单子模拟了与真实世界交互的最严重的污染。你可以创建一个类似于MonadIO的MonadTaint类型类，然后将你的BadRandom和Unbounded类型作为它的实例。 - cdk

@cdk，这并不起作用，因为如果我在类型中跟踪多个污点，我就不再有一个简单的单子了（绑定两侧的值不一定具有相同的类型）。索引单子可能会有所帮助，但是... - aleator

我还没有使用过它，但这听起来像是 http://hackage.haskell.org/package/control-monad-exception 中采用的方法。 - jberryman

@aleator 函数能够“污染”值，还是只有源头才会“污染”值？此外，你能否举一个不限制污点的操作的例子？ - danidiaz

有两种数据级别的方法可以实现这一点。一种是在构造函数中隐藏数据，并要求使用特殊方法才能获取它。这是IO采用的方法。另一种是只接受在构造函数中的数据，并要求使用特殊方法将其放入。Haskell对后者提供了更多支持，包括类型类支持。与其展示一个值不适合某个目的（不足够随机），然后在使用它之前未能展示它不适合该目的（不足够随机），您可以展示它足够随机并要求相同。 - Cirdec

Answer 1

不是一个完整的解决方案（即没有很好的现有方法来解决这个问题），但是有一些提示：

我知道两篇关于Haskell中安全信息流的论文，分别是Li和Zdanevic 2006年的文章（其中一位作者还参与了Jif）以及Russo等人在2008年发表的文章。两篇论文的方法都从相反的方向来处理你所描述的"污染"，即通过标记值的安全等级，采用格结构对不同安全等级进行排序 -- 但所解决的问题应该是相同的。

第一种方法使用箭头来传递带有安全信息的值（类似于StaticArrow），因此在运行时检查信息流策略（即如果您尝试访问未被允许访问的值，则会发生运行时错误）。

第二种方法基本上使用一个带有类型标签的身份单子来索引包含值的安全级别，因此在编译时运行。但是，为了转换不同的安全级别和更复杂的东西，他们使用一个围绕这个单子的IO包装器，因此他们的系统再次不是完全静态的。正如您在评论中提到的那样，这里问题的源头似乎是不同标记的单子不兼容。

当我为大学研讨会调查这些论文时，我还重新实现了一些代码，然后进行了一些测试，试图避免采用IO。其中一个结果是这个；也许这种修改可以作为一个有用的实验（尽管我没有进行任何真正的测试）。

最后，我真的想看到将这些方法与依赖类型相结合。应用Agda的全部功能来完成这样的任务似乎是正确的方向...

- phipsgabler

Answer 2

一个简单的模型可能如下所示：

{-# LANGUAGE EmptyDataDecls             #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators              #-}

module Taint ( (:+), srand, BadRandom, Unbounded, Tainted (), (<+>)) where

import           Control.Applicative
import           Control.Monad.Identity

data a :+ b

data BadRandom
data Unbounded

newtype Tainted taint a = Tainted { clean :: Identity a }
  deriving ( Functor, Applicative, Monad )

(<+>) :: Tainted t1 (a -> b) -> Tainted t2 a -> Tainted (t1 :+ t2) b
Tainted (Identity f) <+> Tainted (Identity x) = Tainted (Identity (f x))

srand :: IO (Tainted BadRandom Int)
srand = undefined

由于 clean 没有被导出，因此使用 srand 的用户无法删除 Tainted 标记。此外，您可以使用“伪Applicative”应用函数 (<+>) 来合并污点。我们也可以轻松地为“伪Monad”接口制作类似的组合器：

(>>-) :: Tainted t1 a -> (a -> Tainted t2 b) -> Tainted (t1 :+ t2) b
Tainted (Identity a) >>- f = let Tainted (Identity b) = f a in Tainted (Identity b)

- J. Abrahamson

---

Identity 的目的是通过 {-# LANGUAGE GeneralizedNewtypeDeriving #-} 来窃取 Identity 的 Monad 和 Applicative 实例吗？ - Cirdec

是的 - 我本来也可以直接写，但这样更清晰明了。 - J. Abrahamson