Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Verification, Model Checking, and Abstract Interpretation

VMCAI 2015: Verification, Model Checking, and Abstract Interpretation pp 61–79Cite as

Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8931))

Abstract

We introduce an enhanced information-flow analysis for tracking the amount of confidential data that is possibly released to third parties by a mobile application. The main novelty of our solution is that it can explicitly keep track of the footprint of data sources in the expressions formed and manipulated by the program, as well as of transformations over them, yielding a lazy approach with finer granularity, which may reduce false positives with respect to state-of-the-art information-flow analyses.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alvim, M.S., Scedrov, A., Schneider, F.B.: When not all bits are equal: Worth-based information flow. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 120–139. Springer, Heidelberg (2014)

    Google Scholar 

  2. Amtoft, T., Banerjee, A.: A logic for information flow analysis with an application to forward slicing of simple imperative programs. Science of Compututer Programming 64, 3–28 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  3. AppBrain. Adnetwork stats, http://www.appbrain.com/stats/libraries/ad

  4. Arzt, S., Rasthofer, S., et al.: Flowdroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. In: PLDI. ACM (2014)

    Google Scholar 

  5. Askarov, A., Myers, A.: A semantic framework for declassification and endorsement. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 64–84. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Cavadini, S.: Secure slices of insecure programs. In: ASIACCS. ACM Press (2008)

    Google Scholar 

  7. Chaudhuri, A.: Language-based security on android. In: PLAS. ACM (2009)

    Google Scholar 

  8. Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. EPTCS 129, 325–336 (2013)

    Article  Google Scholar 

  9. Costantini, G., Ferrara, P., Cortesi, A.: Static analysis of string values. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 505–521. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  10. Cousot, P., Cousot, R.: Abstract interpretation: Past, present and future. In: CSL-LICS. ACM (2014)

    Google Scholar 

  11. Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL. ACM (2011)

    Google Scholar 

  12. Denning, D.E.: A lattice model of secure information flow. Communications of the ACM 19, 236–243 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  13. Dwork, C.: Differential privacy: A survey of results. In: Agrawal, M., Du, D.-Z., Duan, Z., Li, A. (eds.) TAMC 2008. LNCS, vol. 4978, pp. 1–19. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  14. Ebadi, H., Sands, D., Schneider, G.: Differential privacy: Now it’s getting personal. In: POPL. ACM (2015)

    Google Scholar 

  15. Enck, W., Gilbert, P., et al.: Taintdroid: An information flow tracking system for real-time privacy monitoring on smartphones. Comm. of the ACM 57(3), 99–106 (2014)

    Article  Google Scholar 

  16. Ferrara, P.: Generic combination of heap and value analyses in abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 302–321. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  17. Halder, R., Zanioli, M., Cortesi, A.: Information leakage analysis of database query languages. In: SAC. ACM (2014)

    Google Scholar 

  18. Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. International Journal of Information Security 8, 399–422 (2009)

    Article  Google Scholar 

  19. Hornyack, P., Han, S., Jung, J., Schechter, S.E., Wetherall, D.: These aren’t the droids you’re looking for: retrofitting android to protect data from imperious applications. In: CCS. ACM (2011)

    Google Scholar 

  20. Krohn, M.N., Tromer, E.: Noninterference for a practical DIFC-based operating system. In: IEEE S&P. IEEE (2009)

    Google Scholar 

  21. Li, B.: Analyzing information-flow in java program based on slicing technique. SIGSOFT Softw. Eng. Notes 27, 98–103 (2002)

    Article  Google Scholar 

  22. Lochbihler, A., Snelting, G.: On temporal path conditions in dependence graphs. Journal of Automated Software Engineering 16, 263–290 (2009)

    Article  Google Scholar 

  23. Logozzo, F.: Class invariants as abstract interpretation of trace semantics. Computer Languages, Systems & Structures 35, 100–142 (2009)

    Article  Google Scholar 

  24. Lu, L., Li, Z., Wu, Z., Lee, W., Jiang, G.: Chex: statically vetting android apps for component hijacking vulnerabilities. In: CCS. ACM (2012)

    Google Scholar 

  25. McCamant, S., Ernst, M.D.: Quantitative information flow as network flow capacity. In: PLDI. ACM (2008)

    Google Scholar 

  26. Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)

    Article  MATH  Google Scholar 

  27. Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: SOSP. ACM (1997)

    Google Scholar 

  28. Nanevski, A., Banerjee, A., Garg, D.: Dependent type theory for verification of information flow and access control policies. ACM TOPLAS 35(2), 6:1–6:41 (2013)

    Google Scholar 

  29. Omoronyia, I., Cavallaro, L., et al.: Engineering adaptive privacy: on the role of privacy awareness requirements. In: ICSE. IEEE/ACM (2013)

    Google Scholar 

  30. Pottier, F., Simonet, V.: Information flow inference for ml. ACM Transactions on Programming Languages and Systems 25, 117–158 (2003)

    Article  Google Scholar 

  31. Rasthofer, S., Lovat, E., Bodden, E.: Droid force: Enforcing complex, data-centric, system-wide policies in android. In: ARES (2014)

    Google Scholar 

  32. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21, 5–19 (2003)

    Article  Google Scholar 

  33. Sabelfeld, A., Sands, D.: Declassification: Dimensions and principles. Journal of Computer Security 17, 517–548 (2009)

    Google Scholar 

  34. Smith, G.: Principles of secure information flow analysis. In: Christodorescu, M., et al. (eds.) Malware Detection. Advances in Information Security, vol. 27, pp. 291–307. Springer (2007)

    Google Scholar 

  35. Smith, S.F., Thober, M.: Refactoring programs to secure information flows. In: PLAS. ACM (2006)

    Google Scholar 

  36. Spiekermann, S., Cranor, L.F.: Engineering privacy. IEEE Trans. Software Eng. 35(1), 67–82 (2009)

    Article  Google Scholar 

  37. Sridharan, M., Artzi, S., Pistoia, M., Guarnieri, S., Tripp, O., Berg, R.: F4f: Taint analysis of framework-based web applications. In: OOPSLA. ACM (2011)

    Google Scholar 

  38. Tripp, O., Ferrara, P., Pistoia, M.: Hybrid security analysis of web javascript code via dynamic partial evaluation. In: ISSTA. ACM (2014)

    Google Scholar 

  39. Tripp, O., Pistoia, M., Fink, S.J., Sridharan, M., Weisman, O.: Taj: Effective taint analysis of web applications. In: PLDI. ACM (2009)

    Google Scholar 

  40. Tripp, O., Rubin, J.: A bayesian approach to privacy enforcement in smartphones. In: USENIX Security (2014)

    Google Scholar 

  41. Xiao, X., Tillmann, N., Fähndrich, M., de Halleux, J., Moskal, M.: User-aware privacy control via extended static-information-flow analysis. In: ASE. ACM (2012)

    Google Scholar 

  42. Zanioli, M., Ferrara, P., Cortesi, A.: Sails: Static analysis of information leakage with sample. In: SAC. ACM (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IBM Thomas J.Watson Research Center, USA

    Agostino Cortesi, Pietro Ferrara, Marco Pistoia & Omer Tripp

  2. Università Ca’ Foscari Venezia, Italy

    Agostino Cortesi

Authors
  1. Agostino Cortesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pietro Ferrara
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marco Pistoia
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Omer Tripp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Automation, Indian Institute of Science, Bangalore, India

    Deepak D’Souza

  2. Microsoft Research India, 560001, Bangalore, India

    Akash Lal

  3. Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, DK-9220, Aalborg East, Denmark

    Kim Guldstrand Larsen

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cortesi, A., Ferrara, P., Pistoia, M., Tripp, O. (2015). Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications. In: D’Souza, D., Lal, A., Larsen, K.G. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2015. Lecture Notes in Computer Science, vol 8931. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46081-8_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-46081-8_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-46080-1

  • Online ISBN: 978-3-662-46081-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation