Part of the role of the bytecode verifier is to ensure that all avm2 stack accesses are within bounds - neither the interpreter nor jit code check these bounds at runtime so the verifier must be able to prove that all accesses are safe.

During verification the verifier uses FrameState objects to keep track of the states of the local variables and the scope and argument stacks. These three regions are actually allocated contiguously on the heap in the FrameState constructor:

        locals = (FrameValue*)mmfx_alloc_opt(sizeof(FrameValue) * frameSize, MMgc::kZero);

where FrameState.locals will actually be used like this:
   ________
  |        |
  | stack  |
  |        |
  |--------| <- stackBase is this offset
  |        |
  | scope  |
  |        |
  |--------| <- scopeBase is this offset
  |        |
  | locals |
  |________| <- FrameState.locals point here


The size of each of the locals, scope and stack are read directly from the method_body_info of the abcfile structure. This structure is laid out in exactly the same way as it would be in the interpreter/jit stack frame, but for the verifier these are allocated on the heap. For each framestate the verifier also stores the current offset in to the stack and scopestack as stackDepth and scopeDepth.

The verifier uses the following functions to check stack bounds and then to push and pop traits to the framestate (the verifier isn't pushing concrete values, only traits representing the types of value which will be pushed at runtime):
  checkState(pop, push) - checks that there is space on the stack to pop and push this number of traits
  pop(n) - pop this number of traits from the stack
  push(t) - push a trait representing this type to the stack

checkState, as well as checking that the runtime stack accesses will be in-bounds, is also checking that these verifier accesses are valid - the verifier framestate stack allocation is the same size as the runtime one, so every push/pop must first be checked with a checkState.

Here's the code from the verifier when it's checking instructions which could throw exceptions:

  if (pc < tryTo && pc >= tryFrom &&
      (opcodeInfo[opcode].canThrow || (isLoopHeader && pc == start_pos))) {
      // If this instruction can throw exceptions, treat it as an edge to
      // each in-scope catch handler.  The instruction can throw exceptions
      // if canThrow = true, or if this is the target of a backedge, where
      // the implicit interrupt check can throw an exception.
      for (int i=0, n=exTable->exception_count; i < n; i++) {
          ExceptionHandler* handler = &exTable->exceptions[i];
          if (pc >= code_pos + handler->from && pc < code_pos + handler->to) {
              int saveStackDepth = state->stackDepth;
              int saveScopeDepth = state->scopeDepth;
              FrameValue stackEntryZero = saveStackDepth > 0 ? state->stackValue(0) : state->value(0);
              state->stackDepth = 0;                                             <--- (a)
              state->scopeDepth = 0;

              // add edge from try statement to catch block
              const uint8_t* target = code_pos + handler->target;
              // The thrown value is received as an atom but we will coerce it to
              // the expected type before handing control to the catch block.
              state->push(handler->traits);                                      <--- (b)
              checkTarget(pc, target, /*isExceptionEdge*/true);
              state->pop();

              state->stackDepth = saveStackDepth;
              state->scopeDepth = saveScopeDepth;
              if (saveStackDepth > 0)
                  state->stackValue(0) = stackEntryZero;

              // Note that an exception may be caught in this method.
              handlerIsReachable = true;
          }
      }
  }

When a catch block is entered the stack and scopeStack will both be cleared so the handler will have a clean stack and scopeStack - this is achieved in the verifier at point (a) by settings state->stackDepth and state->scopeDepth to 0. The verifier then calls state->push(handler->traits) at point (b) to push the type traits for the thrown object on to the stack, but doesn't first calls checkStack(0,1) to check whether this push is valid. Note that the stackDepth was explicitly set to 0 at (b), but it's perfectly valid to have a method with a 0-sized stack. Here's the implementation of state->push():

REALLY_INLINE void FrameState::push(Traits* traits, bool notNull)
{
    AvmAssert(stackBase + stackDepth+1 <= frameSize);
    setType(stackBase + stackDepth++, traits, notNull);
}

REALLY_INLINE void FrameState::setType(int32_t i, Traits* t, bool notNull, bool isWith)
{
    FrameValue& v = value(i);
    v.traits = t;
    v.notNull = notNull;
    v.isWith = isWith;
#ifdef VMCFG_NANOJIT
    BuiltinType bt = Traits::getBuiltinType(t);
    v.sst_mask = 1 << valueStorageType(bt);

FLOAT_ONLY( 
    if(bt == BUILTIN_float4) info->forceLargeVarSize();
)
#endif
}

So in a release build this push will write an 8-byte trait off the end of the locals heap allocation and in debug it will hit the AvmAssert(stackBase + stackDepth+1 <= frameSize) .

I've attached an abc file which you can use with avmshell to hit the bug - I've tested that it hits the assert in a debug build and valgrind sees the 8 byte heap overflow in a valgrind build. It's harder to get real flash to crash on this at it would require some heap grooming but it should be easy to verify in avmshell.

The PoC has a three byte function with a 0-sized stack in the method_body_info and the first instruction is one which throws an exception and is covered by a try block.
 

hit_heap_overflow.abc 42 bytes Download