From 758ebb324340e9981ab12d4b3d3432fc6af3b983 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 7 Nov 2017 16:32:13 +0000
Subject: [PATCH 1/2] transfer taint on memcpy and memmove

---
 .../taint-memcpy1/main.c                         |  15 +++++++++++++++
 .../taint-memcpy1/main.o                         | Bin 0 -> 5637 bytes
 .../taint-memcpy1/taint.json                     |   4 ++++
 .../taint-memcpy1/test.desc                      |   7 +++++++
 src/analyses/custom_bitvector_analysis.cpp       |  13 +++++++++++++
 5 files changed, 39 insertions(+)
 create mode 100644 regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.c
 create mode 100644 regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.o
 create mode 100644 regression/goto-analyzer-taint-ansi-c/taint-memcpy1/taint.json
 create mode 100644 regression/goto-analyzer-taint-ansi-c/taint-memcpy1/test.desc

diff --git a/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.c b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.c
new file mode 100644
index 00000000000..806b14fa2b4
--- /dev/null
+++ b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.c
@@ -0,0 +1,15 @@
+#include <string.h>
+
+void my_f(void *) { }
+void my_h(void *) { }
+
+void my_function()
+{
+  void *o1;
+  my_f(o1); // T1 source
+
+  void *o2;
+  memcpy(o2, o1, 100);
+
+  my_h(o2); // T1 sink
+}
diff --git a/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.o b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/main.o
new file mode 100644
index 0000000000000000000000000000000000000000..566d8da99a72e7df83eeb8264b5ef93737bea913
GIT binary patch
literal 5637
zcmbtYdwdkt6~1?u1u{fdjja;IqM=$_Lb4$uq;^XkP}|bcGF9t?j+5Ql?8xp+oSiiU
zYZb88`e@Z!Tk%QdO@KsR0*Yu!L`Z<PQd<!e`?3`gt@Y2^@64T@9iWSUm>>C(o!R?+
z-}&x2=bo9{F1`4Y=vY>pveO1rKH-kx79C4-JKGJ$hZf8>%SgB0%#=mE!%Vwb7I`Z&
zzKJn;<Dj~f_*V4si1?ajS}wz_IlRuaQg*&QXSfC%v_F!-)mX$bb4-bPz=Lst4PnZu
z88c_Fp)V!#x@nC|F{aeyOv_+Zk4lL~d>WA{S}E7GEhhCP^PO7oktzFP9kw&mwA!?^
z=@=>3b~@RxIa0%w1;Z&c%yewS!p(+u$8K{PQmy$^eVgevI7XXe6be9WXtQ0rUbpmI
z=WN5NcOk&V$AVd(Y7igtMn2WvN!oWN#ougzlTdu#8<i=9>TJ7>b%w*#lO`MacDIws
z@w$RtbW(<vvs1dKeK-Ogs?@|EktR`060{G)AB*_O2O|@jVOV@Piw)lq4zQ&q(b8f!
zf$)_i{@WYfkz`{}$*QMLmg6-7?zD%b3CF<Ey;#lm<AD+YdO2w)0JI%IpR2`2e;!b$
z3#c>hksw1EG1ymjAlj}wdLFyy6xax+ycaQYIkUZB7T6%DJ)PCQouvK6=A{`sy)QYy
z`(R05l8qio&}RaAlz=|#4hh*3hW-LmN6+U00aD`Zta>K7L5uJ!FW_~pdcn{vNMPse
zOV;U@Z6O`x`=WJb+OS+RW5V*f{S;`nrKNPAoE*h!NA-Hw5ppj?^+ME`p@5IbcSq||
zwpDO-r0F0eaFl&<YH&e`a%IZRdah`&bDvE%p7;kzA;-@{gkM^myr{Kk=3LXN*PT?>
zbdich$EYv34$`lXMC>)^cS}uJ;h8J%6v447cHY*crpZ@Kzx=AH)3xwoO}TQ~G|en%
zNK6}HY(*GbldSQ}S@kOv$=Cyti4bsil!B;#Fp|pZ4w6w=IF3{)H4UqzCaNGW)f%^R
zJ)Ne+*X#^a6QfNlZOme7(?TwEY9SlO8@l7@olI@^xQK!&nSwdnU>8hPq7&%q$+&vq
zlcloH*{DKM`^uDwFMOJLpJFW)K7>!1bi0(-Q+9!@9w+bMbvdy+gP7VvI+Q72ef_gh
zK?pHLoAG;5R&A!h7#p{x(zZa$0N;Ym*n-XY8a6{Xo)nIMy-P|^eS3~i-p<u;j8-pR
z$d#yU06H^8XrB7~XVaWWP(y+}mwZw+YvKe=^p7O`Az%DhSaNfv7%0yW#b!jY8BvV6
z6ta-`=gRTRL>S*(E+vp%rDUyQmu;$qWmsubw=AR;5H|sF6Cr*}Ab$JN>Jx5sg3OoW
z(*)~xmP&~W!>rRbR$@gfMz7cGcEi!FwB{w|0N)7ujYO{m0bMSjuXr<(phijig6gYc
zmv5*9t><vu<<Vde&jtW)Ai(bm!07|h3FGmSNsg<6^m~h>#06neb$un$j5*6lYZ=?o
zGC5l(>h+*rPt;fX)N=eP0ekfVDKS0_d)3-Xu+$W&hZJ$7(HRchwZL6VxZfAJ*Q`0I
zVo2B?`k^hlR&ZC99lW-?5^LHnw&n~?j0yw18;spxye_L=KUt2?01^(uL83-P^~_+g
z8E<$eR?x@?_&%&-tZVR?ANWe;xF%HG@UV1Lo@gs8N%6W;sWk<PRswk?d7umA)}@s_
zK>TC_d5{w9>HDRlb~Ux461!)A$%YjmT|uNq5Kcw_w%sKiwV#<~l>m>6WEnu05olI`
zn%yUeL~JKTa-$#?d*Ic>jY}$VqNfMOEdkvUqMIq`rps}Rb9B_?pOz9dJ_H4pTUQCN
z!?VRbCNI|kdL5v-6+qj7Zl5cOv$dWM*L2#XVM?5+H?1Bv;ix8McMmI{rH)-hXTq73
zr<oR6I1E`hj7=Ql_)f|3f{=bzS#)7(MbWksw3(%lx)f5~SgUR47%N_A*{*R@QO_~;
z=0JT1saI-d{ab22DqYl0|0^^H%kd7@@sU)Po!4_18Oa;V=)gcghwuRZNZK3yNMen%
zt4ftDrg2P5w+I@4E9XS&Xtqup8TP|@Ay{gV8s>5w*|$CwDS==*4G!(tj|9+dA4tum
zjr=f#;0yCR?S~NbAq3sdv+5j<s-DZm@_GDysX54IOeg+Cg8O%H1b#ctnIH2vIZZb>
z!shZL$8*@NH)4Q7*hj!}1T1%g<tM~)m(TK3{;t#<OjBhR+`pSx?(|sLUHni8J#Bd2
z>aN!Z4*~lSu<rr(y@Y+AkNq?LAE`MwE6Uio|8v5=M_}K_KMrC0=TXkkXF~VK!2TH6
zWA3K~_<pM#e}LdoC})(j?E${LQo2!M1y#2k`L-PS_8_OZ`g-L+^cS3|5Ape!E3QLB
z#jJb|#^PV{H!x|Ux@WN38QZ*W3N72PcpJvw*|A&ZNdtTyq|KAqy;~y>b3^?VuR;SJ
zi>&xHf2^DqrCBob2>&lPt&C}zc&Nd+CCBIcE<MWMlE#;+51hCjo6ip(X9*M>1m!`A
zHH~@9cjIxs@&sMVYqws%eZsfww6bMS@UBXh6|%O2rV{E_T?oC4y490Du_?!&@-gFO
z%%}M3ikN61p_6Pi09ONWfoB`dzqhjA@R3w;DZSt_^=Y37eQ}|0)FQr98Xu%8jUGyL
z0cQ(&f5<C0>lk`kGwFcthh6;=o4D8`iGXAYf1<oMV#Hp`N2<%pWXpZB6?{>3qVX8E
z#hfkYi>u2$rrm5eFzgq-5odAr-ss|L*4TwQSV?uT%EwyG-;<i@vCV7g<vPIqZes2d
zb+C#b4h4c5OKU;>9!4mKQ3q$oM(xMrVQ`@L_{y)5<Ini}F}A!P&+t{1_QQYB4k}|6
zHe?m;@ERX+Eq|usXzfokUTUrLY1i||B^sv7?CW?>C3de{9y8qZKtT@_Y(O=+O6FM<
zj8`WceHSAhG71D2VjKCckXK^U3z{(t4~(?)yI|KY*tN;4^Ubsw&-pOV^Yv0wsVy^f
zfWh9q*mHbC2$Aa4#Qch<G|a9*+aR&gTl_r24tlx7VlVih=X=_ELI9;FK$MXvdaX$L
zHo$uT)<Yd_t8X+)=|$hem-v%XB1ja<@E7@-N*<OD|I$>n2L7$_O6s>r>1{qb>ZjKi
z*~fQF<AVbwsGnZGC#2glX1Q9pi1tA59_WqI`yv*3nMc^R<c!#M!grM^ukb$ZI(W**
z&nNhaGqwY!M|bjCrp)D`_Y3`KpbTpVNRBtQj_Bu}Z&llQX)V2hAd=qXC{UEH?h=T=
z+l@Pn^(OcDAZIBfcK<(+;LX<1-|<@Y_k2>JGvA5{Ly4XOls|C1w(;KlK&NssUSYU~
z_nh)7zcg*6Fo@92zGThtvWC6Dd6}z!<dc->gB&3JT#moy%ebNR8cIAk{)wk`r>#hk
z1*ZO)mIzu};e7={i1~G{my~KLoT)?%%)aDn{NytAK2X0wAl0DV&++bxUU3P8SD|7!
z77PzbJs_mMNlR!G-r_rH$q=R<<Z1QoG7_!{!G8%$^soKZ&!E5Y{)&yDF@aWqf24be
zH~j{I5no?&NGOcI3t9glu91+n8`9tL4Sb0o?chHl^j~42?;PWsx3n+$PS~e+L2#(N
v$d~dSzl?e*Nj&VcU0ouB!oxgXcKUrF94UJdAb3lU`R)fnQc507D2x9GlzDCc

literal 0
HcmV?d00001

diff --git a/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/taint.json b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/taint.json
new file mode 100644
index 00000000000..44a841f0cc4
--- /dev/null
+++ b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/taint.json
@@ -0,0 +1,4 @@
+[
+{ "id": "my_f", "kind": "source", "where": "parameter1", "taint": "T1", "function": "my_f" },
+{ "id": "my_h", "kind": "sink",   "where": "parameter1", "taint": "T1", "function": "my_h", "message": "There is a T1 flow" }
+]
diff --git a/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/test.desc b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/test.desc
new file mode 100644
index 00000000000..af2d62eb456
--- /dev/null
+++ b/regression/goto-analyzer-taint-ansi-c/taint-memcpy1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.o
+--taint taint.json
+^EXIT=0$
+^SIGNAL=0$
+^file main.c line 12( function .*)?: There is a T1 flow \(taint rule my_h\)$
+--
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index a0d835dd865..906365b97a8 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -380,6 +380,19 @@ void custom_bitvector_domaint::transform(
             }
           }
         }
+        else if(identifier=="memcpy" ||
+                identifier=="memmove")
+        {
+          if(code_function_call.arguments().size()==3)
+          {
+            // we copy all tracked bits from op1 to op0
+            // we do not consider any bits attached to the size op2
+            dereference_exprt lhs_deref(code_function_call.arguments()[0]);
+            dereference_exprt rhs_deref(code_function_call.arguments()[1]);
+
+            assign_struct_rec(from, lhs_deref, rhs_deref, cba, ns);
+          }
+        }
         else
         {
           goto_programt::const_targett next=from;

From fa7d62a554cf0bb22d12c2a47efe8a1732aad611 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Fri, 10 Nov 2017 14:33:13 +0000
Subject: [PATCH 2/2] Makefile for goto-analyzer-taint-ansi-c

---
 .../goto-analyzer-taint-ansi-c/Makefile       | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 regression/goto-analyzer-taint-ansi-c/Makefile

diff --git a/regression/goto-analyzer-taint-ansi-c/Makefile b/regression/goto-analyzer-taint-ansi-c/Makefile
new file mode 100644
index 00000000000..462e051669c
--- /dev/null
+++ b/regression/goto-analyzer-taint-ansi-c/Makefile
@@ -0,0 +1,19 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log