Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design

21-11-2022

Introducing robust reachability

Authors: Guillaume Girol, Benjamin Farinier, Sébastien Bardin

Published in: Formal Methods in System Design

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
2
We need to handle the case where the considered trace t is not in O, but one of its prefix is – which indeed satisfies reachability. Yet, in the cases where O is upward-closed (i.@e.@, closed by extension of trace) or \({\texttt {GetPaths}}(k)\) returns all path prefixes (and not only maximal paths), \({{\,\textrm{mon}\,}}_\pi ^O\) simply needs to express that \(t \in O\).
 
3
Without a null byte, but we ignore this detail for the sake of simplicity.
 
Literature
1.
2.
Avgerinos T, Cha SK, Rebert A, Schwartz EJ, Woo M, Brumley D (2014) Automatic exploit generation. Communicat ACM 57(2):74–84CrossRef
3.
Aziz A, Sanwal K, Singhal V, Brayton R (1996) Verifying continuous time Markov chains. In: CAV. Springer
4.
Baldoni R, Coppa E, D’elia DC, Demetrescu C, Finocchi I (2018) A Survey of Symbolic Execution Techniques. ACM Comput Survey 51(3):1–39CrossRef
5.
Barret CW, Sebastiani R, Seshia SA, Tinelli C (2009) Satisfiability Modulo Theories. In: Handbook of Satisfiability. Ios press edn
6.
Barrett C, Conway CL, Deters M, Hadarean L, Jovanović D, King T, Reynolds A, Tinelli C (2011) CVC4. In: CAV. Springer
7.
Barthe G, D’Argenio P, Rezk T (2004) Secure information flow by self-composition. In CSF’04 Workshop
8.
Bradley AR, Manna Z, Sipma HB (2005) What’s Decidable About Arrays? In VMCAI. Springer
9.
Brillout A, Kroening D, Rümmer P, Wahl T (2011) Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. In VMCAI. Springer
10.
Cadar C, Sen K (2013) Symbolic execution for software testing: three decades later. Communicat ACM 56(2):82–90CrossRef
11.
Cha SK, Avgerinos T, Rebert A, Brumley D (2012) Unleashing mayhem on binary Code. In S &P 2012
12.
Chakraborty S, Meel K, Mistry R, Vardi M (2016) approximate probabilistic inference via Word-Level counting. AAAI 30(1)
13.
Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NuSMV: a new Symbolic Model Verifier. In CAV’99. Springer
14.
Clarke E, Kroening D, Lerda F (2004) A Tool for Checking ANSI-C Programs. In TACAS. Springer
15.
Clarke EM, Emerson EA (1982) Design and synthesis of synchronization skeletons using branching time temporal logic. In Logics of Programs. Springer
16.
Clarkson MR, Finkbeiner B, Koleini M, Micinski KK, Rabe MN, Sánchez C (2014) Temporal logics for hyperproperties. In principles of security and trust. Springer
17.
Clarkson MR, Schneider FB (2010) Hyperproperties. J Comput Secur 18(6):1157–1210CrossRef
18.
Cook B, Podelski A, Rybalchenko A (2006) Terminator: Beyond Safety. In: CAV. Springer
19.
Cowan C, Pu C, Maier D, Walpole J, Bakke P, Beattie S, Grier A, Wagle P, Zhang Q, Hinton H (1998) StackGuard: Automatic adaptive detection and prevention of buffer-overflow attacks. In USENIX Security
20.
Daniel LA, Bardin S, Rezk T (2020) Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level. In S &P 2020. IEEE
21.
David R, Bardin S, Ta TD, Mounier L, Feist J, Potet ML, Marion JY (2016) BINSEC/SE: A dynamic symbolic Execution toolkit for binary-level analysis. In SANER 2016. IEEE
22.
David R, Bardin S, Feist J, Mounier L, Potet ML, Ta TD, Marion JY (2016) Specification of concretization and symbolization policies in symbolic execution. In ISSTA 2016. ACM
23.
de Moura L, Bjørner N (2008) Z3: An Efficient SMT Solver. In TACAS. Springer
24.
Djoudi A, Bardin S (2015) BINSEC: Binary code analysis with low-level regions. In: TACAS. Springer
25.
Farinier B (2020) Decision Procedures for Vulnerability Analysis. Ph.D. thesis, Université Grenoble-Alpes
26.
Farinier B, Bardin S, Bonichon R, Potet ML (2018) Model generation for quantified formulas: a taint-based approach. In CAV. Springer
27.
Farinier B, David R, Bardin S, Lemerre M (2018) Arrays made simpler: an efficient, scalable and thorough Preprocessing. In LPAR-22
28.
Ge Y, de Moura L (2009) Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In CAV. Springer
29.
Girol G, Farinier B, Bardin, S (2021) Not all bugs are created equal, but robust reachability can tell the difference. In CAV ’21. Springer
30.
Godefroid P (2011) Higher-order test generation. In PLDI ’11. ACM
31.
Godefroid P, Klarlund N, Sen K (2005) DART: directed automated random testing. In PLDI 2005. ACM
32.
Godefroid P, Levin MY, Molnar D (2012) SAGE: Whitebox fuzzing for security testing: SAGE has had a remarkable impact at Microsoft. Queue 10(1):20–27CrossRef
33.
Goguen JA, Meseguer J (1982) Security Policies and Security Models. In S &P 1982. IEEE
34.
Gomes CP, Sabharwal A, Selman B (2008) Model Counting. In Handbook of Satisfiability. Ios press edn
35.
Hansen T, Schachte P, Søndergaard H (2009) State Joining and Splitting for the Symbolic Execution of Binaries. In Runtime Verification. Springer
36.
Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Formal Aspects o Comput 6(5):512–535CrossRefMATH
37.
Hart S, Sharir M, Pnueli A (1983) Termination of Probabilistic Concurrent Program. ACM Transact Program Lang Syst 5(3):356–380CrossRefMATH
38.
Heelan S (2009) Automatic generation of control flow hijacking exploits for software vulnerabilities. Master’s thesis, University of Oxford
39.
Heusser J, Malacaria P (2010) Quantifying information leaks in software. In ACSAC ’10. ACM Press
40.
Holler C, Herzig K, Zeller A (2012) Fuzzing with code fragments. In 21st USENIX security symposium. USENIX Association
41.
Kim S, McCamant S (2018) Bit-vector Model counting using statistical estimation. In TACAS. Springer
42.
Kurpiewski D, Knapik M, Jamroga W (2019) On Domination and Control in Strategic Ability. AAMAS .9
43.
Laroussinie F, Meyer A, Petonnet E (2010) Counting CTL. In: Foundations of Software Science and Computational Structures. pp. 206–220. Lecture Notes in Computer Science
44.
Livshits B, Sridharan M, Smaragdakis Y, Lhoták O, Amaral JN, Chang BYE, Guyer SZ, Khedker UP, Møller A, Vardoulakis D (2015) In defense of soundiness: A manifesto. Communicat ACM 58(2):44–46CrossRef
45.
de Moura L, Bjørner N (2007) Efficient E-Matching for SMT Solvers. In Automated Deduction - CADE-21. Springer
46.
Niemetz A, Preiner M, Biere A (2015) Boolector 2.0: System description. J Satisf Boolean Modeling Comput 9(1)
47.
O’Hearn PW (2020) Incorrectness logic. POPL.4:1–32
48.
Recoules F, Bardin S, Bonichon R, Mounier L, Potet ML (2019) Get Rid of Inline assembly through verification-oriented lifting. In ASE 2019. IEEE
49.
Reynolds A, Tinelli C, Goel A, Krstić S (2013) Finite model finding in SMT. In CAV. Springer
50.
Sen K, Marinov D, Agha G (2005) CUTE: a concolic unit testing engine for C. In ESEC/FSE-13. ACM
51.
Shoshitaishvili Y, Wang R, Salls C, Stephens N, Polino M, Dutcher A, Grosen J, Feng S, Hauser C, Kruegel C, Vigna G (2016) SOK: (State of) The art of war: Offensive techniques in binary analysis. In: SP 2016
52.
53.
Urban C, Miné A (2017) Inference of ranking functions for proving temporal properties by abstract interpretation. Comput Lang Syst Struct 47:77–103MATH
54.
Urban C, Ueltschi S, Müller P (2018) Abstract interpretation of CTL properties. In SAS 2018. Springer
55.
Williams N, Marre B, Mouy P, Roger M (2005) Pathcrawler: Automatic generation of path tests by combining static and dynamic analysis. In EDCC-05. Springer
Metadata
Title
Introducing robust reachability
Authors
Guillaume Girol
Benjamin Farinier
Sébastien Bardin
Publication date
21-11-2022
Publisher
Springer US
Published in
Formal Methods in System Design
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-022-00402-x

Premium Partner

    Image Credits