Alexandria Digital Research Library

Data model verification via theorem proving

Author:
Bocic, Ivan
Degree Grantor:
University of California, Santa Barbara. Computer Science
Degree Supervisor:
Tevfik Bultan
Place of Publication:
[Santa Barbara, Calif.]
Publisher:
University of California, Santa Barbara
Creation Date:
2016
Issued Date:
2016
Topics:
Computer science
Keywords:
Data models
Software analysis
Verification
Web applications
Genres:
Dissertations, Academic and Online resources
Dissertation:
Ph.D.--University of California, Santa Barbara, 2016
Description:

Software applications have moved from desktop computers onto the web. This is not surprising since there are many advantages that web applications provide, such as ubiquitous access and distributed processing power. However, these benefits come at a cost. Web applications are complex distributed systems written in multiple languages. As such, they are prone to errors at any stage of development, and difficult to verify, or even test. Considering that web applications store and manage data for millions (even billions) of users, errors in web applications can have disastrous effects.

In this dissertation, we present a method for verifying code that is used to access and modify data in web applications. We focus on applications that use frameworks such as Ruby on Rails, Django or Spring. These frameworks are RESTful, enforce the Model-View-Controller architecture, and use Object Relational Mapping libraries to manipulate data. We developed a formal model for data stores and data store manipulation, including access control. We developed a translation of these models to formulas in First Order Logic (FOL) that allows for verification of data model invariants using off-the-shelf FOL theorem provers. In addition, we developed a method for extracting these models from existing applications implemented in Ruby on Rails. Our results demonstrate that our approach is applicable to real world applications, it is able to discover previously unknown bugs, and it does so within minutes on commonly available hardware.

Physical Description:
1 online resource (160 pages)
Format:
Text
Collection(s):
UCSB electronic theses and dissertations
ARK:
ark:/48907/f3pr7w57
ISBN:
9781369575842
Catalog System Number:
990047511680203776
Rights:
Inc.icon only.dark In Copyright
Copyright Holder:
Ivan Bocic
File Description
Access: Public access
Bocic_ucsb_0035D_13245.pdf pdf (Portable Document Format)