correctness of BPF stack size checking logic for multi-function programs?

[Jann Horn]

Hi!

I saw the recently-added support for multiple functions in a single
program in BPF. I've stumbled over something that looks like it might
be a bug; I haven't verified it yet, but I thought I should give you a
heads-up before this lands in a release in case I'm right. If I'm
wrong, it might be worth adding a comment to stacksafe() that explains
why.

stacksafe() has the following code:

/* if explored stack has more populated slots than current stack
* such stacks are not equivalent
*/
if (old->allocated_stack > cur->allocated_stack)
return false;

Note that if the old state had a smaller stack than the new state,
that is permitted because it is guaranteed that none of the extra
space in the new state will be used.

However, as far as I can tell, this can be used to smuggle a call
chain with a total stack size bigger than the permitted maximum
through the verifier, with code roughly as follows:

void b(void) {
  <allocate 300 bytes stack>
}
void main(void) {
  if (<condition>) {
    <allocate 300 bytes stack>
  }
  b();
}

AFAICS, if the verifier first verifies the branch of main() where
<condition> is false, it will go down into b, seeing a total stack
size of around 300 bytes. Afterwards, it will verify the branch of
main() where <condition> is true, but the states will converge after
the branch, preventing the verifier from going down into b() again and
discovering through update_stack_depth() that actually, the total
stack size is around 600 bytes. From a coarse look, it seems like this
might be usable to overflow the kernel stack, which would be
exploitable on systems without vmapped stack?

And actually, you could probably even trigger it with something like
this, since the stack is always fully allocated on function entry:

void b(void) {
  <allocate 300 bytes stack>
}
void main(void) {
  b();
  <allocate 300 bytes stack>
}

So I think it might be necessary to do an extra pass for the stack
depth checking when all the stackframe sizes are known?