4 ms·

I am pretty sure that if you rewrite code, you should test rewritten version for equivalence. GCC has about 300K tests for a reason. I would not say kernel is l

by adontz 7y ago

I am pretty sure that if you rewrite code, you should test rewritten version for equivalence. GCC has about 300K tests for a reason. I would not say kernel is less important.

lixtra 7y ago
Testing for equivalence? Don’t you need to solve the halting problem for that? EDIT: I’m curious if a down voter can provide a piece of code that tests whether two compilates are equivalent. The root cause of the bug in the article was introduced by a patch to automatically modify an arbitrary program to harden against spectre.
- adontz 7y ago
  If we are talking about arithmetic operations, then I believe no.
- adontz 7y ago
  Also, I'm not talking about theoretical proof of equivalence, I'm talking about simple test like assert func(params) == rewrite(func)(params) for some reasonable set of func and params. Totally enough to catch problems like this. I'd say [unit-]testing that subtraction operator works is not that hard.
  - lixtra 7y ago
    Except, that in this case params is a string containing an arbitrary program. It would help the discussion if you read the TFA (edit: more carefully). Rewrite() in this case modified the params program to harden it against Spectre.
    - Quekid5 7y ago
      I think the poster is talking about something along the lines of bisimulation[1]. No need to solve the halting problem for that. [1] https://en.wikipedia.org/wiki/Bisimulation https://en.wikipedia.org/wiki/Bisimulation
    - marcinzm 7y ago
      That argument applies to pretty much every single unit test ever written. A function running on a single long can take 2^64 possible values. Impossible to test by your logic. Yet they're tested without issues constantly. What you do is put together a long list of sample functions and sample arguments that covers the expected edge cases and then test those for equivalence. Hardly impossible. Just takes time. Not bulletproof but better than nothing.
- rndgermandude 7y ago
  We're talking about eBPF programs here. Those halt by design as you cannot loop (jump backwards) and have a limited number of instructions you can use per program. So the halting problem isn't really and issue here in this particular case. You can just run the original and rewritten code in an eBPF VM with mock inputs and compare.

by adontz 7y ago

I am pretty sure that if you rewrite code, you should test rewritten version for equivalence. GCC has about 300K tests for a reason. I would not say kernel is less important.

lixtra 7y ago

Testing for equivalence? Don’t you need to solve the halting problem for that? EDIT: I’m curious if a down voter can provide a piece of code that tests whether two compilates are equivalent. The root cause of the bug in the article was introduced by a patch to automatically modify an arbitrary program to harden against spectre.

adontz 7y ago
If we are talking about arithmetic operations, then I believe no.
adontz 7y ago
Also, I'm not talking about theoretical proof of equivalence, I'm talking about simple test like assert func(params) == rewrite(func)(params) for some reasonable set of func and params. Totally enough to catch problems like this. I'd say [unit-]testing that subtraction operator works is not that hard.
- lixtra 7y ago
  Except, that in this case params is a string containing an arbitrary program. It would help the discussion if you read the TFA (edit: more carefully). Rewrite() in this case modified the params program to harden it against Spectre.
  - Quekid5 7y ago
    I think the poster is talking about something along the lines of bisimulation[1]. No need to solve the halting problem for that. [1] https://en.wikipedia.org/wiki/Bisimulation https://en.wikipedia.org/wiki/Bisimulation
  - marcinzm 7y ago
    That argument applies to pretty much every single unit test ever written. A function running on a single long can take 2^64 possible values. Impossible to test by your logic. Yet they're tested without issues constantly. What you do is put together a long list of sample functions and sample arguments that covers the expected edge cases and then test those for equivalence. Hardly impossible. Just takes time. Not bulletproof but better than nothing.
rndgermandude 7y ago
We're talking about eBPF programs here. Those halt by design as you cannot loop (jump backwards) and have a limited number of instructions you can use per program. So the halting problem isn't really and issue here in this particular case. You can just run the original and rewritten code in an eBPF VM with mock inputs and compare.