5 ms·

Reading more about that… How does the verifier detect infinite loops anyway? Halting problem and all. It must use some rather crude heuristics, no?

1propionyl 3y ago
It doesn't. Flip things around and you get something tractable, though incomplete. Unsolvable problem: reject any loop that is provably infinite. Solvable problem: reject any loop that isn't provably finite. The trade off is that there will always be some loops that in fact always do terminate, but that the verifier can't prove do.
blipvert 3y ago
You need to slightly modify your code. Rather than: while (condition) { … } Do: #define MAX 1000 for n = 0; n < MAX; n++ { if !condition break; … } Unroll all loops, don’t allow any backward jumps and limit to (say) 1m instructions.
- kqr 3y ago
  Incidentally, iteration limits are a good idea for production code anyway. If you don't imagine any input needing more than 50 k iterations, throw a user-friendly exception after something like 10 M iterations. Prevents much more annoying problems than it causes.
  - blipvert 3y ago
    Nice. Be good if the language had an easy way to handle it, eg.: while(condition)[1000 label]{…}
  - guenthert 3y ago
    > If you don't imagine any input needing more than 50 k iterations What could possibly go wrong.
    - kqr 3y ago
      You get an error is the worst that happens. Way better than running a denial of service attack on your own systems or those of your customer's.
      - deleted 3y ago
        [deleted]
      - guenthert 3y ago
        > You get an error is the worst that happens. That certainly depends on what eBPF is used for. If your load balancer errors out at [greatest number of connections envisioned] and an adversary manages to establish [greatest number of connections envisioned] then the result is a denial of service. Not every operator is confident in making code changes in 3rd party software or might even be allowed to make such changes. Increasing resources o.t.o.h., e.g. adding RAM, is rarely banned. I sure would want a system to make best use of available resources.
        kqr 3y ago
        I still think a denial of service due to tripping some sort of circuit breaker is preferable to one due to resource exhaustion. If the code is intended to use as a library or the binary distributed to third parties one will have to handle it differently. For libraries taking a parameter indicating the maximum expected is common, for example. See e.g. man 3 read.

1propionyl 3y ago

It doesn't. Flip things around and you get something tractable, though incomplete. Unsolvable problem: reject any loop that is provably infinite. Solvable problem: reject any loop that isn't provably finite. The trade off is that there will always be some loops that in fact always do terminate, but that the verifier can't prove do.

blipvert 3y ago

You need to slightly modify your code. Rather than: while (condition) { … } Do: #define MAX 1000 for n = 0; n < MAX; n++ { if !condition break; … } Unroll all loops, don’t allow any backward jumps and limit to (say) 1m instructions.

kqr 3y ago
Incidentally, iteration limits are a good idea for production code anyway. If you don't imagine any input needing more than 50 k iterations, throw a user-friendly exception after something like 10 M iterations. Prevents much more annoying problems than it causes.
- blipvert 3y ago
  Nice. Be good if the language had an easy way to handle it, eg.: while(condition)[1000 label]{…}
- guenthert 3y ago
  > If you don't imagine any input needing more than 50 k iterations What could possibly go wrong.
  - kqr 3y ago
    You get an error is the worst that happens. Way better than running a denial of service attack on your own systems or those of your customer's.
    - deleted 3y ago
      [deleted]
    - guenthert 3y ago
      > You get an error is the worst that happens. That certainly depends on what eBPF is used for. If your load balancer errors out at [greatest number of connections envisioned] and an adversary manages to establish [greatest number of connections envisioned] then the result is a denial of service. Not every operator is confident in making code changes in 3rd party software or might even be allowed to make such changes. Increasing resources o.t.o.h., e.g. adding RAM, is rarely banned. I sure would want a system to make best use of available resources.
      - kqr 3y ago
        I still think a denial of service due to tripping some sort of circuit breaker is preferable to one due to resource exhaustion. If the code is intended to use as a library or the binary distributed to third parties one will have to handle it differently. For libraries taking a parameter indicating the maximum expected is common, for example. See e.g. man 3 read.