Sage Journals: Discover world-class research

Abstract

We propose a formal and automated approach that allows one to (i) reason about vulnerabilities of web applications and (ii) combine multiple vulnerabilities for the identification of complex, multi-stage attacks. We have developed WAFEx, an automatic tool that implements our approach and we show its efficiency by applying it to real-world case studies. WAFEx was able to generate, and exploit, previously unknown attacks.

Keywords

Security testing vulnerability assessment penetration testing model checking web applications formal methods SQL injection cross-site scripting cross-site request forgery file-system related vulnerabilities

Get full access to this article

View all access options for this article.

References

Akhawe,

Barth,

P.E.

Lam,

Mitchell and

Song, Towards a formal foundation of web security, in: 23rd IEEE Computer Security Foundations Symposium (CSF), IEEE, 2010, pp. 290–304. doi:10.1109/CSF.2010.27.

Alhuzali,

Gjomemo,

Eshete and

V.N.

Venkatakrishnan, NAVEX: Precise and scalable exploit generation for dynamic web applications, in: 27th USENIX Security Symposium, USENIX Association, 2018, pp. 377–392. doi:10.5555/3277203.3277232.

Arachni – Web application security scanner framework, http://www.arachni-scanner.com/.

Armando,

Arsac,

Avanesov,

Barletta,

Calvi,

Cappai,

Carbone,

Chevalier,

Compagna,

Cuéllar,

Erzse,

Frau,

Minea,

Mödersheim,

von Oheimb,

Pellegrino,

Ponta,

Rocchetto,

Rusinowitch,

Torabi Dashti,

Turuani and

Viganò, The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures, in: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, Vol. 7214, Springer, 2012, pp. 267–282. doi:10.1007/978-3-642-28756-5_19.

Armando,

Carbone,

Compagna,

Li and

Pellegrino, Model-checking driven security testing of web-based applications, in: 3rd International Conference on Software Testing, Verification and Validation (ICST), IEEE, 2010, pp. 361–370. doi:10.1109/ICSTW.2010.54.

Armando,

Pellegrino,

Carbone,

Merlo and

Balzarotti, From model-checking to automated testing of security protocols: Bridging the gap, in: 6th International Conference on Tests and Proofs (TAP), LNCS, Vol. 7305, Springer, 2012, pp. 3–18. doi:10.1007/978-3-642-30473-6_3.

ASP documentation: Including files in ASP applications, Microsoft, https://msdn.microsoft.com/en-us/library/ms524876(v=vs.90).aspx.

AVANTSSAR, Deliverable 2.3 (update): ASLan++ specification and tutorial, 2011, http://www.avantssar.eu.

Backes,

Rieck,

Skoruppa,

Stock and

Yamaguchi, Efficient and flexible discovery of PHP application vulnerabilities, in: IEEE European Symposium on Security and Privacy (EuroS&P), IEEE, 2017, pp. 334–349. doi:10.1109/EuroSP.2017.14.

10.

Bishop, About penetration testing, IEEE Security & Privacy 5(6) (2007), 84–87. doi:10.1109/MSP.2007.159.

11.

Büchler,

Oudinet and

Pretschner, Semi-automatic security testing of web applications from a secure model, in: IEEE Sixth International Conference on Software Security and Reliability (SERE), IEEE, 2012, pp. 253–262. doi:10.1109/SERE.2012.38.

12.

Calvi and

Viganò, An automated approach for testing the security of web applications against chained attacks, in: 31st ACM/SIGAPP Symposium on Applied Computing (SAC), ACM Press, 2016. doi:10.1145/2851613.2851803.

13.

Carey, Penetration testing vs. vulnerability scanning – What’s the difference?, https://www.alienvault.com/blogs/security-essentials/penetration-testing-vs-vulnerability-scanning-whats-the-difference.

14.

Christey, The 2019 CWE/SANS top 25 most dangerous programming errors, http://cwe.mitre.org/top25.

15.

Damele and

Guimarães, Advanced SQL injection to operating system full control, in: BlackHat EU, 2009.

16.

De Meo,

Rocchetto and

Viganò, Formal analysis of vulnerabilities of web applications based on SQL injection, in: International Workshop on Security and Trust Management (STM), LNCS, Vol. 9871, Springer, 2016, pp. 179–195. doi:10.1007/978-3-319-46598-2_13.

17.

De Meo and

Viganò, A formal approach to exploiting multi-stage attacks based on file-system vulnerabilities of web applications, in: 9th International Symposium on Engineering Secure Software and Systems (ESSoS), LNCS, Vol. 10379, Springer, 2017, pp. 196–212. doi:10.1007/978-3-319-62105-0_13.

18.

Dolev and

A.C.

Yao, On the security of public key protocols, IEEE Transactions on Information Theory 29(2) (1983), 198–208. doi:10.1109/TIT.1983.1056650.

19.

DotDotPwn – The directory traversal fuzzer, https://github.com/wireghoul/dotdotpwn.

20.

Doupé,

Cova and

Vigna, Why Johnny can’t pentest: An analysis of black-box web vulnerability scanners, in: International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment (DIMVA), LNCS, Vol. 6201, Springer, 2010, pp. 111–131. doi:10.1007/978-3-642-14215-4_7.

21.

DVWA: Damn vulnerable web application, RandomStorm, http://www.dvwa.co.uk/.

22.

Felderer,

Büchler,

Johns,

A.D.

Brucker,

Breu and

Pretschner, Security testing: A survey, Advances in Computers 101 (2016), 1–51. doi:10.1016/bs.adcom.2015.11.003.

23.

Felderer,

Zech,

Breu,

Büchler and

Pretschner, Model-based security testing: A taxonomy and systematic classification, Software Testing, Verification and Reliability 26 (2015), 119–148. doi:10.1002/stvr.1580.

24.

Glynn, Vulnerability assessment and penetration testing, http://www.veracode.com/security/vulnerability-assessment-and-penetration-testing.

25.

Google Gruyere app engine, Google, https://google-gruyere.appspot.com/.

26.

W.G.J.

Halfond,

Viegas and

Orso, A classification of SQL-injection attacks and countermeasures, in: IEEE International Symposium on Secure Software Engineering (ISSSE), 2006.

27.

Jackson, Software Abstractions: Logic, Language, and Analysis, MIT Press, 2012.

28.

Joomla!, https://www.joomla.org.

29.

MBST classification, https://qe-informatik.uibk.ac.at/mbst-classification/.

30.

P.F.

Mihancea and

Minea, JMODEX: Model extraction for verifying security properties of web applications, in: IEEE Conference on Software Maintenance, Reengineering, and Reverse Engineering (CSMR-WCRE), 2014, pp. 450–453. doi:10.1109/CSMR-WCRE.2014.6747216.

31.

OWASP, Top 10 for 2013, https://www.owasp.org/index.php/Category:OWASP_Top_Ten_Project.

32.

OWASP, Zed Attack Proxy (ZAP), https://www.owasp.org/index.php/OWASP_Zed_Attack_Proxy_Project.

33.

OWASP WebGoat project, OWASP, https://www.owasp.org/index.php/Category:OWASP_WebGoat_Project.

34.

Pellegrino,

Johns,

Koch,

Backes and

Rossow, Deemon: Detecting CSRF with dynamic analysis and property graphs, in: ACM SIGSAC Conference on Computer and Communications Security (CCS), ACM, 2017, pp. 1757–1771. doi:10.1145/3133956.3133959.

35.

PHP documentation: Include, http://php.net/manual/it/function.include.php.

36.

Postswigger, Burp Proxy, 2014, https://portswigger.net/burp/proxy.html.

37.

Rocchetto,

Ochoa and

Torabi Dashti, Model-based detection of CSRF, in: ICT Systems Security and Privacy Protection, IFIP AICT, Vol. 428, Springer, 2014, pp. 30–43. doi:10.1007/978-3-642-55415-5_3.

38.

Rocchetto,

Viganò and

Volpe, An interpolation-based method for the verification of security protocols, Journal of Computer Security 25(6) (2017), 463–510. doi:10.3233/JCS-16832.

39.

SANS Institute, Penetration testing: Assessing your overall security before attackers do, https://www.sans.org/reading-room/whitepapers/analyst/penetration-testing-assessing-security-attackers-34635.

40.

sqlmap: Automatic SQL injection and database takeover tool, 2013, http://sqlmap.org.

41.

sqlninja: A SQL Server injection and takeover tool, sqlninja, http://sqlninja.sourceforge.net/.

42.

The Java EE 5 tutorial: Reusing content in JSP pages, Oracle, http://docs.oracle.com/javaee/5/tutorial/doc/bnajb.html.

43.

Trustwave SpiderLabs, Joomla SQL injection vulnerability exploit results in full administrative access, 2015, https://www.trustwave.com/Resources/SpiderLabs-Blog/Joomla-SQL-Injection-Vulnerability-Exploit-Results-in-Full-Administrative-Access.

44.

Turuani, The CL-AtSe protocol analyser, in: International Conference on Rewriting Techniques and Applications (RTA), LNCS, Vol 4098, Springer, 2006, pp. 277–286. doi:10.1007/11805618_21.

45.

Utting,

Pretschner and

Legeard, A taxonomy of model-based testing approaches, Software Testing, Verification and Reliability 22(5) (2012), 297–312. doi:10.1002/stvr.456.

46.

Vibhandik and

A.K.

Bose, Vulnerability assessment of web applications – A testing approach, in: 2015 Forth International Conference on E-Technologies and Networks for Development (ICeND), IEEE, 2015, pp. 1–6. doi:10.1109/ICeND.2015.7328531.

47.

Viganò, The SPaCIoS project: Secure provision and consumption in the Internet of Services, in: Sixth IEEE International Conference on Software Testing, Verification and Validation (ICST), IEEE CS Press, 2013, pp. 497–498. doi:10.1109/ICST.2013.75.

48.

von Oheimb and

Mödersheim, ASLan++ – A formal security specification language for distributed systems, in: Formal Methods for Components and Objects (FMCO), LNCS, Vol. 6957, Springer, 2010, pp. 1–22. doi:10.1007/978-3-642-25271-6_1.

49.

Web Application Formal Exploiter (WAFEx), https://github.com/rhaidiz/wafex.

50.

Web Application Formal Exploiter (WAFEx) model creator, https://github.com/rhaidiz/wafex-model-creator.

51.

Wfuzz: The web bruteforcer, edge-security, https://github.com/xmendez/wfuzz.

52.

XSS-Proxy, http://xss-proxy.sourceforge.net/.

A formal and automated approach to exploiting multi-stage attacks of web applications

Abstract

Keywords

Get full access to this article

References