Implement slice/slicing

[0ca]

Original definition:

identifying all program code that can in any way affect the value of a given variable
This is now called “static backward slicing”

More info: http://web.cs.iastate.edu/~weile/cs513x/5.TaintAnalysis2.pdf

The idea is from an instruction get all the previous instructions that modified the values used in the current instr.

This is very useful for exploiting. If you found an input is crashing a program via fuzzing, and you want to know where comes from the values from the registers, memory, you could use that.

They implemented in the past something similar in this paper. But they never released a fully functional version: https://media.blackhat.com/us-13/US-13-Li-How-to-Grow-a-TREE-Slides.pdf They show the previous functions involved in the tainting.

[0ca]

In semtrax they call this Up-graph and it can be seen here: https://vimeo.com/119980186

The idea is to see with instructions modified the taint input.

They also implement down-graph. Starting with a taint input, like argv[0] see how this value in use along the program.

[pfsun]

Hi @0ca, I was wondering how is going for slicing?

[0ca]

Hi @pfsun, right now we are not dedicating too much time to Ponce, we are working in parallel projects.

But this functionality should be easy to code, I will try to do it in the next weeks ;)

[JonathanSalwan]

But this functionality should be easy to code, I will try to do it in the next weeks ;)

API::sliceExpressions =).

[0ca]

Thanks!

[pfsun]

Thanks:-)

[pfsun]

@JonathanSalwan I just the sliceExpressions API. It seems the output will not be the backwards sequence, right? For example, the expression is :Expression: ref!62385 = ((_ zero_extend 0) (bvadd ((_ extract 127 0) ref!62381) ((_ extract 127 0) ref!62375))) ; ADDSD operation The Slice result is :{57843L: ref!57843 = ((_ extract 55 48) ((_ extract 127 0) ref!57834)) ; Byte reference - MOVSD operation, 45299L: ref!45299 = ((_ extract 7 0) ((_ extract 63 0) ref!45288)) ; Byte reference - MOV operation, 62381L: ref!62381 = ((_ zero_extend 64) (concat ((_ extract 7 0) (_ bv63 8)) ((_ extract 7 0) (_ bv169 8)) ((_ extract 7 0) (_ bv153 8)) ((_ extract 7 0) (_ bv153 8)) ((_ extract 7 0) (_ bv153 8)) ((_ extract 7 0) (_ bv153 8)) ((_ extract 7 0) (_ bv153 8)) ((_ extract 7 0) (_ bv154 8)))) ; MOVSD operation, 57689L: ref!57689 = ((_ extract 15 8) ((_ extract 63 0) ref!57681)) ; Byte reference - MOV operation, 57558L: ref!57558 = ((_ extract 7 0) ((_ extract 63 0) ref!57549)) ; Byte reference - MOV operation, 62385L: ref!62385 = ((_ zero_extend 0) (bvadd ((_ extract 127 0) ref!62381) ((_ extract 127 0) ref!62375))) ; ADDSD operation, 44611L: ref!44611 = ((_ zero_extend 0) (concat ((_ extract 7 0) ref!44360) ((_ extract 7 0) ref!44361) ((_ extract 7 0) ref!44362) ((_ extract 7 0) ref!44363) ((_ extract 7 0) ref!44364) ((_ extract 7 0) ref!44365) ((_ extract 7 0) ref!44366) ((_ extract 7 0) ref!44367))) ; MOV operation,.........

[JonathanSalwan]

why it's not?