Between Dec 19, 2024 and Jan 2, 2025, datasets can be submitted to DRUM but will not be processed until after the break. Staff will not be available to answer email during this period, and will not be able to provide DOIs until after Jan 2. If you are in need of a DOI during this period, consider Dryad or OpenICPSR. Submission responses to the UDC may also be delayed during this time.

Browsing by Author "Sharma, Vaibhav"

Now showing 1 - 4 of 4
  • Thumbnail Image
    Item
    Adapter Synthesis: Synthesizing And Repairing Programs Using Scalable Symbolic Execution
    (2020-02) Sharma, Vaibhav
    Independently developed codebases typically contain many segments of code that perform the same or closely related operations (semantic clones). Finding functionally equivalent segments enables applications like replacing a segment by a more efficient or more secure alternative. Such related segments often have different interfaces, so some glue code (an adapter) is needed to replace one with the other. We present an algorithm that searches for replaceable code segments by attempting to synthesize an adapter between them from some finite family of adapters; it terminates if it finds no possible adapter. The use of symbolic execution during adapter search implicitly relies on being able to summarize the entire adapter into a single formula. Merging related execution paths is a powerful technique for reducing path explosion in symbolic execution. One approach, introduced and dubbed “veritesting” by Avgerinos et al., works by statically translating a bounded control flow region into a single formula. Java’s typed memory structure is very different from a binary, but we present an extension of previous path-merging approaches for symbolic execution of Java. Bugs in commercial software and third-party components are an undesirable and expensive phenomenon. Such software is usually released to users only in binary form. The lack of source code renders users of such software dependent on their software vendors for repairs of bugs. Such dependence is even more harmful if the bugs introduce new vulnerabilities in the software. Being able to automatically repair security bugs breaks this dependence and increases software robustness. In the third part of this dissertation, we present an automated program repair approach for binary code.
  • Thumbnail Image
    Item
    Contract discovery from black-box components
    (2018) Sharma, Vaibhav; Byun, Taejoon; McCamant, Stephen; Rayadurgam, Sanjai; Heimdahl, Mats
    Complex computer-controlled systems are commonly constructed in a middle-out fashion where existing subsystems and available components have a significant influence on system architecture and drive design decisions. During system design, the architect must verify that the components, put together as specified in the architecture, will achieve the desired system behavior. This typically leads to further design modifications or adjustments to requirements triggering another iteration of the design-verify cycle. For software components that are acquired from third-parties, often the only definitive source of information about the component's system-relevant behavior -- its contract -- is its object code. We posit that existing static and dynamic analysis techniques can be used to discover contracts that can help the system designer and specifically discuss how symbolic execution of object code may be particularly well-suited for this purpose.
  • Thumbnail Image
    Item
    Discovering Instructions for Robust Binary-level Coverage Criteria
    (2017) Sharma, Vaibhav; Byun, Taejoon; McCamant, Stephen; Rayadurgam, Sanjai; Heimdahl, Mats
    Object-Branch Coverage (OBC) is often used to measure e ective- ness of test suites, when source code is unavailable. The traditional OBC de nition can be made more resilient to variations in compil- ers and the structure of generated code by creating more robust de nitions. However nding which instructions should be included in each new de nition is laborious, error-prone, and architecture- dependent. We automate the discovery of instructions to be in- cluded for an improved OBC de nition on the X86 and ARM archi- tectures. We discover all possible valid instructions by symbolically executing instruction decoders for X86 and ARM instructions. For each discovered instruction, we translate it to Vine IR, and check if the Vine IR translation satis es the OBC de nition. We verify the correctness of our tool by comparing its output with the X86 and ARM architecture manuals. Our automated instruction clas- si cation facilitates development of more robust OBC de nitions with better bug- nding ability and lesser sensitivity to compiler variations.
  • Thumbnail Image
    Item
    Toward Rigorous Object-Code Coverage Criteria
    (2017-06-13) Byun, Taejoon; Sharma, Vaibhav; Rayadurgam, Sanjai; McCamant, Stephen; Heimdahl, Mats
    Object-branch coverage (OBC) is often used as a measure of the thoroughness of tests suites, augmenting or substituting source-code based structural criteria such as branch coverage and modified condition/decision coverage (MC/DC). In addition, with the increasing use of third-party components for which source-code access may be unavailable, robust object-code coverage criteria are essential to assess how well the components are exercised during testing. While OBC has the advantage of being programming language independent and is amenable to non-intrusive coverage measurement techniques, variations in compilers, and the optimizations they perform can substantially change what is seen as an object branch, which itself appears to be an informally understood concept. To address the need for a robust object coverage criterion, this paper proposes a rigorous definition of OBC such that it captures well the semantic of source code branches for a given instruction set architecture. We report an empirical assessment of these criteria for the Intel x86 instruction set on several examples from embedded control systems software. Preliminary results indicate that object-code coverage can be made robust to compilation variations and is comparable in its bug-finding efficacy to source level MC/DC.