nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Jaint: A Framework for User-Defined Dynamic Taint-Analyses Based on Dynamic Symbolic Execution of Java Programs

verfasst von : Malte Mues, Till Schallau, Falk Howar

Erschienen in: Integrated Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We present Jaint, a generic security analysis for Java Web-applications that combines concolic execution and dynamic taint analysis in a modular way. Jaint executes user-defined taint analyses that are formally specified in a domain-specific language for expressing taint-flow analyses. We demonstrate how dynamic taint analysis can be integrated into JDart, a dynamic symbolic execution engine for the Java virtual machine in Java PathFinder. The integration of the two methods is modular in the sense that it traces taint independently of symbolic annotations. Therefore, Jaint is capable of sanitizing taint information (if specified by a taint analysis) and using multi-colored taint for running multiple taint analyses in parallel. We design a domain-specific language that enables users to define specific taint-based security analyses for Java Web-applications. Specifications in this domain-specific language serve as a basis for the automated generation of corresponding taint injectors, sanitization points and taint-flow monitors that implement taint analyses in Jaint. We demonstrate the generality and effectiveness of the approach by analyzing the OWASP benchmark set, using generated taint analyses for all 11 classes of CVEs in the benchmark set.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Towards Generating SPARK from Event-B Models

Nächstes Kapitel Automatic Generation of Guard-Stable Floating-Point Code

Allen, J.: Perl version 5.8.8 documentation - perlsec (May 2016). http://perldoc.perl.org/5.8.8/perlsec.pdf

Baldoni, R., Coppa, E., D’elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. (CSUR) 51(3), 50 (2018)CrossRef

Bekrar, S., Bekrar, C., Groz, R., Mounier, L.: A taint based approach for smart fuzzing. In: 2012 IEEE 5th International Conference on Software Testing, Verification and Validation, pp. 818–825. IEEE (2012)

Burato, E., Ferrara, P., Spoto, F.: Security analysis of the OWASP benchmark with Julia. In: 2017 Proceedings of ITASEC (2017)

Cadar, C., Dunbar, D., Engler, D.R., et al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, vol. 8, pp. 209–224 (2008)

Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82–90 (2013). https://doi.org/10.1145/2408776.2408795CrossRef

Cheng, W., Zhao, Q., Yu, B., Hiroshige, S.: TaintTrace: efficient flow tracing with dynamic binary rewriting. In: 11th IEEE Symposium on Computers and Communications, ISCC 2006, pp. 749–754. IEEE (2006)

Clause, J., Li, W., Orso, A.: Dytan: a generic dynamic taint analysis framework. In: Proceedings of the 2007 International Symposium on Software Testing and Analysis, pp. 196–206. ACM (2007)

Conti, J.J., Russo, A.: A taint mode for Python via a library. In: Aura, T., Järvinen, K., Nyberg, K. (eds.) NordSec 2010. LNCS, vol. 7127, pp. 210–222. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27937-9_15CrossRef

10.

Corin, R., Manzano, F.A.: Taint analysis of security code in the KLEE symbolic execution engine. In: Chim, T.W., Yuen, T.H. (eds.) ICICS 2012. LNCS, vol. 7618, pp. 264–275. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34129-8_23CrossRef

11.

Edalat, E., Sadeghiyan, B., Ghassemi, F.: ConsiDroid: A concolic-based tool for detecting SQL injection vulnerability in android apps. CoRR, abs/1811.10448, arXiv arXiv:1811.10448 (2018)

12.

Haldar, V., Chandra, D., Franz, M.: Dynamic taint propagation for Java. In: 21st Annual Computer Security Applications Conference, ACSAC 2005, p. 9. IEEE (2005)

13.

Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366–381 (2000)CrossRef

14.

Jee, K., Portokalidis, G., Kemerlis, V.P., Ghosh, S., August, D.I., Keromytis, A.D.: A general approach for efficiently accelerating software-based dynamic data flow tracking on commodity hardware. In: NDSS (2012)

15.

Kang, M.G., McCamant, S., Poosankam, P., Song, D.: DTA++: dynamic taint analysis with targeted control-flow propagation. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 2011, San Diego, California, USA, 6–9 February 2011 (2011). http://www.isoc.org/isoc/conferences/ndss/11/pdf/5_4.pdf

16.

Lam, L.C., Chiueh, T.: A general dynamic information flow tracking framework for security applications. In: 2006 22nd Annual Computer Security Applications Conference, ACSAC 2006, pp. 463–472. IEEE (2006)

17.

Livshits, V.B., Lam, M.S.: Finding security vulnerabilities in Java applications with static analysis. In: USENIX Security Symposium, vol. 14, p. 18 (2005)

18.

Luckow, K., et al.: JDart: a dynamic symbolic analysis framework. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 442–459. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_26CrossRef

19.

Mues, M., Howar, F.: JDart: dynamic symbolic execution for Java bytecode (competition contribution). In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12079, pp. 398–402. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_28CrossRef

20.

Mues, M., Schallau, T., Howar, F.: Artifact for ‘Jaint: A Framework for User-Defined Dynamic Taint-Analyses based on Dynamic Symbolic Execution of Java Programs’, September 2020. https://doi.org/10.5281/zenodo.4060244

21.

Newsome, J., Song, D.X.: Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software. In: NDSS, vol. 5, pp. 3–4. Citeseer (2005)

22.

Nguyen-Tuong, A., Guarnieri, S., Greene, D., Shirley, J., Evans, D.: Automatically hardening web applications using precise tainting. In: Sasaki, R., Qing, S., Okamoto, E., Yoshiura, H. (eds.) SEC 2005. IAICT, vol. 181, pp. 295–307. Springer, Boston, MA (2005). https://doi.org/10.1007/0-387-25660-1_20CrossRef

23.

Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)CrossRef

24.

Schoepe, D., Balliu, M., Pierce, B.C., Sabelfeld, A.: Explicit secrecy: a policy for taint tracking. In: 2016 IEEE European Symposium on Security and Privacy (EuroS&P), pp. 15–30. IEEE (2016)

25.

Schwartz, E.J., Avgerinos, T., Brumley, D.: All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In: 2010 IEEE Symposium on Security and Privacy, pp. 317–331. IEEE (2010)

26.

Song, D., et al.: BitBlaze: a new approach to computer security via binary analysis. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 1–25. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89862-7_1CrossRef

27.

Spoto, F.: The Julia static analyzer for Java. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 39–57. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_3CrossRef

28.

Xu, W., Bhatkar, S., Sekar, R.: Taint-enhanced policy enforcement: a practical approach to defeat a wide range of attacks. In: USENIX Security Symposium, pp. 121–136 (2006)

Titel: Jaint: A Framework for User-Defined Dynamic Taint-Analyses Based on Dynamic Symbolic Execution of Java Programs
verfasst von: Malte Mues
Till Schallau
Falk Howar
Verlag: Springer International Publishing
Buch: Integrated Formal Methods
Print ISBN: 978-3-030-63460-5

Electronic ISBN: 978-3-030-63461-2

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-63461-2_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner