Skip to main content
SpringerLink
Log in

An Executable Formal Semantics of PHP

  • Conference paper
ECOOP 2014 – Object-Oriented Programming (ECOOP 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8586))

Included in the following conference series:

Abstract

PHP is among the most used languages for server-side scripting. Although substantial effort has been spent on the problem of automatically analysing PHP code, vulnerabilities remain pervasive in web applications, and analysis tools do not provide any formal guarantees of soundness or coverage. This is partly due to the lack of a precise specification of the language, which is highly dynamic and often exhibits subtle behaviour.

We present the first formal semantics for a substantial core of PHP, based on the official documentation and experiments with the Zend reference implementation. Our semantics is executable, and is validated by testing it against the Zend test suite. We define the semantics of PHP in a term-rewriting framework which supports LTL model checking and symbolic execution. As a demonstration, we extend LTL with predicates for the verification of PHP programs, and analyse two common PHP functions.

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. Arusoaie, A., Lucanu, D., Rusu, V.: A Generic Framework for Symbolic Execution. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 281–301. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  2. Bertot, Y., Castéran, P., Huet, G., Paulin-Mohring, C.: Interactive Theorem Proving and Program Development - Coq’Art - the Calculus of Inductive Constructions. Texts in theoretical computer science. Springer (2004)

    Google Scholar 

  3. Blazy, S., Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language. Journal of Automated Reasoning 43, 263–288 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  4. Bodin, M., Charguéraud, A., Filaretti, D., Gardner, P., Maffeis, S., Schmitt, A., Smith, G.: A Trusted Mechanised JavaScript Specification. In: POPL 2014 (2014)

    Google Scholar 

  5. Bogdanas, D.: Formal Semantics of Java in the K Framework, https://github.com/kframework/java-semantics

  6. Bogdanas, D.: Label-Based Programming Language Semantics in the K Framework with SDF. In: SYNASC 2012, pp. 170–177 (2012)

    Google Scholar 

  7. Bouwers, E.: PHP-Sat, http://www.program-transformation.org/PHP/PhpSat

  8. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and Programming in Rewriting Logic. Theoretical Computer Science 285(2), 187–243 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  9. Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL 1977, pp. 238–252 (1977)

    Google Scholar 

  10. PHP Documentation. Cryptographic Function pbkdf2, http://php.net/manual/en/function.hash-hmac.php

  11. Ellison, C., Roşu, G.: An Executable Formal Semantics of C with Applications. In: POPL 2012, pp. 533–544 (2012)

    Google Scholar 

  12. Free Software Foundation. GCC Torture Suite, http://gcc.gnu.org/onlinedocs/gccint/C-Tests.html

  13. The PHP Group. PHP Official Documentation, http://www.php.net/manual/en/

  14. The PHP Group. PHP Zend Engine, http://php.net

  15. Guha, A., Saftoiu, C., Krishnamurthi, S.: The Essence of Javascript. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 126–150. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Guth, D.: Python Semantics in K, http://code.google.com/p/k-python-semantics/

  17. Heering, J., Hendriks, P.R.H., Klint, P., Rekers, J.: The Syntax Definition Formalism SDF - Reference Manual. SIGPLAN Not. 24(11), 43–75 (1989)

    Article  Google Scholar 

  18. ECMA International. ECMA-262 ECMAScript Language Specification (2009), http://www.ecma-international.org/publications/standards/Ecma-262.htm

  19. International Organization for Standardization. C Language Specification - C11. ISO/IEC 9899:2011 (2011), http://www.iso.org/iso/iso_catalogue/catalogue_tc/catalogue_detail.htm?csnumber=57853

  20. Jhala, R., Majumdar, R.: Software Model Checking. ACM Compututing Surveys 41(4) (2009)

    Google Scholar 

  21. Jovanovic, N., Kruegel, C., Kirda, E.: Static Analysis for Detecting Taint-Style Vulnerabilities in Web Applications. Journal of Computer Security 18(5), 861–907 (2010)

    Google Scholar 

  22. Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, A., Rafkind, J., Tobin-Hochstadt, S., Findler, R.B.: Run Your Research: On the Effectiveness of Lightweight Mechanization. In: POPL 2012, pp. 285–296 (2012)

    Google Scholar 

  23. Lazar, D.: Haskell Semantics in K, https://github.com/davidlazar/haskell-semantics

  24. Lucanu, D., Rusu, V.: Program Equivalence by Circular Reasoning. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 362–377. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  25. Maffeis, S., Mitchell, J.C., Taly, A.: An Operational Semantics for JavaScript. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 307–325. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  26. Maffeis, S., Mitchell, J.C., Taly, A.: Isolating JavaScript with Filters, Rewriting, and Wrappers. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 505–522. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  27. Maffeis, S., Taly, A.: Language-Based Isolation of Untrusted JavaScript. In: CSF 2009, pp. 77–91 (2009)

    Google Scholar 

  28. Meredith, P., Hills, M., Roşu, G.: A K Definition of Scheme. Technical Report Department of Computer Science UIUCDCS-R-2007-2907, University of Illinois at Urbana-Champaign (2007)

    Google Scholar 

  29. Meredith, P., Katelman, M., Meseguer, J., Roşu, G.: A Formal Executable Semantics of Verilog. In: MEMOCODE 2010, pp. 179–188 (2010)

    Google Scholar 

  30. pR. Milner, M. Tofte, and D. Macqueen. The Definition of Standard ML. MIT Press (1997)

    Google Scholar 

  31. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    Book  MATH  Google Scholar 

  32. Norrish, M.: C Formalised in HOL. University of Cambridge Technical Report UCAM-CL-TR-453 (1998)

    Google Scholar 

  33. phpMyAdmin Team. phpMyAdmin, http://www.phpmyadmin.net/home_page/index.php

  34. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    Google Scholar 

  35. Politz, J.G., Martinez, A., Milano, M., Warren, S., Patterson, D., Li, J., Chitipothu, A., Krishnamurthi, S.: Python: the Full Monty. In: OOPSLA 2013 (2013)

    Google Scholar 

  36. Roşu, G., Ştefănescu, A.: Checking Reachability using Matching Logic. In: OOPSLA 2012, pp. 555–574 (2012)

    Google Scholar 

  37. Roşu, G., Şerbănuţă, T.F.: An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)

    Google Scholar 

  38. Fortify Team. Fortify Code Secure, http://www.armorize.com/codesecure/

  39. K Team. The K Framework, http://k-framework.org/index.php/Main_Page

  40. PHP Quality Assurance Team. Zend Test Suite, https://qa.php.net/write-test.php

  41. Tozawa, A., Tatsubori, M., Onodera, T., Minamide, Y.: Copy-On-Write in the PHP Language. In: POPL 2009, pp. 200–212 (2009)

    Google Scholar 

  42. Woo, T.Y.C., Lam, M.: A Semantic Model for Authentication Protocols. In: Security and Privacy (SP), pp. 178–194 (1993)

    Google Scholar 

  43. Xie, Y., Aiken, A.: Static Detection of Security Vulnerabilities in Scripting Languages. In: USENIX 2006 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College London, London, UK

    Daniele Filaretti & Sergio Maffeis

Authors
  1. Daniele Filaretti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sergio Maffeis
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, University of Kent, Canterbury, Kent, UK

    Richard Jones

1 Electronic Supplementary Material

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Filaretti, D., Maffeis, S. (2014). An Executable Formal Semantics of PHP. In: Jones, R. (eds) ECOOP 2014 – Object-Oriented Programming. ECOOP 2014. Lecture Notes in Computer Science, vol 8586. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44202-9_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-44202-9_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-44201-2

  • Online ISBN: 978-3-662-44202-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation