CS395T Unified Approach to Verification and Validation Project Proposal:Combining Static Analysis and Runtime Monitoring for SQL-injection Attacks inExecutable Model-based Software DevelopmentDongjin [email protected]. Problem DescriptionDatabase-driven web applications have becomewidely deployed on the Internet. Theseapplications, and their underlying databases,often contain confidential, or even sensitive,information, such as customer and financialrecords. In recent years there has been anincrease in attacks against these onlinedatabases. One type of attacks, SQL-InjectionAttacks (SQLIAs), has been described as one ofthe most serious treats for Web applications,which are vulnerable to SQL injection mayallow an attacker to achieve complete accessright to their databases by submitting SQLcommands directly to them. With that, theattacker possesses the power to leak, modify,and even remove information that is stored onthem. The cause of SQL injection vulnerabilities isinsufficient verification and validation of userinput. Thus, this project provides the hybridverification framework combining staticanalysis and run-time monitoring schemes. Thiswork illustrates the incorporation of verificationprocess into a design methodology for a systemdevelopment. 2. Approach and ResultI introduce a hybrid verification framework in amodel-based development for the detection andprevention of SQLIAs. Model-baseddevelopment has focused on verification andtesting for functional or timing aspects, but anyweb-related applications using databaseconnection also contain resource and security-related properties.This work focuses on how to integrate theverification of Security and Resource(S/R)properties in to the software development cycleof executable model-based approaches.As explained, this methodology includes:xUML (eXecutable Unified ModelingLanguage) modeling and simulation-based model testing supported by theObjectbenchAutomatic code generation fromxUML models by CodeGenesis codegeneratorFormal functional verification byObjectCheck model checking forxUML modelS/R bound checking based on efficientdynamic monitoring Rescheck, S/R verifier, deals with S/Rproperties to provide the comprehensiveautonomous support for S/R safety verification.In static phase of Rescheck, the techniqueleverages an existing, conservative stringanalysis to analyze the web-application. In thedynamic phase of Rescheck, this monitors alldynamically-generated queries at runtime andchecks them for compliance with the statically-generated state model in Control Follow Graph(CFG). I illustrate one case study; security verificationto counter SQL-injection attacks in webapplications, which will represent profits byinserting verification procedure into systemdesign and merging static analysis and runtimemonitoring. The case study about embeddedsystem is optional.3. Milestone(Sep. 23 ~ Sep. 30): I research aboutexisting hybrid model-based developmentapproach and study related works. (Oct. 1~ Oct. 31): I apply this approach toSQL injection security model.(Nov. 1 ~ Nov. 20): I plan to experimentand finalize this work.Reference[1] J i a n l i a n g Yi ,H o n g u k Wo o , J a m e s C . Br o w n e ,A l o y s i u s K . M o k , F e i X i e , E l l a A t k i n s , C h a n - G u nL e e. Incorporating Resource Safety Verification toExecutable Model-based Development forEmbedded Systems RTAS, pp. 137-146, 2008 IEEE Real-Time andEmbedded Technology and ApplicationsSymposium, 2008[2] William G. J. Halfond ,Alessandro Orso. Combining static analysis and runtime monitoring to counter SQL-injection attacks. In Proceeding of the Third International ICSE Workshop on Dynamic Analysis (WODA 2005), St. Louis, MO, USA. May 2005.[3] Weijiang Yu, Aloysius K. Mok. TINMAN: AResource Bound Security Checking System forMobile Code, Proceedings of the 7th EuropeanSymposium on Research in Computer Security,p.178-193, October 14-16,
View Full Document