Securing web application code by static analysis and runtime protection

ABSTRACT

Security remains a major roadblock to universal acceptance of the Web for many kinds of transactions, especially since the recent sharp increase in remotely exploitable vulnerabilities have been attributed to Web application bugs. Many verification tools are discovering previously unknown vulnerabilities in legacy C programs, raising hopes that the same success can be achieved with Web applications. In this paper, we describe a sound and holistic approach to ensuring Web application security. Viewing Web application vulnerabilities as a secure information flow problem, we created a lattice-based static analysis algorithm derived from type systems and typestate, and addressed its soundness. During the analysis, sections of code considered vulnerable are instrumented with runtime guards, thus securing Web applications in the absence of user intervention. With sufficient annotations, runtime overhead can be reduced to zero. We also created a tool named.WebSSARI (Web application Security by Static Analysis and Runtime Inspection) to test our algorithm, and used it to verify 230 open-source Web application projects on SourceForge.net, which were selected to represent projects of different maturity, popularity, and scale. 69 contained vulnerabilities. After notifying the developers, 38 acknowledged our findings and stated their plans to provide patches. Our statistics also show that static analysis reduced potential runtime overhead by 98.4%.

REFERENCES

• 1: F. E. Allen , J. Cocke, A program data flow analysis procedure, Communications of the ACM, v.19 n.3, p.137, March 1976 [doi>10.1145/360018.360025]
• 2: Gregory R. Andrews , Richard P. Reitman, An Axiomatic Approach to Information Flow in Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.56-76, Jan. 1980 [doi>10.1145/357084.357088]
• 3: Ken Ashcraft , Dawson Engler, Using Programmer-Written Compiler Extensions to Catch Security Holes, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.143, May 12-15, 2002
• 4: Larry Augustin , Dan Bressler , Guy Smith, Accelerating software development through collaboration, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581409]
• 5: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 6: Jean-Pierre Banâtre , Ciarán Bryce , Daniel Le Métayer, Compile-Time Detection of Information Flow in Sequential Programs, Proceedings of the Third European Symposium on Research in Computer Security, p.55-73, November 07-09, 1994
• 7: Anindya Banerjee , David A. Naumann, Secure Information Flow and Pointer Confinement in a Java-like Language, Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), p.253, June 24-26, 2002
• 8: Jeffrey M. Barth, A practical interprocedural data flow analysis algorithm, Communications of the ACM, v.21 n.9, p.724-736, Sept. 1978 [doi>10.1145/359588.359596]
• 9: Bell, D. E., La Padula, L. J. "Secure Computer System: Unified Exposition and Multics Interpretation." Tech Rep. ESD-TR-75--306, MITRE Corporation, 1976.
• 10: Biba, K. J. "Integrity Considerations for Secure Computer Systems." Technical Report ESD-TR-76-372, USAF Electronic Systems Division, Bedford, Massachusetts, Apr 1977.
• 11: Bishop, M., Dilger, M. "Checking for Race Conditions in File Accesses." Computing Systems, 9(2):131--152, Spring 1996.
• 12: Bobbitt, M. "Bulletproof Web Security." Network Security Magazine, TechTarget Storage Media, May 2002. http://infosecuritymag.techtarget.com/2002/may/bulletproof.shtml
• 13: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 14: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 15: Cowan, C., D. Maier, C. Pu, Walpole, J., Bakke, P., Beattie, S., Grier, A., Wagle, P., Zhang, Q., Hinton, H. "StackGuard: Automatic adaptive detection and prevention of buffer-overflow attacks." In Proc. 7th USENIX Security Conference (USENIX'98), pages 63--78, San Antonio, Texas, Jan 1998.
• 16: Crispin Cowan, Software Security for Open-Source Systems, IEEE Security and Privacy, v.1 n.1, p.38-45, January 2003 [doi>10.1109/MSECP.2003.1176994]
• 17: Curphey, M., Endler, D., Hau, W., Taylor, S., Smith, T., Russell, A., McKenna, G., Parke, R., McLaughlin, K., Tranter, N., Klien, A., Groves, D., By-Gad, I., Huseby, S., Eizner, M., McNamara, R. "A Guide to Building Secure Web Applications." The Open Web Application Security Project, v.1.1.1, Sep 2002.
• 18: Darvas, A., Hähnle, R., Sands, D. "A Theorem Proving Approach to Analysis of Secure Information Flow." In Proc. Workshop on Issues in the Theory of Security (WITS'03), Warsaw, Poland, Apr 5-6, 2003.
• 19: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 20: DeKok, A. "PScan: A Limited Problem Scanner for C Source Files." http://www.striker.ottawa.on.ca/ aland/pscan/
• 21: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 22: 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]
• 23: Franklin L. DeRemer, Simple LR(k) grammars, Communications of the ACM, v.14 n.7, p.453-460, July 1971 [doi>10.1145/362619.362625]
• 24: Dharmapurikar, S., Krishnamurthy, P., Sproull, T., and Lockwood, J. "Deep Packet Inspection Using Parallel Bloom Filters." In Proc. 11th Symp. High Performance Interconnects (HOTI'03), pages 44--51, Stanford, California, 2003.
• 25: Kyung Goo Doh , Seung Cheol Shin, Detection of information leak by data flow analysis, ACM SIGPLAN Notices, v.37 n.8, August 2002 [doi>10.1145/596992.597005]
• 26: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 27: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 28: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 29: Etienne M. Gagnon , Laurie J. Hendren, SableCC, an Object-Oriented Compiler Framework, Proceedings of the Technology of Object-Oriented Languages and Systems, p.140, August 03-07, 1998
• 30: Goguen, J. A., Meseguer, J. "Security Policies and Security Models." In Proc. IEEE Symp. Security and Privacy, pages 11--20, Oakland, California, Apr 1982.
• 31: Susan L. Graham , Mark Wegman, A Fast and Usually Linear Algorithm for Global Flow Analysis, Journal of the ACM (JACM), v.23 n.1, p.172-202, Jan. 1976 [doi>10.1145/321921.321939]
• 32: Guyer, S. Z., Berger, E. D., Lin, C. "Detecting Errors with Configurable Whole-program Dataflow Analysis." Technical Report, UTCS TR-02-04, University of Texas at Austin, 2002.
• 33: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 34: Matthew S. Hecht , Jeffrey D. Ullman, Analysis of a simple algorithm global data flow problems, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.207-217, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512946]
• 35: Fritz Henglein, Dynamic typing, Symposium proceedings on 4th European symposium on programming, p.233-253, January 1992, Rennes, France
• 36: Higgins, M., Ahmad, D., Arnold, C. L., Dunphy, B., Prosser, M., and Weafer, V., "Symantec Internet Security Threat Report-Attack Trends for Q3 and Q4 2002," Symantec, Feb 2003.
• 37: Gerard J. Holzmann, The logic of bugs, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587064]
• 38: Yao-Wen Huang , Shih-Kun Huang , Tsung-Po Lin , Chung-Hung Tsai, Web application security assessment by fault injection and behavior monitoring, Proceedings of the 12th international conference on World Wide Web, May 20-24, 2003, Budapest, Hungary [doi>10.1145/775152.775174]
• 39: Yao-Wen Huang , Fang Yu , Christian Hang , Chung-Hung Tsai , D. T. Lee , Sy-Yen Kuo, Verifying Web Applications Using Bounded Model Checking, Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN'04), p.199, June 28-July 01, 2004
• 40: Hughes, F. "PHP: Most Popular Server-Side Web Scripting Technology." LWN.net. http://lwn.net/Articles/1433/
• 41: Jensen, T., Le Metayer, D., Thorn, T. "Verification of Control Flow Based Security Properties." In Proc. 20th IEEE Symp. Security and Privacy, pages 89--103, IEEE Computer Society, New York, USA, 1999.
• 42: Rajeev Joshi , K. Rustan M. Leino, A semantic approach to secure information flow, Science of Computer Programming, v.37 n.1-3, p.113-138, May 2000 [doi>10.1016/S0167-6423(99)00024-6]
• 43: Kavado, Inc. "InterDo Version 3.0." Kavado Whitepaper, 2003.
• 44: Larochelle, D., Evans, D. "Statically Detecting Likely Buffer Overflow Vulnerabilities." In Proc. 10th USENIX Security Symposium (USENIX'01), Washington, D.C., Aug 2001.
• 45: Mandre, I. "PHP 4 Grammar for SableCC 3 Complete with Transformations." Indrek's SableCC Page, 2003. http://www.mare.ee/indrek/sablecc/
• 46: Meier, J. D., Mackman, A., Vasireddy, S. Dunner, M., Escamilla, R., Murukan, A. "Improving Web Application Security-Threats and Countermeasures." Microsoft Corporation, 2003.
• 47: Microsoft. "Visual C++ Compiler Options: /GS (Buffer Security Check)." MSDN Library, 2003. http://msdn.microsoft.com/library/default.asp?url=/library/en-us/vccore/html/vclrfGSBufferSecurity.asp
• 48: Mizuno, M., Schmidt, D. A. "A Security Flow Control Algorithm and Its Denotational Semantics Correctness Proof." Formal Aspects of Computing, 4(6A):727--754, 1992.
• 49: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 50: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 51: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 52: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 53: 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
• 54: OWASP. "The Ten Most Critical Web Application Security Vulnerabilities." OWASP Whitepaper, version 1.0, 2003.
• 55: Joon S. Park , Ravi Sandhu , Gail-Joon Ahn, Role-based access control on the web, ACM Transactions on Information and System Security (TISSEC), v.4 n.1, p.37-71, Feb. 2001 [doi>10.1145/383775.383777]
• 56: François Pottier , Vincent Simonet, Information flow inference for ML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.1, p.117-158, January 2003 [doi>10.1145/596980.596983]
• 57: Sabelfeld, A., Myers, A. C. "Language-Based Information-Flow Security." IEEE Journal on Selected Areas in Communications, 21(1):5--19, 2003.
• 58: Sanctum Inc. "AppShield 4.0 Whitepaper." 2002. http://www.sanctuminc.com
• 59: Sanctum Inc. "Web Application Security Testing-AppScan 3.5." http://www.sanctuminc.com
• 60: Ravi S. Sandhu, Lattice-Based Access Control Models, Computer, v.26 n.11, p.9-19, November 1993 [doi>10.1109/2.241422]
• 61: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 62: David Scott , Richard Sharp, Abstracting application-level web security, Proceedings of the 11th international conference on World Wide Web, May 07-11, 2002, Honolulu, Hawaii, USA [doi>10.1145/511446.511498]
• 63: David Scott , Richard Sharp, Developing Secure Web Applications, IEEE Internet Computing, v.6 n.6, p.38-45, November 2002 [doi>10.1109/MIC.2002.1067735]
• 64: Secure Software, Inc. "RATS-Rough Auditing Tool for Security." http://www.securesoftware.com/
• 65: Shankar, U., Talwar, K., Foster, J. S., Wagner, D. "Detecting Format String Vulnerabilities with Type Qualifiers." In Proc. 10th USENIX Security Symposium (USENIX'02), pages 201--220, Washington DC, Aug 2002.
• 66: SPI Dynamics. "Web Application Security Assessment." SPI Dynamics Whitepaper, 2003.
• 67: Stiennon, R., "Magic Quadrant for Enterprise Firewalls, 1H03." Research Note. M-20-0110, Gartner, Inc., 2003.
• 68: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 69: J. Viega , J. T. Bloch , Y. Kohno , G. McGraw, ITS4: A static vulnerability scanner for C and C++ code, Proceedings of the 16th Annual Computer Security Applications Conference, p.257, December 11-15, 2000
• 70: Dennis Volpano , Cynthia Irvine , Geoffrey Smith, A sound type system for secure flow analysis, Journal of Computer Security, v.4 n.2-3, p.167-187, Jan. 1996
• 71: Wagner, D., Foster, J. S., Brewer, E. A., Aiken, A. "A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities." In Proc. 7th Network and Distributed System Security Symposium (NDSS2000), pages 3--17, San Diego, California, Feb 2000.
• 72: Larry Wall , Mike Loukides, Programming Perl, O'Reilly & Associates, Inc., Sebastopol, CA, 2000
• 73: David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325728]
• 74: Watts, G. "PHPXref: PHP Cross Referencing Documentation Generator." Sep 2003. http://phpxref.sourceforge.net/
• 75: Wheeler, D. A. "FlawFinder." http://www.dwheeler.com/flawfinder/
• 76: Brian Witten , Carl Landwehr , Michael Caloyannides, Does Open Source Improve System Security?, IEEE Software, v.18 n.5, p.57-61, September 2001 [doi>10.1109/52.951496]
• 77: Andrew K. Wright , Robert Cartwright, A practical soft type system for scheme, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.87-152, Jan. 1997 [doi>10.1145/239912.239917]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Class invariants

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Information flow controls

  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.2 Social Issues
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Unauthorized access (e.g., hacking, phreaking); Invasive software (e.g., viruses, worms, Trojan horses)

General Terms:
Security, Verification

Keywords:
information flow, noninterference, program security, security vulnerabilities, type systems, verification, web application security