Abstract: We present a taint analysis that can automatically detect
when string operations result in a string that is free of taints, where
all the tainted patterns have been removed. This is an improvement
on the conservative behavior of previous taint analyzers, where a
string operation on a tainted string always leads to a tainted string
unless the operation is manually marked as a sanitizer. The taint
analysis is built on top of a string analysis that uses finite state
automata to approximate the sets of values that string variables can
take during the execution of a program. The proposed approach has
been implemented as an extension of FlowDroid and experimental
results show that the resulting taint analyzer is much more precise
than the original FlowDroid.
Abstract: We design and implement a precise model of string
operations using finite state machine transformers and state
transformers to approximate the values string variables can take
throughout the execution of the program.We use our model to analyze
Android program string variables. Our experimental results show that
our string analysis is very efficient at detecting the contextual effect
of string operations on the string variables. Our model proved to be
very useful when it came to verifying statements about the string
variables of the program.