Skip to content

Commit 758ebb3

Browse files
author
Daniel Kroening
committed
transfer taint on memcpy and memmove
1 parent 5be97db commit 758ebb3

File tree

5 files changed

+39
-0
lines changed

5 files changed

+39
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <string.h>
2+
3+
void my_f(void *) { }
4+
void my_h(void *) { }
5+
6+
void my_function()
7+
{
8+
void *o1;
9+
my_f(o1); // T1 source
10+
11+
void *o2;
12+
memcpy(o2, o1, 100);
13+
14+
my_h(o2); // T1 sink
15+
}
Binary file not shown.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
[
2+
{ "id": "my_f", "kind": "source", "where": "parameter1", "taint": "T1", "function": "my_f" },
3+
{ "id": "my_h", "kind": "sink", "where": "parameter1", "taint": "T1", "function": "my_h", "message": "There is a T1 flow" }
4+
]
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.o
3+
--taint taint.json
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^file main.c line 12( function .*)?: There is a T1 flow \(taint rule my_h\)$
7+
--

src/analyses/custom_bitvector_analysis.cpp

+13
Original file line numberDiff line numberDiff line change
@@ -380,6 +380,19 @@ void custom_bitvector_domaint::transform(
380380
}
381381
}
382382
}
383+
else if(identifier=="memcpy" ||
384+
identifier=="memmove")
385+
{
386+
if(code_function_call.arguments().size()==3)
387+
{
388+
// we copy all tracked bits from op1 to op0
389+
// we do not consider any bits attached to the size op2
390+
dereference_exprt lhs_deref(code_function_call.arguments()[0]);
391+
dereference_exprt rhs_deref(code_function_call.arguments()[1]);
392+
393+
assign_struct_rec(from, lhs_deref, rhs_deref, cba, ns);
394+
}
395+
}
383396
else
384397
{
385398
goto_programt::const_targett next=from;

0 commit comments

Comments
 (0)