research-article

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

Authors:

Sylvain Hallé,

Tevfik BultanAuthors Info & Claims

ASE '10: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering

Pages 235 - 244

https://doi.org/10.1145/1858996.1859044

Published: 20 September 2010 Publication History

Abstract

The enforcement of navigation constraints in web applications is challenging and error prone due to the unrestricted use of navigation functions in web browsers. This often leads to navigation errors, producing cryptic messages and exposing information that can be exploited by malicious 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 reduce server processing time in handling unexpected requests; 2) by combining runtime enforcement with model checking, navigation correctness can be efficiently guaranteed in large web applications.

References

[1]

}}19th IEEE International Conference on Automated Software Engineering (ASE 2004), 20-25 September 2004, Linz, Austria. IEEE Computer Society, 2004.

[2]

}}D. A. Basin, F. Klaedtke, S. Müller, and B. Pfitzmann. Runtime monitoring of metric first-order temporal properties. In R. Hariharan, M. Mukund, and V. Vinay, editors, FSTTCS, volume 2 of LIPIcs, pages 49--60. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2008.

[3]

}}A. Betin-Can and T. Bultan. Verifiable web services with hierarchical interfaces. In Proceedings of the IEEE International Conference on Web Services (ICWS 2005), pages 85--94, 2005.

Digital Library

[4]

}}M. Book, T. Brückmann, V. Gruhn, and M. Hülder. Specification and control of interface responses to user input in rich internet applications. In Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering(ASE 2009), pages 321--331, 2009.

Digital Library

[5]

}}M. Book and V. Gruhn. Modeling web-based dialog flows for automatic dialog control. In ASE {1}, pages 100--109.

Digital Library

[6]

}}A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An open-source tool for symbolic model checking. In E. Brinksma and K. G. Larsen, editors, CAV, volume 2404 of Lecture Notes in Computer Science, pages 359--364. Springer, 2002.

Digital Library

[7]

}}L. de Alfaro and T. A. Henzinger. Interface automata. In Proceedings 9th Annual Symposium on Foundations of Software Engineering, pages 109--120, 2001.

Digital Library

[8]

}}L. Desmet, P. Verbaeten, W. Joosen, and F. Piessens. Provable protection against web application vulnerabilities related to session data dependencies. IEEE Trans. Software Eng., 34(1):50--64, 2008.

Digital Library

[9]

}}A. Deutsch, L. Sui, V. Vianu, and D. Zhou. A system for specification and verification of interactive, data-driven web applications. In S. Chaudhuri, V. Hristidis, and N. Polyzotis, editors, SIGMOD Conference, pages 772--774. ACM, 2006.

Digital Library

[10]

}}F. M. Donini, M. Mongiello, M. Ruta, and R. Totaro. A model checking-based method for verifying web application design. Electr. Notes Theor. Comput. Sci., 151(2):19--32, 2006.

Digital Library

[11]

}}A. Guha, S. Krishnamurthi, and T. Jim. Using static analysis for Ajax intrusion detection. In J. Quemada, G. León, Y. S. Maarek, and W. Nejdl, editors, WWW, pages 561--570. ACM, 2009.

Digital Library

[12]

}}S. Hallé and R. Villemaire. Browser-based enforcement of interface contracts in web applications with BeepBeep. In A. Bouajjani and O. Maler, editors, CAV, volume 5643 of Lecture Notes in Computer Science, pages 648--653. Springer, 2009.

Digital Library

[13]

}}M. Han and C. Hofmeister. Relating navigation and request routing models in web applications. In G. Engels, B. Opdyke, D. C. Schmidt, and F. Weil, editors, MoDELS, volume 4735 of Lecture Notes in Computer Science, pages 346--359. Springer, 2007.

Digital Library

[14]

}}M. Haydar. Formal framework for automated analysis and verification of web-based applications. In ASE {1}, pages 410--413.

Digital Library

[15]

}}K. Hokamura, N. Ubayashi, S. Nakajima, and A. Iwai. Aspect-oriented programming for web controller layer. In APSEC, pages 529--536. IEEE Computer Society, 2008.

Digital Library

[16]

}}S. Krishnamurthi, R. B. Findler, P. Graunke, and M. Felleisen. Modeling Web Interactions and Errors, pages 255--275. Springer, 2006.

[17]

}}D. R. Licata and S. Krishnamurthi. Verifying interactive web programs. In ASE {1}, pages 164--173.

Digital Library

[18]

}}H. Miao and H. Zeng. Model checking-based verification of web application. In ICECCS, pages 47--55. IEEE Computer Society, 2007.

Digital Library

[19]

}}E. D. Sciascio, F. M. Donini, M. Mongiello, R. Totaro, and D. Castelluccia. Design verification of web applications using symbolic model checking. In D. Lowe and M. Gaedke, editors, ICWE, volume 3579 of Lecture Notes in Computer Science, pages 69--74. Springer, 2005.

Digital Library

[20]

}}P. D. Stotts, R. Furuta, and C. R. Cabarrus. Hyperdocuments as automata: Verification of trace-based browsing properties by model checking. ACM Trans. Inf. Syst., 16(1):1--30, 1998.

Digital Library

[21]

}}S. Yuen, K. Kato, D. Kato, and K. Agusa. Web automata: A behavioral model of web applications based on the MVC model. Information and Media Technologies, 1(1):66--79, 2006.

Cited By

Ali Mangi FSu GZhang M(2023)PM2PMC: A Probabilistic Model Checking Approach in Process Mining2023 IEEE IAS Global Conference on Emerging Technologies (GlobConET)10.1109/GlobConET56651.2023.10149898(1-6)Online publication date: 19-May-2023
https://doi.org/10.1109/GlobConET56651.2023.10149898
Mangi FSu GZhang M(2023)Integrating Process Mining with Probabilistic Model Checking via Continuous Time Markov Chains2023 Congress in Computer Science, Computer Engineering, & Applied Computing (CSCE)10.1109/CSCE60160.2023.00163(973-978)Online publication date: 24-Jul-2023
https://doi.org/10.1109/CSCE60160.2023.00163
Geng MZhang XLi J(2021)Finding More Property Violations in Model Checking via the Restart PolicyElectronics10.3390/electronics1023295710:23(2957)Online publication date: 27-Nov-2021
https://doi.org/10.3390/electronics10232957
Show More Cited By

Index Terms

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

Recommendations

Modeling and Verifying for Frameset-Based Web Applications
TASE '11: Proceedings of the 2011 Fifth International Conference on Theoretical Aspects of Software Engineering

As Web applications evolve, their structure may be-come more and more complex. Web frameset is used to organize multiple frames and nested framesets to make the layout of some Web pages more identical and bring the development of Web applications easier,...
Robot Navigation Based on Multi-sensor Data Fusion
ICDMA '11: Proceedings of the 2011 Second International Conference on Digital Manufacturing & Automation

This paper mainly focuses on a multi-sensor system for combining data from infrared and ultrasonic sensors in the navigation of coal mine rescue robots, meanwhile a navigation method is presented. A multiple infrared and ultrasonic sensor system has ...
Vision-Based Humanoid Robot Navigation in a Featureless Environment
MCPR 2015: Proceedings of the 7th Mexican Conference on Pattern Recognition - Volume 9116

One of the most basic tasks for any autonomous mobile robot is that of safely navigating from one point to another e.g. service robots should be able to find their way in different kinds of environments. Typically, vision is used to find landmarks in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '10: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering

September 2010

534 pages

ISBN:9781450301169

DOI:10.1145/1858996

General Chair:
Charles Pecheur
Université catholique de Louvain, Belgium
,
Program Chairs:
Jamie Andrews
University of Western Ontario, Canada
,
Elisabetta Di Nitto
Politecnico di Milano, Italy

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 September 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ASE10

Sponsor:

ASE10: IEEE/ACM International Conference on Automated Software Engineering

September 20 - 24, 2010

Antwerp, Belgium

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

41
Total Citations
View Citations
428
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)2

Reflects downloads up to 14 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ali Mangi FSu GZhang M(2023)PM2PMC: A Probabilistic Model Checking Approach in Process Mining2023 IEEE IAS Global Conference on Emerging Technologies (GlobConET)10.1109/GlobConET56651.2023.10149898(1-6)Online publication date: 19-May-2023
https://doi.org/10.1109/GlobConET56651.2023.10149898
Mangi FSu GZhang M(2023)Integrating Process Mining with Probabilistic Model Checking via Continuous Time Markov Chains2023 Congress in Computer Science, Computer Engineering, & Applied Computing (CSCE)10.1109/CSCE60160.2023.00163(973-978)Online publication date: 24-Jul-2023
https://doi.org/10.1109/CSCE60160.2023.00163
Geng MZhang XLi J(2021)Finding More Property Violations in Model Checking via the Restart PolicyElectronics10.3390/electronics1023295710:23(2957)Online publication date: 27-Nov-2021
https://doi.org/10.3390/electronics10232957
Halle SKhoury R(2021)Test Sequence Generation with Cayley Graphs2021 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)10.1109/ICSTW52544.2021.00040(182-191)Online publication date: Apr-2021
https://doi.org/10.1109/ICSTW52544.2021.00040
Zhang G(2020) Specifying and Model Checking Workflows of Single Page Applications with TLA + 2020 IEEE 20th International Conference on Software Quality, Reliability and Security Companion (QRS-C)10.1109/QRS-C51114.2020.00075(406-410)Online publication date: Dec-2020
https://doi.org/10.1109/QRS-C51114.2020.00075
Hayek MFarhat PYamout YGhorra CHaraty R(2019)Web 2.0 Testing Tools: A Compendium2019 International Conference on Innovation and Intelligence for Informatics, Computing, and Technologies (3ICT)10.1109/3ICT.2019.8910274(1-6)Online publication date: Sep-2019
https://doi.org/10.1109/3ICT.2019.8910274
Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Riganelli OMicucci DMariani L(2018)Increasing the Reusability of Enforcers with Lifecycle EventsLeveraging Applications of Formal Methods, Verification and Validation. Industrial Practice10.1007/978-3-030-03427-6_7(51-57)Online publication date: 5-Nov-2018
https://dl.acm.org/doi/10.1007/978-3-030-03427-6_7
Waye LChong SDimoulas C(2017)Whip: higher-order contracts for modern servicesProceedings of the ACM on Programming Languages10.1145/31102801:ICFP(1-28)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110280
Bocić IBultan TUchitel SOrso ARobillard M(2017)Symbolic model extraction for web application verificationProceedings of the 39th International Conference on Software Engineering10.1109/ICSE.2017.72(724-734)Online publication date: 20-May-2017
https://dl.acm.org/doi/10.1109/ICSE.2017.72
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten