Replicating the 'Taint mode' from 'Fortify static checking tool' in Haskell

Question

I've read some documentation of the Fortify static checking tool. One of the concepts used by this tool are called taints. Some sources, such as web requests, provide data that is tainted in one or more ways and some sinks, such as web responses, require the data to be untainted.

The nice thing about Fortify is that you can have several types of taints. For example, you could tag srand output with NON_CRYPTO_RAND and then require that this taint is not present when using the variable for crypto purposes. Other examples include non-bound checked numbers and so on.

Is it possible to model taints with the stronger static type system used in Haskell or other programming languages with even more sophisticated type systems?

In Haskell, I could do types such as Tainted [BadRandom,Unbounded] Int but computing with them seems quite difficult as this new type constraints also operations that don't restrict the taints.

Are there nicer ways to accomplish this? Any existing work on the topic?

Answer 1

Not a full solution (= nice existing way to do this), but some hints:

Two papers about secure information flow in Haskell I know of are Li and Zdanevic, 2006 (one of the authors is also involved in Jif) and Russo et al., 2008. Both approach your "tainting" from the opposite side, namely, tagging values by how secure they are known to be, and use a lattice structure for ordering different security levels -- but the problem solved should be the same as you describe.

The first approach uses arrows for passing security information along with values (similar to a StaticArrow, I think), and so dynamically checks information flow policies (i.e., a runtime error occurs if you try to access a value you are not allowed to access).

The second one basically uses an identity monad indexed with a type tag indicating the security level for the contained value, thus operating at compile time. For converting between different security levels and more sophisticated stuff, though, they use an IO wrapper around the monad, so their system again isn't fully static. As you mentioned in a comment, the source of problem here seems to be the incompatibility of differently tagged monads.

When I investigated those papers for a uni seminar, I also reimplemented some of the code and then played around with it, trying to avoid resorting to IO. One of the results was this; maybe this kind of modification can be a useful experiment (I didn't do any real testing, though).

At last, one thing I'd really like to see is combining these approaches with dependent types. Applying the full power of Agda for such a task seems to be just the right direction...