PaperlayerView exact revision on arXiv

Source-linked AI summary

SAVIOR: Towards Bug-Driven Hybrid Testing

Yaohui Chen, Peng Li, Jun Xu, Shengjian Guo, Rundong Zhou, Yulong Zhang, Taowei, Long Lu

arXiv:1906.07327v1cs.SE

TL;DR

Coverage-driven hybrid testing can be inefficient for vulnerability detection because it treats seeds and reached code uniformly. SAVIOR uses bug-driven prioritization and verification, detecting vulnerabilities 43.4% faster than DRILLER on average.

  • Problem

    Coverage-driven hybrid testing can inefficiently allocate effort across code regions and may miss vulnerabilities after reaching their paths.

  • Method

    SAVIOR prioritizes concolic execution of vulnerability-likely seeds and verifies vulnerable candidates along execution paths using SMT-based proofs.

  • Results

    SAVIOR outperforms coverage-driven hybrid tools, detecting vulnerabilities 43.4% faster than DRILLER on average.

  • Takeaways & Limitations

    Bug-driven prioritization and verification improve the efficiency of hybrid testing for vulnerability detection.

  • Takeaways & Limitations

    The paper identifies limitations and future directions for SAVIOR’s current design.

Abstract

from arXiv · show

Hybrid testing combines fuzz testing and concolic execution. It leverages fuzz testing to test easy-to-reach code regions and uses concolic execution to explore code blocks guarded by complex branch conditions. However, its code coverage-centric design is inefficient in vulnerability detection. First, it blindly selects seeds for concolic execution and aims to explore new code continuously. However, as statistics show, a large portion of the explored code is often bug-free. Therefore, giving equal attention to every part of the code during hybrid testing is a non-optimal strategy. It slows down the detection of real vulnerabilities by over 43%. Second, classic hybrid testing quickly moves on after reaching a chunk of code, rather than examining the hidden defects inside. It may frequently miss subtle vulnerabilities despite that it has already explored the vulnerable code paths. We propose SAVIOR, a new hybrid testing framework pioneering a bug-driven principle. Unlike the existing hybrid testing tools, SAVIOR prioritizes the concolic execution of the seeds that are likely to uncover more vulnerabilities. Moreover, SAVIOR verifies all vulnerable program locations along the executing program path. By modeling faulty situations using SMT constraints, SAVIOR reasons the feasibility of vulnerabilities and generates concrete test cases as proofs. Our evaluation shows that the bug-driven approach outperforms mainstream automated testing techniques, including state-of-the-art hybrid testing systems driven by code coverage. On average, SAVIOR detects vulnerabilities 43.4% faster than DRILLER and 44.3% faster than QSYM, leading to the discovery of 88 and 76 more uniquebugs,respectively.Accordingtotheevaluationon11 well fuzzed benchmark programs, within the first 24 hours, SAVIOR triggers 481 UBSAN violations, among which 243 are real bugs.

I. INTRODUCTION · II. BACKGROUND AND MOTIVATION · A. Hybrid Testing

SAVIOR reframes hybrid testing as bug-driven vulnerability detection: it prioritizes concolic execution toward potentially vulnerable code and verifies labeled vulnerabilities along executed paths. Motivated by the coverage-centric limitations of existing hybrid testing, it improves detection speed and bug yield over DRILLER and QSYM.

  • I. INTRODUCTION: Hybrid testing combines fuzz testing for path exploration with concolic execution for solving hard-to-resolve branch conditions.When fuzzing makes little progress, the controller switches to concolic execution, which re-runs fuzz-generated seeds and explores untouched sibling branches.
  • I. INTRODUCTION: Existing hybrid testing treats fuzzing seeds equally, wasting costly testing effort on code regions that may lack vulnerabilities.This coverage-driven strategy can slow vulnerability detection because explored code is often bug-free.
  • I. INTRODUCTION: SAVIOR introduces bug-driven prioritization by statically labeling suspicious program locations and favoring seeds that reach branches guarding more vulnerability labels.The approach prioritizes concolic execution of seeds with higher potential to uncover vulnerabilities rather than running all seeds without distinction.
  • I. INTRODUCTION: SAVIOR also performs bug-guided verification by synthesizing a faulty constraint for each labeled vulnerability encountered on the concolic execution path.A satisfiable constraint yields a concrete proof input, while an unsatisfiable constraint establishes infeasibility under the current path condition.
  • I. INTRODUCTION: 43.4% faster than DRILLER and 44.3% faster than QSYM, SAVIOR detects vulnerabilities faster on average and discovers 88 and 76 more security violations in 24 hours, respectively.Across 11 well-studied benchmarks, SAVIOR discovers 481 unique security violations.
  • II. BACKGROUND AND MOTIVATION: The background section motivates SAVIOR by identifying hybrid testing’s limitations in vulnerability detection and illustrating them through examples.Hybrid testing is presented as a combination of fuzz testing and concolic execution intended to achieve high code coverage.
  • A. Hybrid Testing: In the tcpdump example, fuzzing cannot synthesize inputs matching packet and link-layer types across a 2^32-size mutation space, so hybrid testing switches to concolic execution.The concolic executor solves packet_type to PACKET1, generates a seed for the missed branch, and resumes testing with the fuzzer.
  • A. Hybrid Testing: Despite implementation differences such as QSYM’s continuous concolic execution, existing hybrid tools schedule seeds indiscriminately because they assume equal potential for new coverage.This shared scheduling philosophy motivates SAVIOR’s vulnerability-aware prioritization.

B. Motivation

Existing hybrid testing is inefficient because coverage-driven exploration spends substantial time on hard-to-reach, often bug-free code instead of prioritizing vulnerable code. It can also miss defects after reaching vulnerable locations, making vulnerability detection substantially slower.

  • Inefficiency in Covering Vulnerable Code: Coverage-driven hybrid testing overspends its time budget saturating hard-to-reach code compartments, even though prioritizing vulnerable code would discover more vulnerabilities sooner.The current method does not prioritize vulnerable code despite its potential to improve vulnerability discovery within a limited time frame.
  • Inefficiency in Covering Vulnerable Code: 43.4% and 44.3%: delayed vulnerability coverage defers DRILLER and QSYM, respectively, reducing vulnerability-finding efficiency.These delays occur because concolic execution can run slowly while fuzz testing continues on other paths.
  • Deficiency in Vulnerability Detection: Hybrid testing may reach a vulnerable location along the correct path yet fail to identify the vulnerability itself.The demonstrated objdump-2.29 defect is an integer overflow caused by using an attacker-controlled extreme size in a memory allocation request.
  • Deficiency in Vulnerability Detection: Random mutation is unlikely to trigger the integer overflow because synthesizing the required extreme value requires searching a space of 2^32 or 2^64 possibilities.Hybrid testing can quickly generate a seed reaching line 15, but the input bytes are unconstrained as they propagate to section→size.

III. DESIGN · A. Core Techniques

SAVIOR’s core design is bug-driven: it prioritizes concolic execution seeds by estimated vulnerability potential and verifies every vulnerability site reached along explored paths. It combines sound reachability and UBSan-based labeling with satisfiability checking to find and validate bugs more thoroughly.

  • A. Core Techniques: SAVIOR introduces bug-driven prioritization and bug-guided verification to find bugs faster and more thoroughly.These are the two techniques that define SAVIOR’s core design.
  • A. Core Techniques: SAVIOR prioritizes seeds for concolic execution using target-source information about their potential to trigger vulnerabilities.This replaces classic hybrid testing’s blind seed scheduling.
  • A. Core Techniques: SAVIOR estimates newly explorable regions through static reachability analysis combined with runtime identification of unexplored branches.It computes reachable basic blocks statically and treats blocks reachable from unexplored execution-path branches as newly explorable.
  • A. Core Techniques: SAVIOR uses UBSan labels in each code region to quantify potential vulnerabilities, then statically filters conservative instrumentation’s dummy labels.UBSan annotates three potential bug types in the program under test.
  • A. Core Techniques: For a seed with n unexplored branches, SAVIOR scores each branch’s reachable UBSan labels as e−0.05S_i×L_i and combines the weighted potentials.L_i is the potential of branch i, while S_i counts prior solving attempts.
  • A. Core Techniques: SAVIOR decreases branch potential as solving attempts grow and averages candidate-branch scores to maximize bug-detection gain per unit time.This gradually de-prioritizes hard-to-solve branches while favoring seeds leading to more unverified bugs.
  • A. Core Techniques: Bug-guided verification extracts vulnerability labels along each seed’s execution path and checks each implanted predicate for satisfiability under the current path condition.A satisfiable predicate validates its corresponding vulnerability, enabling detection of an integer overflow missed by classic hybrid testing.

B. System Design · 1) The Compilation Tool-chain:

SAVIOR’s LLVM/Clang-based compilation tool-chain supports vulnerability labeling, reachability-based prioritization, and separate targets for fuzzing, concolic execution, and coordination. It uses UBSan-trigger conditions and static filtering to guide bug verification while reducing misleading labels.

  • B. System Design: SAVIOR’s architecture combines a Clang/LLVM compilation tool-chain, an AFL-derived fuzzer, a KLEE-based concolic executor, and a hybrid coordinator.These components are orchestrated as the framework’s overall architecture.
  • B. System Design: The compilation tool-chain labels potential vulnerabilities, analyzes control-flow reachability, and builds targets for SAVIOR’s components.These are the tool-chain’s stated purposes.
  • 1) The Compilation Tool-chain:: UBSan labels bug families, and SAVIOR attaches !saviorBugNum metadata to each label for reachability analysis.SAVIOR ignores less security-relevant UBSan types such as misaligned references.
  • 1) The Compilation Tool-chain:: UBSan over-approximates vulnerabilities for soundness, while SAVIOR solves each labeled triggering condition to produce a bug witness or prove infeasibility.For example, OOB array access is triggered when an index falls outside 0 through array size minus 1.
  • 1) The Compilation Tool-chain:: Alternative labeling methods must comprehensively annotate potential vulnerabilities and synthesize input-dependent triggering conditions for concolic verification.Without data dependence on program input, concolic execution cannot guide verification toward the vulnerable condition.
  • 1) The Compilation Tool-chain:: 5.36% of labels are conservatively removed on average through static filtering of false positives.SAVIOR trims labels when dominator, variable-definition, and conflicting-constraint requirements hold; the example removes infeasible OOB and integer-overflow labels.
  • 1) The Compilation Tool-chain:: Reachability analysis counts UBSan labels forwardly reachable from each basic block and uses that count as the block’s importance metric for bug-driven prioritization.The analysis builds intraprocedure CFGs, bridges them through caller-callee relations, and resolves indirect calls with iterative Andersen point-to analysis.
  • 1) The Compilation Tool-chain:: The tool-chain builds a fuzzing binary, a SAVIOR binary, and LLVM bitcode, while the coordinator polls the fuzzer queue and prioritizes higher-importance seeds for concolic execution.The SAVIOR binary prints executed basic-block IDs, decoupling the fuzzer, concolic executor, and coordinator.

2) The Coordinator: · 3) The Concolic Executor:

The coordinator updates coverage, rescoring and selecting seeds for concolic execution, while also triaging generated seeds and tracking branch-solving attempts. The concolic executor independently guides branch solving, reuses a fork-server optimization, verifies vulnerability labels, and handles over-constraint and timeout concerns.

  • 2) The Coordinator:: The coordinator executes newly queued fuzzer seeds and updates global edge coverage using AFL’s hit-count ranges.The ranges are [1],,,,,, [32, 127], and [128, ∞).
  • 2) The Coordinator:: Using dynamically updated coverage, the coordinator rescores all seeds not already tested by the concolic executor.This rescoring follows the scheme presented in Section III-A.
  • 2) The Coordinator:: The coordinator sends top-ranked seeds to the concolic executor, breaking score ties in favor of seeds with the +cov property.+cov indicates that a seed brings new code coverage.
  • 2) The Coordinator:: The coordinator triages concolic-generated seeds, retaining those that add coverage or reach uncovered bug labels before transferring them to the fuzzer.It reruns the new seeds to make this determination.
  • 2) The Coordinator:: Uncovered branches gain one solving attempt, causing branches with higher solving-attempt values to be deprioritized.The coordinator updates these values after concolic execution.
  • 3) The Concolic Executor:: The concolic executor replays coordinator-scheduled seeds, selects branch conditions using coverage information, and performs bug-guided verification.It uses an independent coverage scheme because transformations between SAVIOR-binary and KLEE bitcode create edge-ID mismatches.
  • 3) The Concolic Executor:: Fork server mode avoids repeating KLEE initialization across seeds, addressing initialization costs that can exceed actual concolic execution time.KLEE otherwise loads bitcode, links library bitcode, and prepares global data before running a seed; Fig. 7 states that initialization occurs once and the executor is reused.
  • 3) The Concolic Executor:: When an uncovered vulnerability label is reached, the executor solves its triggering constraint and generates a proof seed if successful.For over-constraint cases, SAVIOR applies QSYM’s optimistic strategy only to vulnerability conditions, but relaxed constraints can yield false positives and do not count the label as covered.

IV. IMPLEMENTATION · V. EVALUATION

SAVIOR implements bug-driven hybrid testing by integrating fuzzing, concolic execution, and coordination infrastructure, then evaluates bug-driven prioritization and verification on artificial and real-world benchmarks. The evaluation compares SAVIOR with coverage-based, directed, and complex-condition fuzzing approaches, including a SAVIOR-based reimplementation of DRILLER.

  • IV. IMPLEMENTATION: SAVIOR combines an LLVM-based compiling tool-chain, AFL-based fuzzing, KLEE-based concolic execution, and Python middleware.The implementation contains about 3.3K lines of Python code and 4K lines of additional code.
  • IV. IMPLEMENTATION: Its concolic executor follows the concrete-input path while solving uncovered alternative branches to generate test cases.Generated seeds preserve unconstrained input bytes rather than padding them with random values.
  • IV. IMPLEMENTATION: SAVIOR adds fork-server execution to reduce KLEE’s time-consuming initialization overhead across seeds.The executor setup is reused while stateful changes from prior seed execution are cleaned up.
  • IV. IMPLEMENTATION: The implementation adapts UBSan-instrumented operations into executable LLVM IR so KLEE can process potentially vulnerable operations.UBSan intrinsic functions are replaced with general LLVM IR following KLEE’s existing replacements.
  • V. EVALUATION: The evaluation asks whether bug-driven prioritization finds vulnerabilities quicker and whether bug-guided verification finds them more thoroughly.These questions directly assess SAVIOR’s two key techniques.
  • V. EVALUATION: The benchmarks comprise the LAVA-M dataset with artificial vulnerabilities and ground truth, plus 8 extensively tested real-world programs.Details of the real-world programs are summarized in Table V.
  • V. EVALUATION: SAVIOR is compared with AFL, AFLGO, TFUZZ, and ANGORA, while DRILLER is reimplemented atop SAVIOR because the original cannot run many benchmarks reliably.The reimplemented DRILLER uses AFL and invokes concolic execution when AFL’s pending_favs attribute reaches 0.

A. Evaluation with LAVA-M · 1) Experimental Setup: · 2) Evaluation Results:

SAVIOR’s LAVA-M evaluation uses controlled, resource-matched 24-hour experiments and shows that bug-driven prioritization and verification improve vulnerability triggering efficiency and thoroughness. Hybrid tools generally trigger encountered vulnerabilities, while SAVIOR is especially advantageous when concolic execution is costly or hidden bugs require verification.

  • A. Evaluation with LAVA-M: Each fuzzer receives 3 CPU cores and runs for 24 hours on identical Amazon EC2 instances using the benchmark’s shipped seeds.Experiments run sequentially on 64-core, 256GB-RAM Intel Xeon E5 Broadwell instances with Ubuntu 16.04 LTS.
  • 1) Experimental Setup:: LAVA-M vulnerabilities are represented by inlined lava_get calls, which guide AFLGO and serve as vulnerability labels for SAVIOR’s bug-driven prioritization.The vulnerability condition is hardcoded in lava_get.
  • 2) Evaluation Results:: All fuzzers instantly reach LAVA-vulnerability code, but TFUZZ, ANGORA, DRILLER, QSYM, and SAVIOR trigger most or all vulnerabilities, unlike AFL and AFLGO.The triggering conditions are difficult constraints of the form 3… as described in the evaluation.
  • Vulnerability Finding Efficiency:: TFUZZ rapidly covers the listed vulnerabilities in base64 and uniq because several initial seeds reach them and program transformation immediately triggers encountered vulnerabilities.TFUZZ results for md5sum and who are omitted because a broken third-party dependency interrupts execution.
  • Vulnerability Finding Efficiency:: ANGORA triggers LAVA vulnerabilities immediately by evaluating f(x) = x with x = CONSTANT, though it does not find all vulnerabilities in who.Its missing who vulnerabilities are attributed to limitations discussed in the evaluation; the QEMU-based Angr tracer dependency is broken.
  • Vulnerability Finding Efficiency:: The three hybrid tools trigger every vulnerability their concolic executors encounter, and initial seeds let them reach all vulnerabilities in base64, uniq, and md5sum.Thus, those programs show rapid triggering regardless of seed scheduling.
  • Vulnerability Finding Efficiency:: Over 72 hours of continuous concolic execution are needed for QSYM to reach all LAVA bugs in who from AFL inputs, whereas SAVIOR prioritizes higher-potential seeds.Bug-guided verification also enables every fuzzer to disclose additional LAVA bugs beyond the listed vulnerabilities.

B. Evaluation with Real-world Programs · 1) Experimental Setup: · 2) Evaluation Results:

The real-world evaluation uses eight extensively tested programs with tool-specific fuzzing setups and compares vulnerability discovery, UBSan-label reachability, code coverage, and bug-guided verification over 24 hours. SAVIOR generally finds vulnerabilities faster and reaches more labels, while verification improves thoroughness across all programs, with limited benefit on djpeg.

  • B. Evaluation with Real-world Programs: 8 programs were selected for the real-world evaluation, using seeds shipped with AFL or vendors and configurations aligned with existing work.All programs had been extensively tested by industry and academic researchers.
  • 1) Experimental Setup:: UBSan labels guided AFLGO’s targeting and SAVIOR’s bug-driven prioritization, while ANGORA received developer-recommended handling for un-instrumented library functions.The setups were specific to each fuzzing tool and mostly followed the settings in Table II.
  • 1) Experimental Setup:: 24-hour experiments tracked triggered UBSan bugs and basic-block coverage, using UBSan-label IDs for deduplication and Mann–Whitney U-test p-values for pairwise comparisons.Each UBSan label corresponds to a unique potential defect.
  • 2) Evaluation Results:: 43.4% faster than DRILLER and 44.3% faster than QSYM, SAVIOR discovers vulnerabilities faster on average and in every case except djpeg.The reported improvements generally have p-values below 0.05, although readelf and objdump show quasi-significance because of randomness.
  • 2) Evaluation Results:: 19.68% more labels than DRILLER and 15.18% more than QSYM, SAVIOR reaches more UBSan labels among the hybrid tools.The 24-hour averages indicate that hybrid tools reach more labels than ordinary fuzzers by solving complex conditions.
  • 2) Evaluation Results:: SAVIOR’s vulnerability-finding efficiency does not stem from higher code coverage, which is similar to or slower than DRILLER and QSYM in several programs.The evaluated cases include tcpdump, libxml, tiff2pdf, objdump, and jasper.
  • 2) Evaluation Results:: All 8 programs gained new violations from bug-guided verification, with average increases ranging from 4.5% for SAVIOR to 61.2% for ANGORA.Verification helped ANGORA trigger 82 new UBSan bugs, but provided little benefit on djpeg because its smaller code base has fewer vulnerability labels.

C. Vulnerability Triage · VI. RELATED WORKS

SAVIOR’s UBSan findings were manually triaged to distinguish actionable bugs from likely harmless violations, while related work spans fuzzing, concolic execution, hybrid testing, and guided testing.

  • C. Vulnerability Triage: 481 UBSan violations were collected and manually classified by their consequences.The violations came from SAVIOR’s evaluated programs and additional programs excluded from the main evaluation because all fuzzers triggered fewer than 10 violations.
  • C. Vulnerability Triage: 141 violations resulted in logic errors, including incorrect computations, wrong outputs, and polluted conditional variables.These errors were part of the manually classified UBSan violations.
  • C. Vulnerability Triage: 102 violations led to OOB reads or writes, and 16 of the 243 OOB and logic errors were confirmed by developers.The 243 cases combine the 102 OOB cases and 141 logic-error cases.
  • C. Vulnerability Triage: 238 remaining cases were likely harmless because violations affected storage variables, expired immediately, or were handled by the program.These categories explain why some UBSan violations did not represent harmful behavior.
  • C. Vulnerability Triage: The case studies cover OOB errors, logic errors, and harmless violations, and all selected cases were fixed.One case was selected from each of the three triage categories.
  • C. Vulnerability Triage: One readelf case demonstrates an OOB access caused when input makes inote.namesz equal to 0, underflowing inote.namesz − 1 to the maximal unsigned value.The underflow causes an OOB access to inote.namedata; the case was fixed.
  • VI. RELATED WORKS: Related work mainly covers advanced fuzzing, concolic execution, state-of-the-art hybrid testing, and techniques that facilitate guided testing.These are the work categories identified as most related to SAVIOR.

A. Advanced Fuzzing … VII. CONCLUSION

The paper situates SAVIOR among advanced fuzzing, concolic execution, hybrid testing, and guided-testing approaches. SAVIOR replaces coverage-driven hybrid testing with bug-driven prioritization and verification to improve bug coverage.

  • A. Advanced Fuzzing: Advanced fuzzing improves exploration through collision reduction, hardware tracing, program transformation, and learned surrogate functions.SAVIOR instead uses bug-driven guidance to maximize bug coverage and verifies whether bugs exist in explored paths.
  • B. Concolic Execution: Symbolic execution provides systematic testing but suffers from high computation cost and path explosion.These limitations motivated concolic execution, which combines symbolic constraint solving with concrete execution.
  • B. Concolic Execution: Concolic execution incurs substantial overhead from emulation or heavy instrumentation, making purely concolic exploration impractical for large software.Hybrid testing addresses this by fuzzing broadly and invoking concolic execution on hard-to-solve branches.
  • C. Hybrid Testing: Hybrid testing evolved from interleaving random testing and concolic execution to using guided fuzzing for higher-quality concolic seeds.DRILLER coherently combines both components, while DigFuzz coordinates them using predicted path-exploration difficulty.
  • C. Hybrid Testing: QSYM improves hybrid-testing performance by tailoring unnecessary symbolic-interpretation and constraint-solving computations.The passage identifies slow concolic execution as a major restriction on hybrid testing.
  • C. Hybrid Testing: SAVIOR changes hybrid testing from code-coverage improvement toward bug-driven testing, prioritizing promising seeds and guiding verification of encountered vulnerabilities.This approach aims for quicker and better bug coverage.
  • D. Guided Software Testing: Targeted-testing approaches guide exploration toward specific code locations, using patch proximity or distances to vulnerable regions and other targets.Katch prioritizes seeds approaching patches, while AFLGO favors seeds exercising code regions nearer to targets.
  • VII. CONCLUSION: SAVIOR introduces bug-driven prioritization and bug-guided verification as two techniques that move hybrid testing beyond mainstream coverage-driven designs.It prioritizes concolic execution for seeds more likely to lead to vulnerabilities and examines vulnerable candidates along execution paths.

A. Program Instrumentation … APPENDIX B TECHNICAL DISCUSSION AND FUTURE WORK

SAVIOR instruments UBSan labels for bug-driven prioritization, reduces false-positive labels, and uses bug-guided verification to identify additional LAVA bugs. Its real-world evaluation compares triggered violations across fuzzers, while the appendix discusses design limitations, lessons, and future directions.

  • A. Program Instrumentation: SAVIOR instruments UBSan labels with !saviorBugNum metadata to support bug-driven prioritization.The instrumentation is shown in LLVM IR for the objdump defect motivating example.
  • B. UBSan Label Reduction: SAVIOR reduces UBSan labels that can be confirmed as false positives.Table IX reports the reduction results for the benchmark programs.
  • B. UBSan Label Reduction: 5.36% of UBSan labels are reduced on average across the benchmark programs.This average is reported in Table IX.
  • C. LAVA-M Evaluation: Bug-guided verification identifies a group of LAVA bugs not listed in the LAVA-M evaluation.Table X provides the IDs of these additional LAVA bugs.
  • D. Real World Benchmark Evaluation: SAVIOR’s UBSan violations are compared with those triggered by five other fuzzers in the real-world benchmark evaluation.The comparison results are summarized in Table XI, with triggered violations at 24 hours summarized in Table XII.
  • D. Real World Benchmark Evaluation: SAVIOR usually triggers a superset of the UBSan violations produced by the other fuzzers, particularly AFL and AFLGO.The passage interprets this as greater thoroughness in vulnerability finding.
  • APPENDIX B TECHNICAL DISCUSSION AND FUTURE WORK: The appendix discusses limitations of SAVIOR’s current design, learned insights, and possible future directions.It frames these topics as technical discussion and future work.
  • APPENDIX B TECHNICAL DISCUSSION AND FUTURE WORK: SAVIOR uses sound algorithms to label vulnerabilities, but over-approximation may introduce many false-positive labels.The passage identifies imprecision as a limitation of this labeling approach.

Over-approximation in Vulnerability Labeling: · Prediction in Vulnerability Detection:

SAVIOR’s vulnerability labeling can over-approximate, weakening prioritization, while contradictory predicates terminate labeling-site exploration. The paper proposes finer-grained pruning and future path-constraint prediction using weakest preconditions to anticipate vulnerability-triggering executions.

  • Over-approximation in Vulnerability Labeling:: Table X lists unlisted LAVA-M bugs triggered through bug-guided verification.The table specifically records IDs of unlisted bugs in LAVA-M.
  • Over-approximation in Vulnerability Labeling:: Table XI compares violations triggered by SAVIOR with those triggered by other fuzzers using (+X/-Y) difference notation.+X denotes violations triggered by the other fuzzer but not SAVIOR, while -Y denotes violations triggered by SAVIOR but not that fuzzer.
  • Over-approximation in Vulnerability Labeling:: 43.4% and 44.3% more violations than DRILLER and QSYM, respectively, are reported for SAVIOR in 24-hour UBSan testing.Table XII compares unique UBSan violations triggered by different fuzzers over 24 hours.
  • Over-approximation in Vulnerability Labeling:: Dummy vulnerability labels can weaken SAVIOR’s prioritization, motivating rule-based filtering and finer-grained static-analysis pruning.The design filters false-positive labels with rules, while future work may incorporate complementary static analyses such as STACK and Hathhorn et al.’s approach.
  • Over-approximation in Vulnerability Labeling:: SAVIOR terminates exploration at a labeling site when the label’s guarding predicates contradict the current path condition.Continuing after such a contradiction cannot produce a valuable test input.
  • Prediction in Vulnerability Detection:: Runtime information from previous executions may predict whether an explored path can trigger a vulnerability before reaching its site.The proposed direction requires backwardly summarizing path constraints from labeled sites to predecessors in explored paths.
  • Prediction in Vulnerability Detection:: Weakest preconditions, derived from Hoare logic, are identified as the core technique for backwardly summarizing those path constraints.This summary connects labeled vulnerability sites with predecessor states in explored executions.
Loading 1906.07327v1…