Very cool that they can demonstrate it but it also follows from Rice's theorem. Any sufficiently expressive computational formalism has non-trivial runtime properties/effects & these can not be detected w/ static analysis so you have to run the program to see what happens.
It is unfortunately also possible to construct unprobeable backdoors... [0]
[0]: https://openreview.net/forum?id=Wb8vS1kAHG