A formal android permission model based on the B method

Abstract

The rapid development of Android devices brings the increase of security requirements, especially for access control. Recently, many enhancements have been put forward towards the Android permission mechanism. However, few researches focus on the formalization and verification of security schemes. In this paper, we propose a formal Android permission model based on the B method, describing mechanism specifications and proving security properties. All model components are type checked by AtelierB, with 87% (154 out of 178) of generated proof obligations proved yet. The model is fully animated and checked by ProB. The results show that all specifications are well-defined without any deadlock and invariant violation. The proposed B model is for not only security analysis, but also system animation and extension. It presents a feasible approach to specify and verify the security scheme in the embedded system, which is able to translate into executable codes and implement practical module as well.