http://scholar.google.co.uk/scholar?q=%22timing+attack%22+%22formal+methods%22+OR+%22formal+verification%22&btnG=&hl=en&as_sdt=0%2C5 http://scholar.google.co.uk

http://scholar.google.co.uk/scholar?q=%22timing+attack%22+%22formal+methods%22+OR+%22formal+verification%22&btnG=&hl=en&as_sdt=0%2C5 http://scholar.google.co.uk/scholar?q=%22timing+attack%22+%2... turns up some papers that consider this. They don't seem to provide much by way of tooling though. A glance over the modelling doesn't seem to preclude using a model checker like http://www.event-b.org/ http://www.event-b.org/ for it though. The challenge comes in when you try to translate. You write your model up and validate your approach, you then try to translate it into C (or whatever) and that point you can be as certain of your design as you like, you still can't be sure that the compiled software will work properly. I haven't seen a convincing solution to that particular problem (and I've done some research on the topic for three separate projects now).