Ah, sorry, I didn't mean to imply that Cryptol itself doesn't matter. It does seem very useful for its intended purpose (though again this is from an outsider's perspective).
Rather, I meant to say that you do still need to worry about what sort of code Cryptol generates if you want to address the points raised in the original article (e.g. clearing secret memory). That was my original point, anyway: Cryptol doesn't address low-level side-channel problems.
As far as integrating FaCT and Cryptol, couldn't you use Cryptol to build the reference version of a construction, then implement a fast and side-channel-resistant variant in FaCT, then use SAW to prove the two were equivalent? (Maybe not as ideal as combining the two languages, exactly, but workable.)
I really appreciate you taking the time to reply. This stuff isn't my area of expertise, obviously, but I still find it very interesting.
Ok, yeah, we're on same page now. Far as Cryptol, I wanted to seeif it could be extended to generate FaCT which generated constant-time code. It would also generate C to check with SAW or other tools for extra checking or situations where side channels didn't matter. Could also be a tool that checked equivalence of the two at source or object code level so any checking of C code applied to FaCT.
That should cover most of the problem areas. I still think C itself or SPARK Ada could be modified to do what FaCT does. Some subset at least. Then, one can eliminate need to build FaCT-based tooling. So, those were the ideas I was brainstorming at least for what applies directly to those languages.
Rather, I meant to say that you do still need to worry about what sort of code Cryptol generates if you want to address the points raised in the original article (e.g. clearing secret memory). That was my original point, anyway: Cryptol doesn't address low-level side-channel problems.
As far as integrating FaCT and Cryptol, couldn't you use Cryptol to build the reference version of a construction, then implement a fast and side-channel-resistant variant in FaCT, then use SAW to prove the two were equivalent? (Maybe not as ideal as combining the two languages, exactly, but workable.)
I really appreciate you taking the time to reply. This stuff isn't my area of expertise, obviously, but I still find it very interesting.