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 are relatively complex 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 rather than individually. This offers two distinct benefits. First, together with the counterexamples themselves, they allow for more descriptive and precise error reports. Second, it allows for automated patching at locations where errors are initially introduced rather than at locations where the propagated errors cause problems. Results from a TS-BMC comparison test using 230 open-source Web applications showed a 41.0% decrease in runtime instrumentations when BMC was used. In the 38 vulnerable projects identified by TS, BMC classified the TS-reported 980 individual errors into 578 groups, with each group requiring a minimal set of patches for repair.

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%.