Implementing a hardware-assistedmemory management mechanism for ARM platforms using the Bmethod

摘要

ARM embedded devices are becoming increasingly ubiquitous, permeating many aspects of daily life. The security issues on ARM embedded devices are much more important in critical infrastructure. The trusted hardware technologies provide the trusted environments isolated from the untrusted part of the system. However, for some deficiency, the researchers focus on current hardware-assisted isolated mechanisms. Depending on the implementation of the protection mechanism, the software-based approaches are not efficient and the hardware-based approaches are not flexible. Moreover, these defense mechanisms need formal specification that is inadequate in recent research. B method is a state-based formal method,which provides a successive refinement mechanism. In this paper, we propose a hardware-assisted memory isolation protection mechanism, provide specifications and refinements using the B method, and implement the memory management system on an ARM-based platform. The evaluation results show that the proposed isolation protection mechanism is effective, and the automatic proof rate of machines is acceptable.