Formal Analysis And Realization Of Application Information Flow Security

With the increasing popularity of smartphones and the rapid development of mobile networks,mobile applications have become an integral part of people’s daily lives.More and more people are accustomed to saving their personal information in mobile devices,and the problem of private information leakage has become increasingly prominent.Therefore,how to ensure that the information in mobile applications is not leaked during the transmission process has become a widely concerned and studied issue in academia and industry.The existing methods for ensuring application information security mainly apply the idea of permission access control.That is,when a mobile application submits an application for access to information,the application is verified for permissions.If the verification passes,the information can be accessed,and if the verification fails,the information cannot be accessed.This method protects the information from being illegally obtained to a certain extent,but it still cannot guarantee that the information after authorized access can meet the security requirements in the process of transmission and use.The information flow security technology can ensure information security by analyzing the legality of data transmission in the program,which can be used to solve the existing application program information security problem.In this paper,we focus on the field of mobile applications.We first set a permission set for each application,and use the permission as the basis for whether the application can legally obtain information to ensure that the information is not illegally accessed.For applications that have obtained access permissions,we use information flow security technology to ensure that information will not be leaked to attackers during subsequent transmission and use.Based on this idea,we propose a formal language and a logic rule for information flow security.Finally,we implement and verify the language and logic rules in the Coq tool.Practice has proved that the application-oriented information flow security method proposed by us is a feasible and effective method to ensure application information security.The main contributions of this article are:(1)A permission-based formal language for information flow security: The language abstracts applications as a set of functions,and uses function calls to complete the information exchange between applications.Different from traditional serial languages,we introduce the concept of permissions,and use permissions as the basis for whether an application can obtain information in the process of information interaction.In addition,the operational semantics of the language are strictly formulated,which facilitates the formation of reasoning logic.(2)A set of information flow security logic rules supporting declassification policy: The logic rules are a safe type system that describe how it is safe to pass the flow of information in the proposed formal language.Compared with the traditional information flow,the content of permission check is added to ensure that each application is safe in the process of obtaining information.In addition,a declassification strategy is added to make logical reasoning more accurate.(3)Implementation and verification using the formal proof tool Coq: The formal language,semantics and logic rules proposed above are implemented in the formal theorem proving tool Coq.After the implementation is completed,through the modeling and analysis of the mobile banking login system example,the effectiveness and feasibility of the information flow security method for the application program proposed in this paper are verified.