Under-constrained execution: Making automatic code destruction easy and scalable

Dawson Engler, Daniel Dunbar
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 18 April 2021

Proceedings of the 2007 International Symposium on Software Testing and Analysis
ISSTA '07
London, United Kingdom
Association for Computing Machinery
New York, NY, USA
Pages 1-4
2007
Note(s): EXE verifier, lazy initialization
Papers: calcagno:popl:2009, ramos:sec:2015, khurshid:tacas:2003, xie:popl:2005

Extends the EXE verifier with support for under-constrained variables. Any errors detected by symbolic execution are only reported if the path condition does not depend on the value of an under-constrained variable. For example, if a pointer is dereferenced, we add a constraint that the pointer is non-null and a new under-constrained variable is created for the value read. This idea apparently originates in Java PathFinder (JPF) (khurshid:tacas:2003, xie:popl:2005).

I’m not clear how this is different from abduction (calcagno:popl:2009) which seems to operate in a similar way.

Under-constrained variables are used for function inputs to let us infer function preconditions for each path executed avoiding the need to specify the precondition explicitly.

Under-constrained variables can also be used when a function calls an external function: a symbolic unconstrained return value is created.

This approach allowed them to analyze a lot of Linux device drivers relatively easily.

One tricky detail is that they track under-constrained variables through a form of taint-tracking. The subtle thing is that if you compare a normal “exactly-constrained” variable ‘s’ against an under-constrained variable ‘u’, then ‘s’ gains a constraint that depends on ‘u’ so ‘s’ is now also under-constrained. That is, we can’t use a conventional taint tracking but, instead have to consider an equivalence class of all variables that are transitively related to any under-constrained variable.

EXE symbolic executor, Lazy initialization of symbolic values

  • Generalized symbolic execution for model checking and testing [khurshid:tacas:2003]
  • Practical, low-effort equivalence verification of real code [ramos:cav:2011]
  • Under-constrained symbolic execution: Correctness checking for real code [ramos:sec:2015]
  • Scalable error detection using boolean satisfiability [xie:popl:2005]