This whole thing has got me curious about techniques for formally verifying software.
I'm a complete beginner on this topic, but I assume there are tools to help write software that's formally verified / proven to be correct. Can they make any guarantees about side-channel aspects such as timing in these systems? Anyone care to give me some pointers on where to begin?
A glance over the modelling doesn't seem to preclude using a model checker like 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).