从Haskell中的"强化静态检查工具"复制"污点模式"

Question

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

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

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

在Haskell中,我可以做类型,Tainted [BadRandom,Unbounded] Int但是使用它们进行计算似乎很困难,因为这种新类型限制了不限制污点的操作.

有没有更好的方法来实现这一目标？有关该主题的任何现有工作？

Answer 1

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

我所知道的两篇关于Haskell中安全信息流的论文是Li and Zdanevic, 2006（其中一位作者也参与了Jif）和Russo et al., 2008。两者都从相反的方面处理您的“污染”，即根据已知的安全程度来标记值，并使用网格结构来排序不同的安全级别 - 但解决的问题应该与您所描述的相同。

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

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

当我为大学研讨会调查这些论文时，我还重新实现了一些代码，然后使用它，试图避免诉诸IO. 结果之一是这样的；也许这种修改可以是一个有用的实验（不过我没有做任何真正的测试）。

最后，我真正希望看到的一件事是将这些方法与依赖类型相结合。充分发挥 Agda 的力量来完成这样的任务似乎是正确的方向......