An Executable Formal Semantics of PHP
An Executable Formal Semantics of PHP
复制标题
DOI：
10.1007/978-3-662-44202-9_23
复制
发表时间：
2014-08
期刊：
影响因子：
--
通讯作者：
Daniele Filaretti;S. Maffeis
中科院分区：
文献类型：
--
作者：
Daniele Filaretti;S. Maffeis
PHP是服务器端脚本最常用的语言之一。尽管在自动分析PHP代码的问题上已经花费了大量的努力，但漏洞仍然普遍存在于Web应用程序中，并且分析工具不能提供任何正式的可靠性或覆盖率保证。这部分是由于缺乏一个精确的规范的语言，这是高度动态的，往往表现出微妙的behavior.We提出了第一个正式的语义为实质性的PHP核心，基于官方文档和实验的Zend参考实现。我们的语义是可执行的，并通过测试它对Zend测试套件进行验证。我们定义了一个术语重写框架，支持LTL模型检查和符号执行的PHP的语义。作为示范，我们扩展LTL与谓词的PHP程序的验证，并分析了两个常见的PHP函数。
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.