Using the B Method to Formalize Access Control Mechanism with TrustZone Hardware Isolation (Short Paper)

摘要

Successfully employed in the industry, hardware isolation environment enhances the access control of traditional operating systems and requires more rigorous analysis. This paper first applies the B method to the access control mechanism formalization and proposes an extensible formal model, which not only specifies the access control mechanism with process state transition in Linux, but also introduces the hardware isolation description. Consistent with program implementations, the B specifications can be animated and verified. The proposed B model constructs a mathematical framework for the security analysis, providing a theoretical support for mechanism enhancements. All the model components are type checked by Atelier B, with 547 proof obligations automatically generated. The current rate of model proof is 79%. The experimental results by ProB show that there is no invariant violation or deadlock. In conclusion, this paper presents a feasible solution for access control mechanism formalization and verification in the embedded system design. The access control model can be further extended and refined, with its specifications transformed into executable codes after proved.