Eliminating navigation errors in web applications via model checking and runtime enforcement of navigation state machines

Abstract

The enforcement of navigation constraints in web applications is challenging and error prone due to the unrestricted use ofnavigation functions inweb browsers. This often leads to navigation errors, producing cryptic messages and exposinginformation thatcanbeexploitedbymalicious users. We propose a runtime enforcement mechanism that restricts the control flow of a web application to a state machine model specified by the developer, and use model checking to verify temporal properties on these state machines. Our experiments, performed on three real-world applications, show that 1) our runtime enforcement mechanism incurs negligible overhead under normal circumstances, and can even reduceserverprocessingtimeinhandlingunexpectedrequests; 2) by combining runtime enforcement with model checking, navigation correctness can be efficiently guaranteed in large web applications.