Specification and Verification of Web Applications in Rewriting Logic

MarĂ­a Alpuente, Demis Ballis and Daniel Romero

Abstract

This work presents a Rewriting Logic framework for the formal specification of the operational semantics of Web applications. More precisely, we define a rewrite theory which precisely formalizes the interactions between Web servers and Web browsers through a communicating protocol abstracting the HyperText Transfer Protocol (HTTP).

Our model also supports a scripting language, encompassing the main features of the principal Web scripting languages (e.g. PHP, ASP, Java Servlets), which is powerful enough to model complex Web application. as well as advanced navigation capabilities such as adaptive navigation (that is, a form of navigation through a Web application which can be dynamically customized according to both user and session information). A detailed characterization of browser actions (e.g. forward/backward navigation, refresh, and new window/tab openings) via rewrite rules completes the proposed specification.

Our formalization is particularly suitable for verification purposes, since it allows one to carry out in-depth analyses of several subtle aspects of Web interactions. To this respect, we show how our models can be naturally model-checked by using the Linear Temporal Logic of Rewriting (LTLR) which is a Linear Temporal Logic specifically designed for model-checking rewrite theories.

Finally, the framework has been completely implemented in Maude, and some experiments have been conducted using the Maude LTLR model-checker.

Description

We define a fine-grained, operational semantics of Web applications based on a formal navigational model which is suitable for the verification of real, dynamic Web sites. Our model is formalized within the Rewriting Logic (RWL) framework, a rule-based, logical formalism particularly appropriate to modeling concurrent systems. Specifically, we provide a rigorous rewrite theory which

We also show how rewrite theories specifying Web application models can be model-checked using the Linear Temporal Logic of Rewriting} (LTLR). The LTLR allows us to specify properties at a very high level using RWL rules and hence can be smoothly integrated into our RWL framework.

Finally, the verification framework has been implemented in Maude, a high-performance RWL language, which is equipped with a built-in model-checker for LTLR. By using our prototype, we conducted an experimental evaluation which demonstrates the usefulness of our approach.

To the best of our knowledge, this work represents the first attempt to provide a formal RWL verification environment for Web applications which allows one to verify several important classes of properties (e.g. reachability, security, authentication constraints, mutual exclusion, liveness, etc. w.r.t. a realistic model of a Web application which includes detailed browser-server protocol interactions, browser navigation capabilities, and Web script evaluations.

Example

Consider the navigation model given in Figure 1 representing a generic Webmail application which provides some typical functions such as login/logout features, email management, system administration capabilities, etc. The Web pages of the application are pairwise connected by either navigation links (solid arrows) or continuations (dashed arrows). For example, the solid arrow between the welcome and the home page whose label is ∅,user=x,pass=y defines a navigation link which is always enabled and requires two input parameters. The home page has got two possible continuations (dashed arrows) login=ok and login=no. Only one of them is chosen, according to the user and pass values provided in the previous transition. In the former case the login succeeds and the home page is delivered to the browser, while in the latter case the login fails and the welcome page is sent back to the browser.

An example of adaptive navigation is provided by the navigation link connecting the home page to the administration page. In fact, navigation through that link is enabled only when the condition role=admin holds, that is, the role of the logged user is admin.

Figure 1
Figure 1

The structure of this Web application can be defined in our framework as follows (the whole example is available together with the sources of the tool):

(fmod WEBMAIL is inc PROTOCOL .

 --- Page name
 ops WELCOME HOME ADMINISTRATION EMAIL-LIST VIEW-EMAIL CHANGE-ACCOUNT ADMIN-LOGOUT LOGOUT : -> Qid .
 
 --- Web application
 op wapp : -> Page .
 eq wapp =  welcomePage : homePage : emailListPage : viewEmailPage  : 
            changeAccountPage : administrationPage  : adminLogoutPage : logoutPage   .

 --- Welcome page
 op welcomePage : -> Page .
 eq welcomePage = ( WELCOME , skip , 
                   { cont-empty } , 
                   { ( TRUE  -> ( HOME ? ('user '= "") : ('pass '= "")  ) ) } ) .

 --- Home page
 op homePage : -> Page .
 eq homePage = ( HOME, sHome, { (( s("login") '== s("no") ) => WELCOME ) : 
                                (( s("changeLogin") '== s("no") ) => CHANGE-ACCOUNT ) : 
                                (( s("login") '== s("ok") ) => HOME )								  
                              } , 
                              { (TRUE -> CHANGE-ACCOUNT ? query-empty ) :
                                (( s("role") '== s("admin")) -> ( ADMINISTRATION ? query-empty )) : 
                                (TRUE -> EMAIL-LIST ? query-empty ) :
                                (TRUE -> LOGOUT ? query-empty )
                              } ) .

 op sHome : -> Script .
 eq sHome = 
    'login := getSession( s("login") ) ;
    if ( 'login = null ) then 
        'u := getQuery('user) ;
        'p := getQuery('pass) ;
        'p1 := selectDB('u) ;
         if ( 'p = 'p1 ) then
            'r := selectDB('u '. s("-role") ) ;
            setSession( s("user") , 'u ) ; 
            setSession( s("role") , 'r ) ; 
            setSession( s("login") , s("ok") ) 
         else
            setSession( s("login") , s("no") )
         fi
     fi
     .
 ..... 

endfm)

On the other hand, we can define state predicates in order to evaluate propositions on the states. For example, consider the two following state predicates where: (i) currentPage evaluates to true when a given page passed as parameter is being displayed in the browser; (ii) requestHome holds when there is a requirement to go to the home page. These predicates can be defined as follows:

(fmod WEBMAIL-CHECK is pr TLR[WEBMAIL] .    

 subsorts WebState < State .
 
 vars idb idw : Id .
 vars page : Qid .
 vars url  : URL .
 vars z : Sigma .
 vars lms ms  : Message .
 vars brs : Browser .
 vars sv : Server .
 vars q : Query .
 vars i : Nat .
 
 --- current page
 op currentPage : Id Qid -> Prop .
 eq [ B(idb, idw, page, urls, z, lms, h, n, idlm) : brs ] [ ms ] [ sv ] |= currentPage(idb, page) = true .
 eq [ brs ] [ ms ] [ sv ] |= currentPage(idb, page) = false [owise] .
 
 --- request to go to home
 op requestHome : Id -> Prop .
 eq [ brs ] [ m(idb, idw, (HOME ? q ), i ) : ms ] [ sv ] |= requestHome(idb) = true .
 eq [ brs ] [ ms ] [ sv ] |= requestHome(idb) = false [owise] .

endfm)

Then, we can check properties such as the following liveness property "the user IdA can always access the system" by means of the following LTRL formula.

Maude> (tlr check( initial, [] ((currentPage(idA, WELCOME) /\ 
                                 O requestHome(idA)) -> (<> currentPage(idA, HOME))) ) .)


Download

The preliminary prototype along with some examples can be downloaded from here.


FEDER MINECO MICINN
GVA UPV DSIC