You could have gone to Hackage and checked your protocols correctness using CPSA, not that the side-channel attacks would be discovered by such a tool.
Interesting. I had seen CPSA announced at one point, but there appears to be no documentation whatsoever. Did I miss the doc links?
There's lots of documentation: $ cabal unpack cpsa $ cd cpsa* $ cd doc $ ls *.pdf -- or you might have to build from .tex, I can't recall.
The two large families of side-channel attacks that I know of and that have been popular (== successful) recently are: ... timing and cache miss attacks ... Am I making sense?
So much sense it's painful. (that's a 'yes')
Another of my tentative projects was to write a C library that implements popular crypto building blocks, with a large battery of tests for correctness and resistance to timing attacks.
But how does that prevent a timing-based information flow if the consuming Haskell application is the one performing the branch? Are you assuming all information flow in the Haskell program is so high-level its not cryptographically important, thus protecting these low-level primitives is sufficient? Also, if you feel any of these tests would fit into the Test.Crypto module (or a submodule) then please feel free to send in a patch or start some discussion. Cheers, Thomas