Premium
Implementing a hardware‐assisted memory management mechanism for ARM platforms using the B method
Author(s) -
Chang Rui,
Jiang Liehui,
Xie Yaobin,
He Hongqi,
Chen Danmin,
Ren Lu
Publication year - 2018
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
DOI - 10.1002/cpe.4659
Subject(s) - computer science , embedded system , isolation (microbiology) , mechanism (biology) , software , trusted computing , focus (optics) , protection mechanism , state (computer science) , arm architecture , computer hardware , operating system , control (management) , philosophy , physics , optics , epistemology , algorithm , artificial intelligence , microbiology and biotechnology , biology
Summary 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.