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.
Notes related to Under-constrained execution: Making automatic code destruction easy and scalable
Papers related to Under-constrained execution: Making automatic code destruction easy and scalable
- 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]