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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
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)
Blazy, S., Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language. Journal of Automated Reasoning 43, 263–288 (2009)
Bodin, M., Charguéraud, A., Filaretti, D., Gardner, P., Maffeis, S., Schmitt, A., Smith, G.: A Trusted Mechanised JavaScript Specification. In: POPL 2014 (2014)
Bogdanas, D.: Formal Semantics of Java in the K Framework, https://github.com/kframework/java-semantics
Bogdanas, D.: Label-Based Programming Language Semantics in the K Framework with SDF. In: SYNASC 2012, pp. 170–177 (2012)
Bouwers, E.: PHP-Sat, http://www.program-transformation.org/PHP/PhpSat
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)
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)
PHP Documentation. Cryptographic Function pbkdf2, http://php.net/manual/en/function.hash-hmac.php
Ellison, C., Roşu, G.: An Executable Formal Semantics of C with Applications. In: POPL 2012, pp. 533–544 (2012)
Free Software Foundation. GCC Torture Suite, http://gcc.gnu.org/onlinedocs/gccint/C-Tests.html
The PHP Group. PHP Official Documentation, http://www.php.net/manual/en/
The PHP Group. PHP Zend Engine, http://php.net
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)
Guth, D.: Python Semantics in K, http://code.google.com/p/k-python-semantics/
Heering, J., Hendriks, P.R.H., Klint, P., Rekers, J.: The Syntax Definition Formalism SDF - Reference Manual. SIGPLAN Not. 24(11), 43–75 (1989)
ECMA International. ECMA-262 ECMAScript Language Specification (2009), http://www.ecma-international.org/publications/standards/Ecma-262.htm
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
Jhala, R., Majumdar, R.: Software Model Checking. ACM Compututing Surveys 41(4) (2009)
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)
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)
Lazar, D.: Haskell Semantics in K, https://github.com/davidlazar/haskell-semantics
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)
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)
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)
Maffeis, S., Taly, A.: Language-Based Isolation of Untrusted JavaScript. In: CSF 2009, pp. 77–91 (2009)
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)
Meredith, P., Katelman, M., Meseguer, J., Roşu, G.: A Formal Executable Semantics of Verilog. In: MEMOCODE 2010, pp. 179–188 (2010)
pR. Milner, M. Tofte, and D. Macqueen. The Definition of Standard ML. MIT Press (1997)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Norrish, M.: C Formalised in HOL. University of Cambridge Technical Report UCAM-CL-TR-453 (1998)
phpMyAdmin Team. phpMyAdmin, http://www.phpmyadmin.net/home_page/index.php
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
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)
Roşu, G., Ştefănescu, A.: Checking Reachability using Matching Logic. In: OOPSLA 2012, pp. 555–574 (2012)
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)
Fortify Team. Fortify Code Secure, http://www.armorize.com/codesecure/
K Team. The K Framework, http://k-framework.org/index.php/Main_Page
PHP Quality Assurance Team. Zend Test Suite, https://qa.php.net/write-test.php
Tozawa, A., Tatsubori, M., Onodera, T., Minamide, Y.: Copy-On-Write in the PHP Language. In: POPL 2009, pp. 200–212 (2009)
Woo, T.Y.C., Lam, M.: A Semantic Model for Authentication Protocols. In: Security and Privacy (SP), pp. 178–194 (1993)
Xie, Y., Aiken, A.: Static Detection of Security Vulnerabilities in Scripting Languages. In: USENIX 2006 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
1 Electronic Supplementary Material
Rights 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)