Language-Based Privacy Protection In Android

With the rapid development of mobile Internet and the popularity of smart mobile devices,the smart mobile devices have been part of our daily life.When users use these smart mobile devices,a large number of privacy is stored on these devices.Since there are a lot of third-party applications installed in these devices,there is huge risk that the privacy stored there is leaked by these applications.Previous research on privacy protection in Android applications always develops an analysis tool to check the privacy leak in applications,and lacks formal study of the effectiveness.Formal methods can help us to have a clearer understanding of the problem,and provide a more rigorous guarantee of the correctness of the solu-tion.This paper proposes a checking mechanism to detect privacy leak in Android applications,and formally studies the effectiveness of our method.Then based on the theoretical result,we develop an analysis tool for Android applications to show the feasibility of our method.Our work makes the following contributions:First,we extend the current access control based permission model in An-droid,and introduce a new class of permissions,namely se,nd permission,to de-scribe the private information that an application is allowed to send out.A secure application can declare no or little required send permission to show that it is in-deed trustworthy.Second,we propose a novel hybrid method to prevent collusive information leak caused by communications among applications.Static checking is used to prevent the information leak in an individual application and dynamic checking is used to prevent the collusive leak among applications.The combination can reduce the number of false alarms in purely static approaches,and reduce the runtime overhead of purely dynamic approaches.Third,we study the leak behaviors in Android applications,and formally prove the effectiveness of our mechanism.We propose a new security property,leak-freedom,a non-interference-like property that guarantees that no information is leaked through application collusion.The soundness of our approach is formally defined by requiring that applications conforming to the security policy satisfy leak-freedom.We have written around 15,500 lines of Coq proof scripts for the soundness proofs.Finally,we develop a new hybrid analysis tool AndroidLeaker to prevent the information leak in applications.It uses the taint analysis technique to perform the static checking and instruments the dynamic checking code into the original ap-plication.The taint analysis is flow-sensitive,context-sensitive and field-sensitive.It gets a 82%precision,based on our testing over DroidBench test set.