US Patent:
20120151592, Jun 14, 2012
Inventors:
Margus Veanes - Bellevue WA, US
Pieter Hooimeijer - Charlottesville VA, US
Benjamin Livshits - Kirkland WA, US
Prateek Saxena - Berkeley CA, US
David Molnar - Berkeley CA, US
Assignee:
MICROSOFT CORPORATION - Redmond WA
International Classification:
G06F 11/00
Abstract:
There is provided a computer-implemented method for analyzing string-manipulating programs. An exemplary method comprises describing a string-manipulating program as a finite state transducer. The finite state transducer may be evaluated with a constraint solving methodology to determine whether a particular string may be provided as output by the string-manipulating program. The constraint solving methodology may involve the use of one or more satisfiability modulo theories (SMT) solvers. A determination may be made regarding whether the string-manipulating program may contain a potential security risk depending on whether the particular string may be provided as output by the string-manipulating program.