Inductive verification of data model invariants in web applications using first-order logic

Modern software applications store their data in remote cloud servers. Users interact with these applications using web browsers or thin clients running on mobile devices. A key concern for these applications is the correctness of the actions that update the data store, which are triggered by user requests. Considering that modern applications store and manage data for millions (even billions) of users, misuse or loss of user data can have catastrophic consequences. In this paper, we focus on automated discovery of data store bugs in applications that use development frameworks that are RESTful, enforce the Model–View–Controller architecture, and use Object Relational Mapping libraries to manipulate data. We present a formal data model for data stores and data store manipulation in such applications. We have developed a framework for verification of data models via translation to First Order Logic (FOL), followed by automated theorem proving. Due to the undecidability of FOL, this automated approach does not always produce a conclusive answer. We investigate the use of many-sorted logic in data model verification in order to improve the effectiveness of this approach. Many-sorted logic allows us to specify type information explicitly, thus lightening the burden of reasoning about type information during theorem proving. Our experimental results demonstrate that our verification approach is scalable to real-world web applications and is able to detect bugs in them.