Range checking is done deal with sufficiently strong types (read - dependent types). It was done in the Epigram LONG time ago, ten years ago if not more.
For example, when you fetching bytes for decode you can type-check that you are in the quota and act accordingly.
tyingq
Still a developer choice as to what the quota is though, right? That's the logic error here, quota set too high.
theszOP
No.
Working with two page quota (as QEMU dev intended) at type level won't allow you to pass through three page (as QEMU code allows and what is exploited).
For example, when you fetching bytes for decode you can type-check that you are in the quota and act accordingly.