7July_14_2008 Verifying Web Applications Using Bounded Model Checking
http://doi.ieeecomputersociety.org/10.1109/DSN.2004.1311890
BMC-bounded model checking for verifying WEb app code.
vulnerable parts of code patched automatically w/ runtime guards (verification + assurance)
MC techniques relatively complex compared to typestate-based polynomial time alg(TS)
3 benefits
   counterexamples
   more precise models
   sound and complete verificaiton
conventional MC vs. BMC
   BMC more practical approach for prog. w/ many vars
   BMC requires fixed prog. diameters for completeness
BMC-produced counter-ex's can be grouped
2 benefits
  more descriptive and precise error reports
  automated patching at initial point of error

stats: 230 opensource WEb app 41% decrease in runtime instrumentations
38 vuln. by TS, BMC classifed 980 indiv. errors, 578 groups, requiring minimal patch

INTRO
B2B, B2C, healthcare, e-gov, need security

one approach is applying strategies to existing web apps (enhance w/ fault tolerance)
gateways to filter malicious and erroneous input
-> these 2 offer immediate assurance drawback blind protection w/o looking at why the problem

merzbacher and patterson[18] web app assessment based on user-experience modeling
Huang, et al security assessment framework user behaviour simulation w/ user-experience modeling
2 disadvantages
  not provide immediate quality assurance
  cannot guarantee ide of all flaws

thus use formal verification techniques

combo static and runtime techniques
WebSSARI (Web app Security via Static Analysis and Runtime Inspection)
  -statically verify existing apps
  -protect possibly defective code after verification

based verification (TS) on Strom and Yemini's "Typestate: A programming language concept for enhancing software reliability"
formal verification for reliability and security (similar or identical sets of program chars)
Strom and Yemini's detect at compile time legal syntax but semantically undefined sequences (these could lead to unpredictable behaviour)
  e.g. -reading vars before initialized
        -dereferencing pointers after their dynamic obj are deallocated
security:
  protect confidentiality, integrity, availability
  null points -> denial of service attacks

BMC precise compile-time estimation of runtime state
WebSSARI inserts runtime guards into sections of code w/ potential security risk
points out safety policy violations
....