search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
335 stars 62 forks source link

UAF causing intermittent crashes #67

Closed cdisselkoen closed 4 years ago

cdisselkoen commented 5 years ago

I'm experiencing intermittent crashes which I've been trying to track down more precisely for a while. I believe I've pinpointed it as a UAF in Boolector, but I could still be wrong - among other things, I'm not very familiar with the Boolector codebase.

Specifically I believe the culprit to be btor_node_create_bv_const in btornode.c. I'm looking at the case where the lookup fails such that we end up calling new_const_exp_node. Somehow (I'm not sure) the node returned from new_const_exp_node may have a .next field which refers to some other node, but without recording that it has a ref to that other node. Let the const node be Node A, and the .next node on Node A be Node B. What I believe I'm observing in my crash traces is a case where the external caller uses boolector_release on Node B with the result that it's freed, but later operations (e.g. boolector_sat) still have a pointer to the now-freed Node B through Node A ->next.

I'm guessing this UAF doesn't usually manifest as a problem because the memory isn't reused for anything, so the Node B data stays valid enough for things to work. In my case, I have a multithreaded program where different threads are working on different Boolector instances; but these threads still naturally share the same allocator. So other threads have a timing window to come in and reallocate something else at Node B's address, and this is what I believe is causing my intermittent crashes.

I'm happy to keep digging, and I realize I very much could be wrong about the root cause here, especially as I'm not positive what internal invariants Boolector maintains around when refcounts are supposed to be inc'd and dec'd.

mpreiner commented 5 years ago

@cdisselkoen here is some more information what the next pointer is actually for:

next points to the next node in the collision chain of the unique node hash table. So let's say you create node A, and afterwards node B and they happen to have the same hash value, you would get a collision chain like ... -> A -> B -> ..., i.e., A->next = B and B->next = .... If node B gets released, it gets removed from the collision chain and the list is updated accordingly, i.e., A->next = B->next, so A->next should not point to an invalid node. This happens in function remove_from_nodes_unique_table_exp.

mpreiner commented 5 years ago

@cdisselkoen any news on this issue?

cdisselkoen commented 5 years ago

Sorry for going silent there. I worked around the issue by removing the offending boolector_release operations, and instead just relying on boolector_release_all when done with a Btor instance.