14

我已经阅读了 Fortify 静态检查工具的一些文档。此工具使用的概念之一称为taints。某些来源（例如 Web 请求）提供的数据以一种或多种方式受到污染，而某些接收器（例如 Web 响应）则要求数据不受污染。

Fortify 的好处是您可以拥有多种类型的污点。例如，您可以使用标记srand输出，NON_CRYPTO_RAND然后要求在将变量用于加密目的时不存在此污点。其他示例包括非绑定检查号码等。

是否可以使用 Haskell 中使用的更强大的静态类型系统或其他具有更复杂类型系统的编程语言来建模污点？

在 Haskell 中，我可以做诸如此类的类型，Tainted [BadRandom,Unbounded] Int但使用它们进行计算似乎相当困难，因为这种新的类型约束也是不限制污点的操作。

有更好的方法来实现这一点吗？关于该主题的任何现有工作？

4

2 回答 2

4

不是一个完整的解决方案（=很好的现有方法），但有一些提示：

我知道的两篇关于 Haskell 中安全信息流的论文是Li 和 Zdanevic，2006（其中一位作者也参与了Jif）和Russo 等人，2008。两者都从相反的角度处理您的“污染”，即通过已知它们的安全程度来标记值，并使用点阵结构对不同的安全级别进行排序——但解决的问题应该与您描述的相同。

第一种方法使用箭头与值一起传递安全信息（我认为类似于 a StaticArrow），因此动态检查信息流策略（即，如果您尝试访问不允许访问的值，则会发生运行时错误）。

第二个基本上使用一个标识单子，该单子用一个类型标签索引，指示所包含值的安全级别，因此在编译时运行。但是，为了在不同的安全级别和更复杂的东西之间进行转换，他们使用IO了 monad 的包装器，因此他们的系统也不是完全静态的。正如您在评论中提到的，这里问题的根源似乎是不同标记的单子不兼容。

当我为 uni 研讨会研究这些论文时，我还重新实现了一些代码，然后玩弄它，试图避免使用IO. 结果之一是这样；也许这种修改可能是一个有用的实验（虽然我没有做任何真正的测试）。

最后，我真正希望看到的一件事是将这些方法与依赖类型结合起来。将 Agda 的全部力量用于这样的任务似乎是正确的方向......

于 2014-05-06T22:12:48.540 回答
3

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

{-# 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)
于 2014-05-06T22:21:53.943 回答