problem with constraints

[bejab2020]

hi

i want to generate some vulnerability constraints in simprocedures,for example in strcpy:

class strcpy(angr.SimProcedure):
    #pylint:disable=arguments-differ

    def run(self, dst, src):
        strlen = angr.SIM_PROCEDURES['libc']['strlen']
        strncpy = angr.SIM_PROCEDURES['libc']['strncpy']
        src_len = self.inline_call(strlen, src)
	dst_len = self.inline_call(strlen, dst)

	vul_const = claripy.UGT(src_len,dst_len)
	self.state.globals['const'].append(vul_const)

        ret_expr = self.inline_call(strncpy, dst, src, src_len.ret_expr+1, src_len=src_len.ret_expr).ret_expr
        return ret_expr

can I do this? if I do this is it affect the result of the solver for generating string with a greater size than dst for src?
and i also tried other ways but solver generate some symbols and constraints like <Bool 0x7fffffffffeff88 + strlen_22_64[63:59] == 0> that at the end solver gaves me unsat result.

is there any way that I can generate this kind of constraints for vulnerabilities?

[rhelmot]

So, good news bad news:

The good news is that you can in fact do that and everything will be fine.

The bad news is that that's not a condition which will allow you to detect a vulnerability. The thing you need to compare against is the size of the buffer, which is not the same as the strlen of the buffer. You'll need to use static analysis in order to determine what the actual buffer size is.

[bejab2020]

thanks for the response

consder i have the size of buffer and i run the progran then i collect the constraints and in the strcpy i store src_len
at the end:

con=simgr.deadended[2].solver.constraints // target path 
ex=simgr.deadended[2].globals['extra_const_symb'][0] // src_len in _vul_strcpy
s=claripy.Solver()
s.add(con)
s.add(ex > 50) // the size is 40 for bof i set it to 50
castTO(var_3,s.eval(var_3,1)[0],cast_to=bytes) 

I get unsat result.
I found that in the strlen some constraints added to the state and these constraints is the reason. for example, one reason is adding this constraint:

 <Bool 0x1 + strlen_16_64[63:5] == 0x0>,

if I ignore strlen with exclude_sim_procedures_list it runs again.
is there any way that I can handle this?

[rhelmot]

That constraint is just the way that strlen specifies its return value - it will always provide a new symbol as a return value and just constrain it to be whatever expression it computes as the length. However... that particular constraint looks really weird. It's either not actually the constraint I was just talking about, or it's been mutated badly by z3 simplifications. I think at this point your best bet is to step through the strlen code in a debugger to determine why each constraint is being generated and whether it makes sense?

[bejab2020]

I think the problem was the value of state.libc.buf_symbolic_bytes which was the argument of memory.find function,when i increased it the constraint turns into :

<Bool 0x1 + strlen_66_64[63:8] == 0x0>

and the state is satisfiable and my problem is solved.

Thanks.