polyLarva plugin for PHP

Abstract

Web Applications (WA) are increasingly being expected to behave correctly with a high degree of confidence with the growing presence of mission, safety and business critical applications over the web, as they allow no room for failure as lives could be lost or financial losses could be incurred. PHP is a popular scripting language designed specifically for dynamic web page creation, used for the development of mainstream WAs such as Moodle and Wordpress. Its dynamic and concise nature aids in achieving development targets faster than the alternatives. However, its dynamicity renders verification techniques, based on exhaustive traversal of the state space, such as model checking, not suitable for its verification. Runtime Verification (RV) is a light-weight verification technique that has been shown to be a viable solution for the verification of large complex systems. polyLarva is a technology-agnostic RV tool that can be extended for the run time verification of systems developed in any technology, given the availability of a technology-specific plugin. In this work, we present our approach to extending polyLarva with a PHP plugin, for the runtime verification of any PHP WA. poly Larva had never been extended to scripting languages before, and this presented a new category of challenges for its extension to PHP. For poly Larva to be able to monitor a PHP WA, it is first required that target PHP WA scripts be enhanced with monitoring functionality so that their behaviour becomes observable. Once their behaviour can be observed, properties can be defined, using the polyLarva specification language, for the verification of such behaviour. Following a thorough investigation of the PHP language and ways of expressing correctness properties on such language, we came up with a PHP plugin that was eventually tested in a case study on an e-learning PHP WA called Moodle. A number of properties, based on configurations from a real-life Moodle installation, have been successfully verified by poly Larva by means of the PHP plugin. Through the verified properties we were able to show that the PHP plugin is able to employ monitoring functionality for different real-life properties, specified on PHP script code behaviour, while supporting the flexibility allowed by polyLarva of splitting such properties across the monitored system and the monitor.