Introducing robust reachability

We introduce a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the value of uncontrolled input. Robust reachability is b...

Full description

Saved in:
Bibliographic Details
Published in:Formal methods in system design 2024, Vol.63 (1-3), p.206-234
Main Authors: Girol, Guillaume, Farinier, Benjamin, Bardin, Sébastien
Format: Article
Language:English
Subjects:
CAE) and Design
Circuits and Systems
Computer Science
Computer-Aided Engineering (CAD
Electrical Engineering
Engineering
Engineering Sciences
Robust control
Software engineering
Software Engineering/Programming and Operating Systems
Software testing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We introduce a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the value of uncontrolled input. Robust reachability is better suited than standard reachability in many realistic situations related to security (e.g., criticality assessment or bug prioritization) or software engineering (e.g., replicable test suites and flakiness). We propose a formal treatment of the concept, and we revisit existing symbolic bug finding methods through this new lens. Remarkably, robust reachability allows differentiating bounded model checking from symbolic execution while they have the same deductive power in the standard case. Finally, we propose the first symbolic verifier dedicated to robust reachability: we use it for criticality assessment of 5 existing vulnerabilities, and compare it with standard symbolic execution.
ISSN:0925-9856
1572-8102
DOI:10.1007/s10703-022-00402-x