Path- and Index-sensitive String Analysis based on Monadic Second-order Logic

We propose a novel technique for statically verifying the strings generated by a program.
The verification is conducted by encoding the program in Monadic
Second-Order Logic (M2L). We use M2L to describe constraints among program variables
and to abstract built-in string operations.
Once we encode a program in M2L, a theorem prover for M2L, such as MONA,
can automatically check if a string generated by the program satisfies
a given specification, and if not, exhibit a counterexample.
With this approach, we can naturally encode relationships among strings,
accounting also for cases in which a program manipulates strings using indices.
In addition, our string analysis is path sensitive in that
it accounts for the effects of string and Boolean comparisons, as well as regular-expression matches.

We have implemented our string-analysis algorithm, and used it to augment an
industrial security analysis for Web applications by automatically detecting and
verifying sanitizers---methods that eliminate malicious
patterns from untrusted strings, making those strings safe to use in security-sensitive operations.
On the 8 benchmarks we analyzed, our string analyzer discovered 128 previously
unknown sanitizers, compared to 71 sanitizers detected by a previously presented
string analysis.

By: Takaaki Tateishi, Marco Pistoia, Omer Tripp

Published in: RT0930 in 2011


This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.


Questions about this service can be mailed to .