Enhanced symbolic execution for patch testing and document recovery

Software plays an important role in everyday life, from consumer applications to mission-critical systems. This richness of functionality, however, comes at the price of complexity. Even though software systems are developed manually, they are increasingly too complex to be fully understood by any s...

Full description

Bibliographic Details
Main Author: Kuchta, Tomasz
Other Authors: Cadar, Cristian ; Donaldson, Alastair
Published: Imperial College London 2016
Subjects:
004
Online Access:https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.739615
id ndltd-bl.uk-oai-ethos.bl.uk-739615
record_format oai_dc
spelling ndltd-bl.uk-oai-ethos.bl.uk-7396152019-03-05T15:30:14ZEnhanced symbolic execution for patch testing and document recoveryKuchta, TomaszCadar, Cristian ; Donaldson, Alastair2016Software plays an important role in everyday life, from consumer applications to mission-critical systems. This richness of functionality, however, comes at the price of complexity. Even though software systems are developed manually, they are increasingly too complex to be fully understood by any single programmer. As a consequence, software bugs, which are often the result of programming errors, are commonplace. In this thesis we present two techniques based on dynamic symbolic execution which address the problem of software reliability from two angles: testing software patches and recovering an incorrect program input. We present shadow symbolic execution, a technique that generates test inputs exercising the new program behaviours introduced by a software patch. The old and the new version are executed in the same symbolic execution instance, with the old version shadowing the new one. Whenever the versions diverge at a branch point, we generate an input exercising the divergence and comprehensively test the new behaviours of the new version. We evaluate our technique on a set of incorrect patches from GNU Coreutils for which it generates inputs that exercise newly added behaviours and expose some of the regression bugs. We also present Docovery, a novel document recovery technique that makes it possible to fix broken documents without any knowledge of the file format. Starting from the code path executed when processing a broken document, Docovery explores alternative paths that avoid the error, and makes small changes to the document in order to force the application to follow one of these alternative paths. We evaluate Docovery on files processed by several popular applications: the e-mail client pine, the pagination tool pr and the binary file utilities dwarfdump and readelf. The thesis also includes a motivational large-scale study on the correctness of PDF documents and document readers.004Imperial College Londonhttps://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.739615http://hdl.handle.net/10044/1/58232Electronic Thesis or Dissertation
collection NDLTD
sources NDLTD
topic 004
spellingShingle 004
Kuchta, Tomasz
Enhanced symbolic execution for patch testing and document recovery
description Software plays an important role in everyday life, from consumer applications to mission-critical systems. This richness of functionality, however, comes at the price of complexity. Even though software systems are developed manually, they are increasingly too complex to be fully understood by any single programmer. As a consequence, software bugs, which are often the result of programming errors, are commonplace. In this thesis we present two techniques based on dynamic symbolic execution which address the problem of software reliability from two angles: testing software patches and recovering an incorrect program input. We present shadow symbolic execution, a technique that generates test inputs exercising the new program behaviours introduced by a software patch. The old and the new version are executed in the same symbolic execution instance, with the old version shadowing the new one. Whenever the versions diverge at a branch point, we generate an input exercising the divergence and comprehensively test the new behaviours of the new version. We evaluate our technique on a set of incorrect patches from GNU Coreutils for which it generates inputs that exercise newly added behaviours and expose some of the regression bugs. We also present Docovery, a novel document recovery technique that makes it possible to fix broken documents without any knowledge of the file format. Starting from the code path executed when processing a broken document, Docovery explores alternative paths that avoid the error, and makes small changes to the document in order to force the application to follow one of these alternative paths. We evaluate Docovery on files processed by several popular applications: the e-mail client pine, the pagination tool pr and the binary file utilities dwarfdump and readelf. The thesis also includes a motivational large-scale study on the correctness of PDF documents and document readers.
author2 Cadar, Cristian ; Donaldson, Alastair
author_facet Cadar, Cristian ; Donaldson, Alastair
Kuchta, Tomasz
author Kuchta, Tomasz
author_sort Kuchta, Tomasz
title Enhanced symbolic execution for patch testing and document recovery
title_short Enhanced symbolic execution for patch testing and document recovery
title_full Enhanced symbolic execution for patch testing and document recovery
title_fullStr Enhanced symbolic execution for patch testing and document recovery
title_full_unstemmed Enhanced symbolic execution for patch testing and document recovery
title_sort enhanced symbolic execution for patch testing and document recovery
publisher Imperial College London
publishDate 2016
url https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.739615
work_keys_str_mv AT kuchtatomasz enhancedsymbolicexecutionforpatchtestinganddocumentrecovery
_version_ 1718993588067500032