A New Hybrid Static/Run-time Secure Memory Access Protection

Secure memory access protection plays a critical role in making software systems resilient to malicious security attacks. Run-time checking is one of the major strategies that provides safe memory accesses. However, in many security-critical applications, the performance overhead due to the extra computation at runtime is often unacceptable. In order to reduce this cost, we propose a new strategy that minimizes the number of runtime checks by efficiently integrating the results from static software verification. Our strategy applies a verification approach called SAT-based software bounded model checking (BMC) to detect memory access violations as well as to prove the absence of such violations within a given bound statically, followed by a runtime checking to synergistically and completely secure the memory accesses. Our method makes use of static verification in a fine-grained manner, in which redundant runtime checks can be avoided for those safe accesses. Furthermore, with BMC, our strategy can provide the error traces useful for debugging if the instance is proved unsafe.