Team for Research in
Ubiquitous Secure Technology

Citation
David A Molnar, David Wagner. "Catchconv: Symbolic execution and run-time type inference for integer conversion errors". Technical report, University of California Berkeley, 2007-23, February, 2007.

Abstract
We propose an approach that combines symbolic execution and run-time type inference from a sample program run to generate test cases, and we apply our approach to signed/unsigned conversion errors in programs. A signed/unsigned conversion error occurs when a program makes control flow decisions about a value based on treating it as a signed integer, but then later converts the value to an unsigned integer in a way that breaks the program's implicit assumptions. Our tool follows the approach of Larson and Austin in using an example input to pick a program path for analysis, and we use symbolic execution to attempt synthesis of a program input exhibiting an error. We describe a proof of concept implementation that uses the Valgrind binary analysis framework and the STP decision procedure, and we report on preliminary experiences. Our implementation is available at http://www.sf.net/projects/catchconv .

Electronic downloads

• HTML

  David A Molnar, David Wagner. <a
  href="http://www.truststc.org/pubs/503.html"
  ><i>Catchconv: Symbolic execution and run-time type
  inference for integer conversion errors</i></a>,
  Technical report,  University of California Berkeley,
  2007-23, February, 2007.

• Plain text

  David A Molnar, David Wagner. "Catchconv: Symbolic
  execution and run-time type inference for integer conversion
  errors". Technical report,  University of California
  Berkeley, 2007-23, February, 2007.

• BibTeX

  @techreport{MolnarWagner07_CatchconvSymbolicExecutionRuntimeTypeInferenceForInteger,
      author = {David A Molnar and David Wagner},
      title = {Catchconv: Symbolic execution and run-time type
                inference for integer conversion errors},
      institution = {University of California Berkeley},
      number = {2007-23},
      month = {February},
      year = {2007},
      abstract = {We propose an approach that combines symbolic
                execution and run-time type inference from a
                sample program run to generate test cases, and we
                apply our approach to signed/unsigned conversion
                errors in programs. A signed/unsigned conversion
                error occurs when a program makes control flow
                decisions about a value based on treating it as a
                signed integer, but then later converts the value
                to an unsigned integer in a way that breaks the
                program's implicit assumptions. Our tool follows
                the approach of Larson and Austin in using an
                example input to pick a program path for analysis,
                and we use symbolic execution to attempt synthesis
                of a program input exhibiting an error. We
                describe a proof of concept implementation that
                uses the Valgrind binary analysis framework and
                the STP decision procedure, and we report on
                preliminary experiences. Our implementation is
                available at http://www.sf.net/projects/catchconv .},
      URL = {http://www.truststc.org/pubs/503.html}
  }
  

Posted by David A Molnar on 28 Jan 2009.
Groups: trust
For additional information, see the Publications FAQ or contact webmaster at www truststc org.