The value of this work is in the formal proof of the completeness of their technique, in a defined attack model. It does not mean that implementing an attack undetectable by weaker (and much simpler) setups is trivial (nor does it mean the attack model is always representative of reality).
Furthermore, much progress has been achieved in symbolic execution since then. Will you start backdooring symbolic execution systems so that they can disregard the backdoors you insert elsewhere ? in a consistent way ?
In any case, I forgot to make my main point in the last post, so here it is: The article claims that it would be viable to design a self-backdooring C compiler, to compromise a Verilog compiler, to insert secret hardware backdoors. Why would anyone go through all this trouble, when there already is a backdoor hidden in plain sight ? Have people forgotten about the Intel Management Engine ? If i’d wager a guess, I would say that is what would make NSA people laugh at such a question.
