3 ms·
The first thing I searched for in the README was "constant time". This whole thing has got me curious about techniques for formally verifying software. I'm a
by dhotson 13y ago
The first thing I searched for in the README was "constant time".
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?
- runeks 13y agoThis blog post isn't about writing automated tools to detect timing attacks in code, but it has a lot of stuff about how to write crypto code -- elliptic curve cryptography in particular -- that is impervious to timing attacks, very interesting if you ask me: http://blog.cr.yp.to/20140323-ecdsa.html http://blog.cr.yp.to/20140323-ecdsa.html
- ElliotH 13y agohttp://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).