Skip to main content
SpringerLink
Log in

Interprocedural Information Flow Analysis of XML Processors

  • Conference paper
Language and Automata Theory and Applications (LATA 2014)

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

Abstract

A crucial issue when providing publicly accessible web services is that sensitive data should only be accessible by authorized users. Accessibility of data within an application or information flow can conveniently be formalized as a 2-hyperproperty of a program. Here, we present a technique to interprocedurally analyze information flow in XML processors. Our approach is based on general techniques for program matching, and relational abstract interpretation of the resulting 2-programs. In case of XML processors, the abstract relational semantics then can be practically analyzed by means of finite tree automata.

This work was partially supported by the German Research Foundation (DFG) under the project SpAGAT (grant no. SE 551/14-2) in the priority program “Reliably Secure Software Systems – RS3”.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alves, A., Arkin, A., Askary, S., Barreto, C., Bloch, B., Curbera, F., Ford, M., Goland, Y., Guízar, A., Kartha, N., Liu, C.K., Khalaf, R., Koenig, D., Marin, M., Mehta, V., Thatte, S., Rijn, D., Yendluri, P., Yiu, A.: Web services business process execution language version 2.0 (OASIS standard). WS-BPEL TC OASIS (2007), http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.html

  2. Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200–214. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  3. Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: Asymmetric product programs for relational program verification. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 29–43. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  4. Berglund, A., Boag, S., Chamberlin, D., Fernández, M.F., Kay, M., Robie, J., Siméon, J.: XML path language (XPath) 2.0 (second edition). World Wide Web Consortium, Recommendation REC-xpath20-20101214 (December 14, 2010), http://www.w3.org/TR/2010/REC-xpath20-20101214/

  5. Broberg, N., Sands, D.: Paralocks: Role-based information flow control and beyond. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 431–444 (2010)

    Google Scholar 

  6. Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security 18(6), 1157–1210 (2010)

    Google Scholar 

  7. Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007), http://www.grappa.univ-lille3.fr/tata (release October 12, 2007)

  8. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages (POPL), pp. 238–252. ACM (1977)

    Google Scholar 

  9. Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E. (ed.) IFIP Conf. on Formal Description of Programming Concepts, pp. 237–277. North- Holland (1977)

    Google Scholar 

  10. Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  11. Goguen, J.A., Meseguer, J.: Security policies and security models. IEEE Symposium on Security and Privacy, 11–20 (1982)

    Google Scholar 

  12. Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Sec. 8(6), 399–422 (2009)

    Article  Google Scholar 

  13. Kay, M.: XSL transformations (XSLT) version 2.0. World Wide Web Consortium, Recommendation REC-xslt20-20070123 (January 23, 2007), http://www.w3.org/TR/xslt20/

  14. Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol. 641, pp. 125–140. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  15. Kovács, M., Seidl, H., Finkbeiner, B.: Relational abstract interpretation for the verification of 2-hypersafety properties. In: Sadeghi, A.R., Gligor, V.D., Yung, M. (eds.) ACM Conference on Computer and Communications Security (CCS 2013), pp. 211–222. ACM (2013)

    Google Scholar 

  16. Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Appel, A.W., Aiken, A. (eds.) Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999, pp. 228–241. ACM (1999)

    Google Scholar 

  17. Nanevski, A., Banerjee, A., Garg, D.: Dependent type theory for verification of information flow and access control policies. ACM Trans. Program. Lang. Syst. 35(2), 6 (2013)

    Article  Google Scholar 

  18. Nielson, F., Riis Nielson, H., Seidl, H.: Normalizable horn clauses, strongly recognizable relations, and spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 20–35. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Pawlik, M., Augsten, N.: RTED: A robust algorithm for the tree edit distance. PVLDB 5(4), 334–345 (2011)

    Google Scholar 

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

    Article  Google Scholar 

  21. Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Application, pp. 189–233. Prentice-Hall (1981)

    Google Scholar 

  22. Stewart, G., Banerjee, A., Nanevski, A.: Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. In: Peña, R., Schrijvers, T. (eds.) 15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013), pp. 145–156. ACM (2013)

    Google Scholar 

  23. Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  24. Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. Journal of Computer Security 4(2/3), 167–188 (1996)

    Google Scholar 

  25. Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität München, Germany

    Helmut Seidl & Máté Kovács

Authors
  1. Helmut Seidl
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Máté Kovács
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Research Group on Mathematical Linguistics, Rovira i Virgili University, Avinguda Catalunya, 35, 43002, Tarragona, Spain

    Adrian-Horia Dediu  & Carlos Martín-Vide  & 

  2. School of Computer Science, Department of Software Engineering and Artificial Intelligence, Complutense University of Madrid, Professor José Garcia Santesmases, 9, 28040, Madrid, Spain

    José-Luis Sierra-Rodríguez

  3. Fakultät für Informatik, Institut für Wissens- und Sprachverarbeitung, Otto-von-Guericke-Universität Magdeburg, Universitätsplatz 2, 39106, Magdeburg, Germany

    Bianca Truthe

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Seidl, H., Kovács, M. (2014). Interprocedural Information Flow Analysis of XML Processors. In: Dediu, AH., Martín-Vide, C., Sierra-Rodríguez, JL., Truthe, B. (eds) Language and Automata Theory and Applications. LATA 2014. Lecture Notes in Computer Science, vol 8370. Springer, Cham. https://doi.org/10.1007/978-3-319-04921-2_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-04921-2_4

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-04920-5

  • Online ISBN: 978-3-319-04921-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation