Detecting Behaviorally Equivalent Functions via Symbolic Execution
2016
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
Detecting Behaviorally Equivalent Functions via Symbolic Execution
Alternative title
Authors
Published Date
2016
Publisher
Type
Thesis or Dissertation
Abstract
Software bugs are a reality of programming. They can be difficult to identify and resolve,
even for the most experienced programmers. Certain bugs may even be impossible to remove
because they provide some desired functionality. For this reason, designers of modern
security-critical applications must accept the inevitable existence of bugs and find ways to
detect and recover from the errors they cause. One approach to error detection involves running
multiple implementations of a single program at the same time, on the same input, and
comparing the results. Divergence of the behavior of the different implementations indicates
the existence of a bug.
The question we consider in this paper is how to construct these diverse implementations
of security-critical programs in a cost-effective way. The solution we propose is to
first find existing diverse function implementations and then use these function implementations
as building blocks for diverse program implementations. To find diverse function
implementations, we use a technique we call adaptor synthesis to compare arbitrary functions
for behavioral equivalence. To account for di↵erences in input argument structure
between arbitrary functions we allow for adaptor functions, or adaptors, that convert from
one argument structure to another. Using adaptors, the problem of determining whether
two arbitrary functions are behaviorally equivalent becomes the problem of synthesizing an
adaptor between the two functions that makes their output equivalent on all inputs in a
specified domain.
Along with presenting our adaptor synthesis technique, we describe an implementation
for comparing functions for behavioral equivalence at the binary level on the Linux x86-64
platform using a family of adaptors that allows arithmetic combinations of integer values.
Description
Related to
Replaces
License
Collections
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
Other identifiers
Suggested citation
Hietala, Kesha. (2016). Detecting Behaviorally Equivalent Functions via Symbolic Execution. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/181385.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.