Verifying Web Applications Using Bounded Model Checking

The authors describe the use of bounded model checking (BMC) for verifying Web application code. Vulnerable sections of code are patched automatically with runtime guards, allowing both verification and assurance to occur without user intervention. Model checking techniques have relatively complexity compared to the typestate-based polynomial-time algorithm (TS) we adopted in an earlier paper, but they offer three benefits--they provide counterexamples, more precise models, and sound and complete verification. Compared to conventional model checking techniques, BMC offers a more practical approach to verifying programs containing large numbers of variables, but requires fixed program diameters to be complete. Formalizing Web application vulnerabilities as a secure information flow problem with fixed diameter allows for BMC application without drawback. Using BMC-produced counterexamples, errors that result from propagations of the same initial error can be reported as a single group r...

• Type: Conference
• Year: 2004
• Where: DSN
• Authors: Yao-Wen Huang, Fang Yu, Christian Hang, Chung-Hung Tsai, D. T. Lee, Sy-Yen Kuo
• Keywords: Computer Networks, DSN 2004, Model Checking, Model Checking Techniques, Web Application