Static approximation of dynamically generated Web pages

ABSTRACT

Server-side programming is one of the key technologies that support today's WWW environment. It makes it possible to generate Web pages dynamically according to a user's request and to customize pages for each user. However, the flexibility obtained by server-side programming makes it much harder to guarantee validity and security of dynamically generated pages.To check statically the properties of Web pages generated dynamically by a server-side program, we develop a static program analysis that approximates the string output of a program with a context-free grammar. The approximation obtained by the analyzer can be used to check various properties of a server-side program and the pages it generates.To demonstrate the effectiveness of the analysis, we have implemented a string analyzer for the server-side scripting language PHP. The analyzer is successfully applied to publicly available PHP programs to detect cross-site scripting vulnerabilities and to validate pages they generate dynamically.

REFERENCES

• 1: M. Achour, F. Betz, et~al. PHP Manual, 2005. http://www.php.net/docs.php.
• 2: B. Alpern , M. N. Wegman , F. K. Zadeck, Detecting equality of variables in programs, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-11, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73561]
• 3: Véronique Benzaken , Giuseppe Castagna , Alain Frisch, CDuce: an XML-centric general-purpose language, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.51-63, August 25-29, 2003, Uppsala, Sweden
• 4: J. Berstel. Transductions and Context-Free Languages. Teubner Studienbucher, 1979.
• 5: Claus Brabrand , Anders Møller , Michael I. Schwartzbach, The <bigwig> project, ACM Transactions on Internet Technology (TOIT), v.2 n.2, p.79-114, May 2002 [doi>10.1145/514183.514184]
• 6: Aske Simon Christensen , Anders Møller , Michael I. Schwartzbach, Extending Java for high-level Web service construction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.6, p.814-875, November 2003 [doi>10.1145/945885.945890]
• 7: A. S. Christensen, A. Moller, and M. I. Schwartzbach. Precise analysis of string expressions. In Proceedings of the Static Analysis Symposium (SAS), volume 2694 of LNCS, pages 1--18, 2003.
• 8: Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
• 9: Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
• 10: Carl Gould , Zhendong Su , Premkumar Devanbu, Static Checking of Dynamically Generated Queries in Database Applications, Proceedings of the 26th International Conference on Software Engineering, p.645-654, May 23-28, 2004
• 11: Haruo Hosoya , Benjamin C. Pierce, XDuce: A statically typed XML processing language, ACM Transactions on Internet Technology (TOIT), v.3 n.2, p.117-148, May 2003 [doi>10.1145/767193.767195]
• 12: Yao-Wen Huang , Fang Yu , Christian Hang , Chung-Hung Tsai , Der-Tsai Lee , Sy-Yen Kuo, Securing web application code by static analysis and runtime protection, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA [doi>10.1145/988672.988679]
• 13: D. A. Ladd and J. C. Ramming. Programming the Web: An application-oriented language for hypermedia service programming. In Proceedings of the 4th International World Wide Web Conference, 1995.
• 14: X. Leroy. The Objective Caml system release 3.08: Documentation and user's manual, 2004. http://caml.inria.fr/index-eng.html.
• 15: David Melski , Thomas Reps, Interconvertibility of a class of set constraints and context-free-language reachability, Theoretical Computer Science, v.248 n.1-2, p.29-98, October 2000 [doi>10.1016/S0304-3975(00)00049-9]
• 16: M. Mohri and M.-J. Nederhof. Regular approximation of context-free grammars through transformation. In Robustness in Language and Speech Technology, pages 153--163, 2001.
• 17: Mehryar Mohri , Richard Sproat, An efficient compiler for weighted rewrite rules, Proceedings of the 34th annual meeting on Association for Computational Linguistics, p.231-238, June 24-27, 1996, Santa Cruz, California [doi>10.3115/981863.981894]
• 18: Peter Ørbæk, Can you Trust your Data?, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.575-589, May 22-26, 1995
• 19: P. Ørbæk , J. Palsberg, Trust in the λ-calculus, Journal of Functional Programming, v.7 n.6, p.557-591, November 1997 [doi>10.1017/S0956796897002906]
• 20: L. Quinn. WDG HTML validator. http://www.htmlhelp.com/tools/validator/.
• 21: T. Reps. Program analysis via graph reachability. Information and Software Technology, 40(11--12):701--726, 2000.
• 22: B. K. Rosen , M. N. Wegman , F. K. Zadeck, Global value numbers and redundant computations, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-27, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73562]
• 23: N. Tabuchi, E. Sumii, and A. Yonezawa. Regular expression types for strings in a text processing language. In Proceedings of International Workshop on Types in Programming, ENTCS 75, 2002.
• 24: Peter Thiemann, Grammar-based analysis of string expressions, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.59-70, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040300]
• 25: The W3C markup validation service. http://validator.w3.org/.
• 26: Larry Wall , Mike Loukides, Programming Perl, O'Reilly & Associates, Inc., Sebastopol, CA, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Security, Verification

Keywords:
HTML validation, context-free grammars, cross-site scripting, server-side scripting, static analysis