Combining Static Analysis and Targeted Symbolic Execution for Scalable Bug-finding in Application Binaries
Bibliographic record
Abstract
Manual software testing is laborious and prone to human error. Yet, it is the most popular method for quality assurance. Automating the test-case generation promises better effectiveness, especially for exposing “deep” corner-case bugs. Symbolic execution is an automated technique for program analysis that has recently become practical due to advances in constraint solvers. It stands out as an automated testing technique that has no false positives, it eventually enumerates all feasible program executions, and can prioritize executions of interest. However, “path explosion”, the fact that the number of program executions is typically at least exponential in the size of the program, hinders the adoption of symbolic execution in the real world, where program commonly reaches millions of lines of code. \n \nIn this thesis, we present a method for generating test-cases using symbolic execution which reach a given potentially buggy “target” statement. Such a potentially buggy program statement can be found by static program analysis or from crash-reports given by users and serve as input to our technique. The test-case generated by our technique serves as a proof of the bug. Generating crashes at the target statement have many applications including re-producing crashes, checking warnings generated by static program analysis tools, or analysis of source code patches in code review process. By constantly steering the symbolic execution along the branches that are most likely to lead to the target program statement and pruning the search space that are unlikely to reach the target, we were able to detect deep bugs in real programs. To tackle exponential growth of program paths, we propose a new scheme to manage program execution paths without exhausting memory. Experiments on real-life programs demonstrate that our tool WatSym, built on selective symbolic execution engine S2E, can generate crashing inputs in feasible time and order of magnitude better than symbolic approaches (as embodied by S2E) failed.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.001 | 0.006 |
| Meta-epidemiology (narrow) | 0.002 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.001 |
| Bibliometrics | 0.003 | 0.001 |
| Science and technology studies | 0.001 | 0.002 |
| Scholarly communication | 0.001 | 0.002 |
| Open science | 0.002 | 0.003 |
| Research integrity | 0.001 | 0.001 |
| Insufficient payload (model declined to judge) | 0.003 | 0.001 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".