An Information Flow Security Logic for Permission-Based Declassification Strategy

With the increasing popularity of smartphones and the rapid development of mobile network, ensuring the security of mobile applications becomes more and more important, which has received substantial attention from both academia and industry. Information flow security, as a prominent approach to system and network security, aims at ensuring high security level information would not be accessed by analyzing the information with lower security levels. In this paper, we design a novel information flow security logic to reason about the security of mobile applications, leveraging on the idea of permission based declassification. Firstly, we propose a formal language with permission check branches, through which the access to the confidential information can be controlled. Then we present our novel information flow security logic based on the permission based declassification strategy, which can make the reasoning more precise by degrading the security level of the specific information. Finally, we demonstrate the usability of our logic via examples.