Professor Tevfik Bultan recently received a National Science Foundation grant for a project titled "Data Model Verification". The three-year, $499,888 grant will seek to develop innovative approaches to software verification, particularly focusing on code that manipulates and updates the data in modern software systems.
Increasingly, software applications are web-based and not bound to the computing devices we use. These modern software applications store the data in remote data centers using cloud computing platforms. In this modern computing landscape, software becomes a service that is accessible from any device anywhere, anytime. This saves users from hassles of local data storage, software installation, configuration management, and security patches.
However, these benefits come with a cost: the increasing complexity of software applications. Modern software applications are distributed systems that consist of multiple components that run in parallel on multiple machines in the cloud. Developing such software systems is an extremely difficult and error-prone task, with developers often not being able to find all bugs in the software before it is released to the users. Such bugs lead to unintended behaviors, security vulnerabilities, and crashes. The fact that existing software development practices are unable to produce dependable web applications was recently demonstrated by the well publicized problems of the HealthCare.gov website.
Prof. Bultan's research group has been investigating new ways to find and eliminate bugs in modern software systems. The group develops software that checks software with the mindset that computers are used to automate so many tasks, why not use them for looking for errors in computer software? It turns out that the process of looking for errors in software, called "software verification", is a challenging task. The group focuses on code that manipulates and updates data as this is an extremely critical problem as we keep moving private and sensitive information like health records to the remote data servers in the cloud.
To tackle the software verification problem Prof. Bultan's group has been developing techniques that automatically translate the code that manipulates and updates data into formulas in mathematical logic. After this translation, the task of looking for errors in code becomes a task of checking if a logic formula is satisfiable. Computer scientists have spent much work studying the resulting problem and have developed specialized software for testing satisfiability, which can now be applied to software verification.
In a recent paper titled "Inductive Verification of Data Model Invariants for Web Applications," which was presented at the 36th International Conference of Software Engineering, Prof. Bultan and his Ph.D. student Ivan Bocic demonstrated that they can automatically discover difficult to find errors in software using this approach. They found four previously unknown bugs in three open source web applications and reported them to the developers, who immediately confirmed and fixed them. This new project will enable Prof. Bultan's group to extend their approach to a larger class of bugs and develop techniques for automatically correcting the bugs that are discovered by their approach.