Automated Verification and Web Flow

I 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.

Note: This post is a slightly modified version of the one taken from my web site, found here. As I have had issues uploading images here, only the aforementioned link contains the images referenced here.

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.

src="images/cs267/figure3.jpg">

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.

This entry was posted on Thursday, May 15th, 2008 at 8:19 am and is filed under Java, PHP, Spring, The Internets, Zend. You can follow any responses to this entry through the RSS 2.0 feed. Both comments and pings are currently closed.

Comments are closed.