4 ms·
I just took a look at Meacham's 2008 winner. After skimming your paper I believe it makes it through your countermeasures unscathed.
by jancsika 3y ago
I just took a look at Meacham's 2008 winner. After skimming your paper I believe it makes it through your countermeasures unscathed.
- praptak 3y agoThis is an insightful example because it's kind of "wrong at the higher level". It follows the spec. Every formal verification method will confirm that. It's the spec that is wrong. Obviously I mean the "replaces digits with zeros" spec, which does not follow the "doesn't leak data" spec. The root problem is that "doesn't leak data" is hard to define in a way that can be formally verified. This is a fundamental problem, not an incidental one.
- tgv 3y agoIndeed. It looks as if it could have been written in Rust and Spark. > doesn't leak data This requirement was translated into "zero a rectangle" without considering every format. Careful analysis is clearly possible, it was done by the author of that code, but understanding the full implications of code is hard.
- dwheeler 3y agoI doubt any set of countermeasures will guarantee catching everything. I think the goal should be to make it harder and riskier for attackers to successfully perform the attack. I can't be certain we can get there... but nothing gets better if we don't try to make it better.
- jancsika 3y agoI'm just talking about that scrumptious little contest winner. For example, not wanting to fudge around with allocation while iterating is palpable to anyone who can read C. That contest winner probably squeaks by. But perhaps on the flip side, any memory allocation that takes place while looping over bytes gets flagged for further review? I don't have the numbers but it seems like a lot of security bugs in C have lived there. Maybe the compiler blocks until you email it your pair programmer and they ACK back... :)