TY - GEN
T1 - Practical, formal synthesis and automatic enforcement of security policies for Android
AU - Bagheri, Hamid
AU - Sadeghi, Alireza
AU - Jabbarvand, Reyhaneh
AU - Malek, Sam
N1 - Funding Information:
This work was supported in part by awards CCF-1252644 from the National Science Foundation, D11AP00282 from the Defense Advanced Research Projects Agency, W911NF-09-1-0273 from the Army Research Office, HSHQDC-14-C-B0040 from the Department of Homeland Security, and FA95501610030 from the Air Force Office of Scientific Research.
Publisher Copyright:
© 2016 IEEE.
Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.
PY - 2016/9/29
Y1 - 2016/9/29
N2 - As the dominant mobile computing platform, Android has become a prime target for cyber-security attacks. Many of these attacks are manifested at the application level, and through the exploitation of vulnerabilities in apps downloaded from the popular app stores. Increasingly, sophisticated attacks exploit the vulnerabilities in multiple installed apps, making it extremely difficult to foresee such attacks, as neither the app developers nor the store operators know a priori which apps will be installed together. This paper presents an approach that allows the end-users to safeguard a given bundle of apps installed on their device from such attacks. The approach, realized in a tool, called SEPAR, combines static analysis with lightweight formal methods to automatically infer security-relevant properties from a bundle of apps. It then uses a constraint solver to synthesize possible security exploits, from which fine-grained security policies are derived and automatically enforced to protect a given device. In our experiments with over 4,000 Android apps, SEPAR has proven to be highly effective at detecting previously unknown vulnerabilities as well as preventing their exploitation.
AB - As the dominant mobile computing platform, Android has become a prime target for cyber-security attacks. Many of these attacks are manifested at the application level, and through the exploitation of vulnerabilities in apps downloaded from the popular app stores. Increasingly, sophisticated attacks exploit the vulnerabilities in multiple installed apps, making it extremely difficult to foresee such attacks, as neither the app developers nor the store operators know a priori which apps will be installed together. This paper presents an approach that allows the end-users to safeguard a given bundle of apps installed on their device from such attacks. The approach, realized in a tool, called SEPAR, combines static analysis with lightweight formal methods to automatically infer security-relevant properties from a bundle of apps. It then uses a constraint solver to synthesize possible security exploits, from which fine-grained security policies are derived and automatically enforced to protect a given device. In our experiments with over 4,000 Android apps, SEPAR has proven to be highly effective at detecting previously unknown vulnerabilities as well as preventing their exploitation.
UR - http://www.scopus.com/inward/record.url?scp=84994344814&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84994344814&partnerID=8YFLogxK
U2 - 10.1109/DSN.2016.53
DO - 10.1109/DSN.2016.53
M3 - Conference contribution
AN - SCOPUS:84994344814
T3 - Proceedings - 46th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2016
SP - 514
EP - 525
BT - Proceedings - 46th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2016
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 46th IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2016
Y2 - 28 June 2016 through 1 July 2016
ER -