TU Darmstadt / ULB / TUbiblio

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

Arzt, Steven and Rasthofer, Siegfried and Hahn, Robert and Bodden, Eric (2015):
Using Targeted Symbolic Execution for Reducing False-Positives in Dataflow Analysis.
In: Proceedings of the 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis, In: 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis, Portland, USA, 14.06.2015, [Conference or Workshop Item]

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.

Item Type: Conference or Workshop Item
Erschienen: 2015
Creators: Arzt, Steven and Rasthofer, Siegfried and Hahn, Robert and Bodden, Eric
Title: Using Targeted Symbolic Execution for Reducing False-Positives in Dataflow Analysis
Language: English
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.

Title of Book: Proceedings of the 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis
Divisions: LOEWE > LOEWE-Zentren > CASED – Center for Advanced Security Research Darmstadt
20 Department of Computer Science > EC SPRIDE > Secure Software Engineering
20 Department of Computer Science > EC SPRIDE
Zentrale Einrichtungen
LOEWE
20 Department of Computer Science
LOEWE > LOEWE-Zentren
Event Title: 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis
Event Location: Portland, USA
Event Dates: 14.06.2015
Date Deposited: 06 Aug 2015 08:36
Export:

Optionen (nur für Redakteure)

View Item View Item