TU Darmstadt / ULB / TUbiblio

Using Targeted Symbolic Execution for Reducing False-Positives in Dataflow Analysis

Arzt, Steven ; Rasthofer, Siegfried ; Hahn, Robert ; Bodden, Eric (2015)
Using Targeted Symbolic Execution for Reducing False-Positives in Dataflow Analysis.
4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis. Portland, USA (14.06.2015)
Konferenzveröffentlichung, Bibliographie

Kurzbeschreibung (Abstract)

Static data flow analysis is an indispensable tool for finding potentially malicious data leaks in software programs. Programs, nowadays often consisting of millions of lines of code, have grown much too large to allow for a complete manual inspection. Nevertheless, security experts need to judge whether an application is trustworthy or not, developers need to find bugs, and quality experts need to assess the maturity of software products. Thus, analysts take advantage of automated data flow analysis tools to find candidates for suspicious leaks which are then further investigated.

While much progress has been made in the area with a broad variety of static data flow analysis tools proposed in academia and being offered commercially, the number of false alarms raised by these tools is still a concern. Many of the false alarms are reported because the analysis tool detects data flows along paths which are not realizable at runtime, e.g., due to contradictory conditions on the path. Still, every single report is a potential issue and must be reviewed by an expert which is labor-intensive and costly. In this work, we therefore propose TASMAN, a post-analysis based on symbolic execution that removes such false data leaks along unrealizable paths from the result set. Thus, it greatly improves the usefulness of the result presented to the human analyst.

In our experiments on DroidBench examples, TASMAN reduces the number of false positives by about 80% without pruning any true positives. Additionally, TASMAN also identified false positives in real-world examples which we confirmed by hand. With an average execution time of 5.4 seconds per alleged leak to be checked on large real-world applications, TASMAN is fast enough for practical use.

Typ des Eintrags: Konferenzveröffentlichung
Erschienen: 2015
Autor(en): Arzt, Steven ; Rasthofer, Siegfried ; Hahn, Robert ; Bodden, Eric
Art des Eintrags: Bibliographie
Titel: Using Targeted Symbolic Execution for Reducing False-Positives in Dataflow Analysis
Sprache: Englisch
Publikationsjahr: 14 Juni 2015
Buchtitel: Proceedings of the 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis
Veranstaltungstitel: 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis
Veranstaltungsort: Portland, USA
Veranstaltungsdatum: 14.06.2015
Kurzbeschreibung (Abstract):

Static data flow analysis is an indispensable tool for finding potentially malicious data leaks in software programs. Programs, nowadays often consisting of millions of lines of code, have grown much too large to allow for a complete manual inspection. Nevertheless, security experts need to judge whether an application is trustworthy or not, developers need to find bugs, and quality experts need to assess the maturity of software products. Thus, analysts take advantage of automated data flow analysis tools to find candidates for suspicious leaks which are then further investigated.

While much progress has been made in the area with a broad variety of static data flow analysis tools proposed in academia and being offered commercially, the number of false alarms raised by these tools is still a concern. Many of the false alarms are reported because the analysis tool detects data flows along paths which are not realizable at runtime, e.g., due to contradictory conditions on the path. Still, every single report is a potential issue and must be reviewed by an expert which is labor-intensive and costly. In this work, we therefore propose TASMAN, a post-analysis based on symbolic execution that removes such false data leaks along unrealizable paths from the result set. Thus, it greatly improves the usefulness of the result presented to the human analyst.

In our experiments on DroidBench examples, TASMAN reduces the number of false positives by about 80% without pruning any true positives. Additionally, TASMAN also identified false positives in real-world examples which we confirmed by hand. With an average execution time of 5.4 seconds per alleged leak to be checked on large real-world applications, TASMAN is fast enough for practical use.

Fachbereich(e)/-gebiet(e): LOEWE > LOEWE-Zentren > CASED – Center for Advanced Security Research Darmstadt
20 Fachbereich Informatik > EC SPRIDE > Secure Software Engineering
20 Fachbereich Informatik > EC SPRIDE
Zentrale Einrichtungen
LOEWE
20 Fachbereich Informatik
LOEWE > LOEWE-Zentren
Hinterlegungsdatum: 06 Aug 2015 08:36
Letzte Änderung: 06 Aug 2015 08:36
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen