security - 在 Haskell 中从 'Taint mode' 复制 'Fortify static checking tool'

Question

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

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

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

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

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

Answer 1

不是一个完整的解决方案(=很好的现有方法)，但有一些提示:

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

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

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

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

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