Runtime Verification of Critical Web-based Systems with Lola
Marvin Hofmann
A bug in the code base of a given program can expose the system and can cause failures. These may impact not only the availability of the system but also the integrity of the data. Bugs are hard to predict and can cause millions of dollars in damage. Therefore, preventing these bugs is an important objective, principally, but not only, considering critical systems like financial applications. In web-based systems, automated testing is a common approach to detect bugs before they are deployed into a production environment, preventing the bugs from causing harm to the system. However, testing can only verify code paths explicitly chosen to be tested, and actual usage can differ. This pushes the responsibility to the developers to decide what code paths are critical and require a test. At the same time, tests can also contain bugs and impose a maintenance overhead. Therefore, a solution is desirable, that can help to protect from damages caused by bugs. This solution needs to be easy to use while imposing as little as possible additional overhead onto the developers. At the same time, it should cover all traversed code paths and be human readable in what is checked. Moreover, it should not itself be a source of bugs. We introduce Ruby-Lola, a framework for synchronous runtime verification of web-based systems. Ruby-Lola is based on the Lola stream-based specification language, a simple and expressive language that can describe correctness/failure states of a system. The framework provides a domain-specific language to write specifications for runtime verification in an object-oriented way, allowing for references between database tables and a clean syntax that is familiar to developers. Moreover, Ruby-Lola can be used in combination with automated tests, improving their coverage through the specification. We implemented the framework and applied it to a case study of a web-based system that models an auction house, a practical and critical application. This demonstrates that our framework is sufficient to express complex specifications and that it can detect and mitigate critical bugs in practical applications. We also show that the framework is easy to use and serves as additional documentation. Ruby-Lola imposes minimal overhead related to other costs of processing user requests and is therefore not noticeable by end users in practical usage. Github: https://github.com/reggaemuffin/lola-ruby
Bachelor Thesis.