Verifying Model-View-Controller Applications
We have spent the Spring 2008 quarter working with Taylor Ettema on finding ways to automatically verify Model-View-Controller applications. Specifically, we discuss here the status report we have given on our work. It should be noted that this page is not intended to be a thorough review of our work on the MVC design pattern and it should be taken as merely a re-iteration of our mid-quarter status report on our work.
Our final paper summarizing our work will be posted here upon its completion. This page contains a modified version of the Google Document that we used to collaborate during the course of this project.
Automated verification has long since proven itself a valuable tool in verifying correctness of traditional applications and embedded systems. With the advent of ubiquitous web applications replacing traditional applications and playing an increased role in critical domains, verification of this new type of program has become of significant importance.
Verification of web applications is a relatively recent area of study, in which classic verification techniques are applied to web application code in order to prove correctness of various aspects of the system. However, the challenges of verifying web applications are quite different from traditional applications. Perhaps the most significant differences are the nature of the state and state transitions. A typical application can be modeled as a state machine in a relatively straight-forward way, as the program code has control over execution flow. The state of the machine is the position within the execution flow, and a union of the values of program variables. The state of a web application, however, is less straight-forward. A use case of a typical web application is composed of dozens of transactions, where each transaction consists of an HTTP request followed by a response issued by the server after some computation.
The inherent developmental and security implications of this segmented nature of execution has led to the adoption of Model-View-Controller (MVC) frameworks that greatly ease development and maintenance of web applications in many popular scripting languages. One such framework, Zend Framework, lends an MVC architecture to web applications written in PHP. The Zend_Controller and Zend_View objects are used in tandem to segment the application into controllers, models, and views, similar to the classic MVC design pattern that has dominated desktop application GUI development for years.
Figure 1: Overview of the
Model-View-Controller (MVC) design pattern.
Figure 2: Overview of the
Zend Framework's implementation of the MVC design pattern (courtesy
Zend, Inc.)
Web applications developed using the MVC design pattern feature a logical separation of message dispatch logic, business logic, and user interface logic that has proven to easy software maintenance significantly. In this work, we examine how this organizational design pattern may also make automated verification for web applications more applicable and powerful.
A review of current literature in the field of web application verification found little on the topic of exploiting applications that employ the Model-View-Controller design pattern. Current literature focuses on web applications constructed in an arbitrary manner, where there is no contract between the server and the client that enforces a particular navigation "flow" between pages. With these types of programs, verification at the application scale was extraordinarily difficult due to the lack of well-defined paths of execution. Whereas entire stand-alone applications may be modeled as a straightforward state machine, modeling a web application in a similar way is very difficult due to the nature of the "state" in an intrinsically stateless protocol such as HTTP. While almost any functional web application overcomes this limitation by maintaining client state information in the form of cookies or URL encodings, these methods are primarily designed to maintain datums such as identification, and are not typically used to enforce a flow of execution.
The primary limitation of the work done by others is that it assumes the navigation flow intended by the programmer is the only possible path of execution. As security researchers know all too well, this is hardly the case. Web applications are exceptionally unique in their model of execution flow, in that application logic is segmented into discrete fragments that get invoked with each HTTP request. The sequence of requests that the user should send is merely suggested by the UI, and is in no way enforced. Thus, models used for verification by others and others simply serve to model check UI components and general application architecture; however, based on the assumptions made about execution flow, these models are all but worthless within the context of security.
Our work thus serves largely as an extension of the work done by others, where we exploit architectural traits specific to the MVC design pattern in an attempt to further what can be accomplished with automated verification. In order to build an automated verification framework for modern MVC-based web applications, we investigated how to enhance the nature of the "state" in a web application. Using cookies to enforce a position and path of execution along a web application state machine would seem to prove quite useful within the context of automated verification. The Spring Framework for Java provides many out-of-the-box solutions for enterprise web application development, including a novel feature called "WebFlow", which allows the developer to segment the web application into distinct "flows" that each have an enforced flow of execution.
While the Spring Framework exists solely for Java, and no
implementations of WebFlow for PHP exist, the MVC architecture provided
by the Zend Framework lends a mechanism that makes the addition of
features such as WebFlow fairly simple. The Zend_Controller class
allows for developers to create "plugins" that can be used to insert
logic throughout each stage of the request handling process, from
pre-routing to post-dispatch loop shutdown. Additionally, the
segmentation of web application logic into "controllers" and "actions"
creates convenient flows and states on which the WebFlow plugin can
operate.
We have therefore implemented a WebFlow-like component for PHP/Zend that operates in a similar fashion as the Spring WebFlow implementation. An XML file denotes the states of the application and the transitions between them, which is strictly enforced by the Controller. For example, a simple application may specify that a user can transition from index to a login page, and from login to any member area. No paths exist directly from index to member area pages, and all member areas lead to a logout page.
We have therefore implemented a WebFlow-like component for PHP/Zend that operates in a similar fashion as the Spring WebFlow implementation. An XML file denotes the states of the application and the transitions between them, which is strictly enforced by the Controller. For example, a simple application may specify that a user can transition from index to a login page, and from login to any member area. No paths exist directly from index to member area pages, and all member areas lead to a logout page.
Figure 3. State machine
representation of the transition specification described by the XML
document.
By utilizing the MVC design pattern along with the WebFlow plugin, we now have an enforceable state machine that can be modeled in a standard verifier tool. Whereas state machine representations of web applications done by others were modeled around "desired" execution flows (and thus can really only be used to verify properties if the user abides by the execution flow suggested by the UI), our models are accurate regardless of the actions of the user.
Our key contribution is the ability to perform automated
verification of an application that employs a WebFlow-like transition
model on top of the MVC application architecture. To accomplish
this, we developed an application that performs automated translation of
a WebFlow XML transition specification to an executable state machine
model in the SMV modeling language. This provides the user with a
realistic model of the application against which propositions can be
verified. For example, a developer may which to verify that all
paths that lead to a members-only page must first pass through
successful authentication on a login page. Alternatively, one can
verify the reachability of pages or the status of various properties at
certain points along a flow of execution.
We also propose an extension of the WebFlow XML
transition specification language that allows for the conditional
setting of user-defined atomic properties. Whereas with the strict
WebFlow specification, our atomic properties are limited to the position
of the state and the response of a script, the addition of conditionally
defined atomic properties makes the formulation of SPEC formulas easier
and more intuitive. The automatically generated SMV model will
create the required code to maintain the atomic properties as specified
in the XML document.
Figure 4. Simple
example of the automated conversion from an XML transition specification
to an executable SMV state machine model. An extension of the
WebFlow language (in bold) allows for the definition and conditional
setting of arbitrary user-defined atomic properties, which are then
added to the SMV state machine model.
Our automated verification system is presented to the
developer as a small web application, appropriately enough. The
user simply provides the WebFlow XML transition specification, as well
as an SMV SPEC formula to verify. The verification program
converts the XML specification into an executable state machine model
and runs SMV in the background, returning the result. Any
counter-example paths are returned to the user using the same naming
conventions as given in the WebFlow XML file, so interpreting the SMV
results should be intuitive for the keen developer.
We believe this to be one of the first deployments of
automated verification on web applications at the application-wide scope
(i.e. not simply verifying a single script, but verifying logic across
the application) that exploits the MVC architecture to handle the
problem of arbitrary transitions between states. By creating a
WebFlow plugin for the Zend Framework for PHP, and developing a
conversion tool from the XML transition specification document to an
executable SMV state machine model, we have created a verification
framework for web applications that can be used to check correctness of
truly useful properties across the scope of the entire application, from
request to request across an entire user session.
Chris Bunch
Last Modification on 05/13/08
First Revision Complete 05/13/08
CSS Style Sheets and Web Layout designed by Ben Meadowcroft
The CSS style sheets used here are licensed under a Creative
Commons License.