Detecting Behaviorally Equivalent Functions via Symbolic Execution

Loading...
Thumbnail Image

Persistent link to this item

Statistics
View Statistics

Journal Title

Journal ISSN

Volume Title

Title

Detecting Behaviorally Equivalent Functions via Symbolic Execution

Alternative title

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

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.