Multi-Pass Targeted Dynamic Symbolic Execution

• URL: http://arxiv.org/abs/2408.07797v1
• Date: Wed, 14 Aug 2024 20:14:59 GMT
• Title: Multi-Pass Targeted Dynamic Symbolic Execution
• Authors: Tuba Yavuz,
• Abstract summary: We present a Multi-Pass Targeted Dynamic Execution approach that starts from a target program location and moves backward until it reaches a specified entry point. Our approach achieves on average 4X reduction in the number of paths explored and 2X speedup.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Dynamic symbolic execution (DSE) provides a precise means to analyze programs and it can be used to generate test cases and to detect a variety of bugs including memory vulnerabilities. However, the path explosion problem may prevent a symbolic executor from covering program locations or paths of interest. In this paper, we present a Multi-Pass Targeted Dynamic Symbolic Execution approach that starts from a target program location and moves backward until it reaches a specified entry point to check for reachability, to detect bugs on the feasible paths between the entry point and the target, and to collect constraints about the memory locations accessed by the code. Our approach uses a mix of backward and forward reasoning passes. It introduces an abstract address space that gets populated during the backward pass and uses unification to precisely map the abstract objects to the objects in the concrete address space. We have implemented our approach in a tool called DESTINA using KLEE, a DSE tool. We have evaluated DESTINA using SvComp benchmarks from the memory safety and control-flow categories. Results show that DESTINA can detect memory vulnerabilities precisely and it can help DSE reach target locations faster when it struggles with the path explosion. Our approach achieves on average 4X reduction in the number of paths explored and 2X speedup.

Related papers

• Vital: Vulnerability-Oriented Symbolic Execution via Type-Unsafe Pointer-Guided Monte Carlo Tree Search [18.500951309269396]
  This paper proposes a new vulnerability-oriented symbolic execution via type-unsafe pointer-guided Monte Carlo Tree Search (MCTS) We show that Vital could cover up to 90.03% more unsafe pointers and detect up to 37.50% more unique memory errors. In the latter, the results show that Vital could achieve a speedup of up to 30x execution time and a reduction of up to 20x memory consumption.
  arXiv  Detail & Related papers  (2024-08-16T14:29:57Z)
• RTracker: Recoverable Tracking via PN Tree Structured Memory [71.05904715104411]
  We propose a recoverable tracking framework, RTracker, that uses a tree-structured memory to dynamically associate a tracker and a detector to enable self-recovery. Specifically, we propose a Positive-Negative Tree-structured memory to chronologically store and maintain positive and negative target samples. Our core idea is to use the support samples of positive and negative target categories to establish a relative distance-based criterion for a reliable assessment of target loss.
  arXiv  Detail & Related papers  (2024-03-28T08:54:40Z)
• Rampo: A CEGAR-based Integration of Binary Code Analysis and System Falsification for Cyber-Kinetic Vulnerability Detection [14.7195342186018]
  Rampo can perform binary code analysis to identify cyber kinetic vulnerabilities in CPS. Our tool could compute the same number of vulnerabilities while leading to a speedup that ranges from 3x to 98x.
  arXiv  Detail & Related papers  (2024-02-20T01:36:08Z)
• SparseTrack: Multi-Object Tracking by Performing Scene Decomposition based on Pseudo-Depth [84.64121608109087]
  We propose a pseudo-depth estimation method for obtaining the relative depth of targets from 2D images. Secondly, we design a depth cascading matching (DCM) algorithm, which can use the obtained depth information to convert a dense target set into multiple sparse target subsets. By integrating the pseudo-depth method and the DCM strategy into the data association process, we propose a new tracker, called SparseTrack.
  arXiv  Detail & Related papers  (2023-06-08T14:36:10Z)
• SalienDet: A Saliency-based Feature Enhancement Algorithm for Object Detection for Autonomous Driving [160.57870373052577]
  We propose a saliency-based OD algorithm (SalienDet) to detect unknown objects. Our SalienDet utilizes a saliency-based algorithm to enhance image features for object proposal generation. We design a dataset relabeling approach to differentiate the unknown objects from all objects in training sample set to achieve Open-World Detection.
  arXiv  Detail & Related papers  (2023-05-11T16:19:44Z)
• SegmentMeIfYouCan: A Benchmark for Anomaly Segmentation [111.61261419566908]
  Deep neural networks (DNNs) are usually trained on a closed set of semantic classes. They are ill-equipped to handle previously-unseen objects. detecting and localizing such objects is crucial for safety-critical applications such as perception for automated driving.
  arXiv  Detail & Related papers  (2021-04-30T07:58:19Z)
• Distractor-Aware Fast Tracking via Dynamic Convolutions and MOT Philosophy [63.91005999481061]
  A practical long-term tracker typically contains three key properties, i.e. an efficient model design, an effective global re-detection strategy and a robust distractor awareness mechanism. We propose a two-task tracking frame work (named DMTrack) to achieve distractor-aware fast tracking via Dynamic convolutions (d-convs) and Multiple object tracking (MOT) philosophy. Our tracker achieves state-of-the-art performance on the LaSOT, OxUvA, TLP, VOT2018LT and VOT 2019LT benchmarks and runs in real-time (3x faster
  arXiv  Detail & Related papers  (2021-04-25T00:59:53Z)
• Target-Aware Object Discovery and Association for Unsupervised Video Multi-Object Segmentation [79.6596425920849]
  This paper addresses the task of unsupervised video multi-object segmentation. We introduce a novel approach for more accurate and efficient unseen-temporal segmentation. We evaluate the proposed approach on DAVIS$_17$ and YouTube-VIS, and the results demonstrate that it outperforms state-of-the-art methods both in segmentation accuracy and inference speed.
  arXiv  Detail & Related papers  (2021-04-10T14:39:44Z)
• An Exploration of Target-Conditioned Segmentation Methods for Visual Object Trackers [24.210580784051277]
  We show how to transform a bounding-box tracker into a segmentation tracker. Our analysis shows that such methods allow trackers to compete with recently proposed segmentation trackers.
  arXiv  Detail & Related papers  (2020-08-03T16:21:18Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.