本发明公开一种针对ARM架构的基于安全属性的访问控制形式化验证方法，该方法对系统中的实体进行抽象，为其赋予安全属性，以实现灵活、细粒度的系统资源管理，增强了ARM架构的资源安全保护。首先，定义系统资源的原子安全属性，并基于这些原子安全属性，为系统中的实体指定安全属性；其次，定义访问控制策略，访问控制策略为可信执行环境和非可信执行环境中产生的资源访问请求做出是否允许访问的判断，它以主体属性、客体属性和访问属性配置为输入等，本发明可以实现对特权模式与用户模式的内存读写权限的细粒度描述，增强ARM架构的内存隔离保护。实验证明了本方案设计的访问控制机制的有效性及其较低的性能开销。