Susmit Kumar Jha and Sanjit A. Seshia and Rhishikesh Shrikant Limaye

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2009-41

March 16, 2009

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-41.pdf

Satisfiability solvers are increasingly playing a key role in software verification, with particularly effective use in the analysis of security vulnerabilities. String processing is a key part of many software applications, such as browsers and web servers. These applications are susceptible to attacks through malicious data received over network. Automated tools for analyzing the security of such applications, thus need to reason about strings. For efficiency reasons, it is desirable to have a solver that treats strings as first-class types. In this paper, we present some theories of strings that are useful in a software security context and analyze the computational complexity of the presented theories. We use this complexity analysis to motivate a byte-blast approach which employs a Boolean encoding of the string constraints to a corresponding Boolean satisfiability problem.

---

BibTeX citation:

@techreport{Jha:EECS-2009-41,
    Author= {Jha, Susmit Kumar and Seshia, Sanjit A. and Limaye, Rhishikesh Shrikant},
    Title= {On the Computational Complexity of Satisfiability Solving for String Theories},
    Year= {2009},
    Month= {Mar},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-41.html},
    Number= {UCB/EECS-2009-41},
    Abstract= {Satisfiability solvers are increasingly playing a key role in software verification, with particularly effective use in the analysis of security vulnerabilities. String processing is a key part of many software applications, such as browsers and web servers. These applications are susceptible to attacks through malicious data received over network. Automated tools for analyzing the security of such applications, thus need to reason about strings. For efficiency reasons, it is desirable to have a solver that treats strings as first-class types. In this paper, we present some theories of strings that are useful in a software security context and analyze the computational complexity of the presented theories. We use this complexity analysis to motivate a byte-blast approach which employs a Boolean encoding of the string constraints to a corresponding Boolean satisfiability problem.},
}

EndNote citation:

%0 Report
%A Jha, Susmit Kumar 
%A Seshia, Sanjit A. 
%A Limaye, Rhishikesh Shrikant 
%T On the Computational Complexity of Satisfiability Solving for String Theories
%I EECS Department, University of California, Berkeley
%D 2009
%8 March 16
%@ UCB/EECS-2009-41
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-41.html
%F Jha:EECS-2009-41