Detect invalid stack access by child procedure

[hackaugusto]

Here is an example of a subtle bug:

#! Input: [idx]
#! Output: [addr]
proc.compute_address
   push.BASE_ADDR movup.2 add
end

#! Input: [idx]
#! Output: []
proc.save_index
   dup exec.compute_address memstore
end

The issue above is that movup.2 touches part of the stack it shouldn't, the code works because the expected value happened to be duplicated by the parent, and the final stack state matched the expected state, even though the instruction used was "incorrect". The issue above won't be caught by tests unless compute_address is carefully tested.

The example above happened in the kernel:

• here the parent procedure duplicates the top of the stack
• here the child procedure uses the value saved in the stack as part of the parent state

The tests didn't caught the issue, because process_input_note is not tested directly, only via the prepare_transaction. The code doesn't contain an error, but it is confusing.

[hackaugusto]

I imagine that implementing a way to detect the above is a big change, if possible at all. Because currently we don't have a mechanism to inform the VM what is the expected size of the stack available for the child when doing a call. (Related https://github.com/0xPolygonMiden/miden-vm/issues/772 )

One proposal is to add metadata annotations, say @stack(4), which would mean the procedure takes 4 elements from the top of the stack as inputs. With said annotation the VM could be run on a strict mode, by truncating the stack to only the top 4 elements prior to calling the child process, and trapping if the 5th stack element is accessed (that is, without pushing to the stack).

Another approach is just to say the above is a no issue, and should be handled by better testing.

[bobbinth]

Yes, this will be tricky to catch, but I think you proposal of adding annotations to procedures is probably the best way to handle it. It is not a simple solution because procedures may be inlined into the code - but we need to have a way to catch that anyways.

[bitwalker]

I think an annotation-based approach is the only real option. However, in my mind this clearly overlaps with the need to be able to express the type signature of Miden procedures (using some well-specified ABI for representing complex types).

If the type signature (and necessarily, the calling convention, i.e. how parameters of a given type are passed on the operand stack) of the procedure is known, we can do the same static analysis that the @stack N annotation would enable, but also solve some of the other problems we have at the same time.

As an aside, a type annotation would permit us to implement some basic type checking and optimizations. For example, if a given parameter is declared as a u32, we might be able to elide runtime assertions, and check that callers pass a value of that type in the appropriate position on the operand stack. There are limits, simply due to the low-level nature of MASM, but we could almost certainly catch a broad class of mistakes that would otherwise potentially go unnoticed.