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?

Euhemerize

Well, the IO monad in Haskell models the most grevious taint of interaction with the Real World. You could have a MonadTaint typeclass similar to MonadIO and then make your BadRandom and Unbounded types instances of it. – Cadaver

@Cadaver That doesn't really work since if I track multiple taints in the type, I don't have a plain monad anymore (values on each side of bind don't necessarily have the same type anymore). Indexed monads might help though, but.. – Euhemerize

I haven't gotten to use it, but this sounds like the approach taken in hackage.haskell.org/package/control-monad-exception – Fiver

@Euhemerize Can functions "taint" values, or are values only "tainted" at the source? Also, could you give an example of an operation that doesn't restrict the taints? – Retinoscopy

Sounds like you're looking for something like effect typing, like as implemented as an Idris library: eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf – Glycolysis

There are two data level ways to do this. One is to hide data in a constructor, and require something special to get it out. This is the approach IO takes. The other is to only accept data that's in a constructor, and require something special to put it in. Haskell has more support, including typeclass support, for the latter. Instead of showing that a value is bad for a purpose (insufficiently random), and then failing to show that it is bad before using it for that purpose (not insufficiently random), you could instead show that it is sufficiently random and require the same. – Djebel

@Retinoscopy All taints I have seen come from sources. An example of a function that doesn't care about taints is a (+), it should happily sum both tainted and untainted values – Euhemerize

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...

Headlock

Answer 2

A simple model of this might be as follows:

{-# 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

Since clean is not exported it's impossible for users of srand to remove the Tainted tag. Further, you can use the "pseudo-Applicative" apply function (<+>) to merge taints. We could easily produce a similar combinator for a "pseudo-Monad" interface as well:

(>>-) :: 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)

Harlene

Is the purpose of Identity to steal Identity's Monad and Applicative instances with {-# LANGUAGE GeneralizedNewtypeDeriving #-}? – Djebel

Yep—I could have written them directly as well but this was clearer. – Harlene