VERIFIABLE INTEGRITY GUARANTEES FOR MACHINE CODE PROGRAMS

A verifier performs static checks of machine code to ensure that the code will execute safely. After verification is performed, the code is executed. The code modules generated by the rewriter and verified by the verifier prevent runtime code modifications so that properties established by the verifier cannot be invalidated during execution. Guards ensure that control flows only as expected. Stack data that must be shared within a code module, and which may therefore be corrupted during execution, is placed on a separate data stack. Other stack data remains on the regular execution stack, called the control stack. Multiple memory accesses can be checked by a single memory-range guard, optimized for fast access to the most-frequently used memory.