Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
State Joining and Splitting for the Symbolic Execution of Binaries
verfasst von : Trevor Hansen, Peter Schachte, Harald Søndergaard
Erschienen in: Runtime Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Symbolic execution can be used to explore the possible run-time states of a program. It makes use of a concept of “state” where a variable’s value has been replaced by an expression that gives the value as a function of program input. Additionally, a state can be equipped with a summary of control-flow history: a “path constraint” keeps track of the class of inputs that would have caused the same flow of control. But even simple programs can have trillions of paths, so a path-by-path analysis is impractical. We investigate a “state joining” approach to making symbolic execution more practical and describe the challenges of applying state joining to the analysis of unmodified Linux x86 executables. The results so far are mixed, with good results for some code. On other examples, state joining produces cumbersome constraints that are more expensive to solve than those generated by normal symbolic execution.