Downloads provided by UsageCounts
Characterization of bugs and attack vectors is in many practical scenarios as important as their finding. Recently, Girol et al. have introduced the concept of robust reachability which ensures a perfect reproducibility of the reported violations by distinguishing input which are under the control of the attacker (controlled input) from those which are not (uncontrolled input), and proposed first automated analysis for it. While it is a step toward distinguishing severe bugs from benign ones, it fails to describe violations that are mostly reproducible, i.e., when triggering conditions are likely to happen, meaning that they happen for all uncontrolled input but a few corner cases. To address this issue, we propose to leverage theory-agnostic abduction techniques to generate constraints on the uncontrolled program input that ensure that a target property is robustly satisfied, which is an extension of robust reachability that is generic on the type of trace property and on the technology used to verify the properties. We show that our approach is complete w.r.t. its inference language, and we additionally discuss strategies for the efficient exploration of the inference space. We finally demonstrate the feasibility of the method with an implementation that uses robust reachability oracles to generate constraints on standard benchmarks from software verification and security analysis, and its practical ability to refine the notion of robust reachability. We illustrate the use of our implementation to a vulnerability characterization problem in the context of fault injection attacks. Our method overcomes a major limitation of the initial proposal of robust reachability, without complicating its definition. From a practical view, this is a step toward new verification tools that are able to characterize program violations through high-level feedback.
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 16 | |
| downloads | 1 |

Views provided by UsageCounts
Downloads provided by UsageCounts