search

trailofbits / binary_type_inference

GNU General Public License v3.0
12 stars 0 forks source link

Transitivity not propagating across S-Pointer rules. #14

Closed 2over12 closed 2 years ago

2over12 commented 2 years ago 
a <= x.store
x.load <= c

Pretty obviously we should get a <= c here.

Formally S-Pointer gives us x.store <= x.load Trans of (a <= x.store , x.store <= x.load) gives us a <= x.load Trans of (a <= x.load, x.load <= c) gives us a <= c

This proof breaks down in our proof graph. This is related to the variance of stacks. We have to be careful to not break #6 while fixing this portion of the proof graph.

graphviz

The trick is a should have an edge to x cov store which would then get everything to work out. But this edge was removed in #6

2over12 commented 2 years ago

Turns out this is related to #6. a should have an edge to covariant x.store the original fix for #6 was incorrect.