3 ms·

Underhanded code is interesting and worrying. In April 2020 I wrote a paper on some ideas on how to counter underhanded code. Some countermeasures seem promisi

Underhanded code is interesting and worrying. In April 2020 I wrote a paper on some ideas on how to counter underhanded code. Some countermeasures seem promising, especially when combined. More info here: "Initial Analysis of Underhanded Source Code", April, 2020, IDA document: D-13166, https://www.ida.org/research-and-publications/publications/all/i/in/initial-analysis-of-underhanded-source-code https://www.ida.org/research-and-publications/publications/a... I hope that some find it interesting, or even build on it.

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 ago
  This 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 ago
    Indeed. 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 ago
  I 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 ago
    I'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... :)

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 ago
This 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 ago
  Indeed. 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 ago
I 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 ago
  I'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... :)