Advertisement

An Executable Formal Semantics of PHP

  • Daniele Filaretti
  • Sergio Maffeis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8586)

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.

Keywords

Model Check Test Suite Array Element Formal Semantic Linear Temporal Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Supplementary material

978-3-662-44202-9_23_MOESM1_ESM.zip (267.4 mb)
Electronic Supplementary Material(118 KB)

References

  1. 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)CrossRefGoogle Scholar
  2. 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. 3.
    Blazy, S., Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language. Journal of Automated Reasoning 43, 263–288 (2009)CrossRefMATHMathSciNetGoogle Scholar
  4. 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. 5.
    Bogdanas, D.: Formal Semantics of Java in the K Framework, https://github.com/kframework/java-semantics
  6. 6.
    Bogdanas, D.: Label-Based Programming Language Semantics in the K Framework with SDF. In: SYNASC 2012, pp. 170–177 (2012)Google Scholar
  7. 7.
  8. 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)CrossRefMATHMathSciNetGoogle Scholar
  9. 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. 10.
    PHP Documentation. Cryptographic Function pbkdf2, http://php.net/manual/en/function.hash-hmac.php
  11. 11.
    Ellison, C., Roşu, G.: An Executable Formal Semantics of C with Applications. In: POPL 2012, pp. 533–544 (2012)Google Scholar
  12. 12.
    Free Software Foundation. GCC Torture Suite, http://gcc.gnu.org/onlinedocs/gccint/C-Tests.html
  13. 13.
    The PHP Group. PHP Official Documentation, http://www.php.net/manual/en/
  14. 14.
    The PHP Group. PHP Zend Engine, http://php.net
  15. 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)CrossRefGoogle Scholar
  16. 16.
    Guth, D.: Python Semantics in K, http://code.google.com/p/k-python-semantics/
  17. 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)CrossRefGoogle Scholar
  18. 18.
    ECMA International. ECMA-262 ECMAScript Language Specification (2009), http://www.ecma-international.org/publications/standards/Ecma-262.htm
  19. 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. 20.
    Jhala, R., Majumdar, R.: Software Model Checking. ACM Compututing Surveys 41(4) (2009)Google Scholar
  21. 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. 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. 23.
    Lazar, D.: Haskell Semantics in K, https://github.com/davidlazar/haskell-semantics
  24. 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)CrossRefGoogle Scholar
  25. 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)CrossRefGoogle Scholar
  26. 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)CrossRefGoogle Scholar
  27. 27.
    Maffeis, S., Taly, A.: Language-Based Isolation of Untrusted JavaScript. In: CSF 2009, pp. 77–91 (2009)Google Scholar
  28. 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. 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. 30.
    pR. Milner, M. Tofte, and D. Macqueen. The Definition of Standard ML. MIT Press (1997)Google Scholar
  31. 31.
    Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)CrossRefMATHGoogle Scholar
  32. 32.
    Norrish, M.: C Formalised in HOL. University of Cambridge Technical Report UCAM-CL-TR-453 (1998)Google Scholar
  33. 33.
    phpMyAdmin Team. phpMyAdmin, http://www.phpmyadmin.net/home_page/index.php
  34. 34.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)Google Scholar
  35. 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. 36.
    Roşu, G., Ştefănescu, A.: Checking Reachability using Matching Logic. In: OOPSLA 2012, pp. 555–574 (2012)Google Scholar
  37. 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. 38.
    Fortify Team. Fortify Code Secure, http://www.armorize.com/codesecure/
  39. 39.
  40. 40.
    PHP Quality Assurance Team. Zend Test Suite, https://qa.php.net/write-test.php
  41. 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. 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. 43.
    Xie, Y., Aiken, A.: Static Detection of Security Vulnerabilities in Scripting Languages. In: USENIX 2006 (2006)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Daniele Filaretti
    • 1
  • Sergio Maffeis
    • 1
  1. 1.Department of ComputingImperial College LondonLondonUK

Personalised recommendations