{"id":1137,"date":"2023-11-13T12:53:33","date_gmt":"2023-11-13T03:53:33","guid":{"rendered":"https:\/\/h4ck.kr\/?p=1137"},"modified":"2023-11-13T13:16:18","modified_gmt":"2023-11-13T04:16:18","slug":"klee-%eb%91%90%eb%b2%88%ec%a7%b8-%ed%8a%9c%ed%86%a0%eb%a6%ac%ec%96%bc-%ea%b0%84%eb%8b%a8%ed%95%9c-%ec%a0%95%ea%b7%9c-%ed%91%9c%ed%98%84%ec%8b%9d-%eb%9d%bc%ec%9d%b4%eb%b8%8c%eb%9f%ac%eb%a6%ac%eb%a5%bc","status":"publish","type":"post","link":"https:\/\/h4ck.kr\/?p=1137","title":{"rendered":"KLEE \ub450\ubc88\uc9f8 \ud29c\ud1a0\ub9ac\uc5bc: \uac04\ub2e8\ud55c \uc815\uaddc \ud45c\ud604\uc2dd \ub77c\uc774\ube0c\ub7ec\ub9ac\ub97c \ud14c\uc2a4\ud2b8\ud574\ubcf4\uae30"},"content":{"rendered":"\n

\uc774\uac83\uc740 \uac04\ub2e8\ud55c \uc815\uaddc \ud45c\ud604\uc2dd \uc77c\uce58 \ud568\uc218\ub97c \ud14c\uc2a4\ud2b8\ud558\uae30 \uc704\ud574 KLEE\ub97c \uc0ac\uc6a9\ud558\ub294 \uc608\uc81c\uc774\ub2e4.
\uc18c\uc2a4 \ud2b8\ub9ac\uc5d0\uc11c examples\/regexp<\/strong>\uc5d0 \uae30\ubcf8 \uc608\uc81c\ub97c \ucc3e\uc744 \uc218 \uc788\ub2e4.<\/p>\n\n\n\n

Regexp.c<\/strong>\uc5d0\ub294 \uac04\ub2e8\ud55c \uc815\uaddc \ud45c\ud604\uc2dd \uc77c\uce58 \ud568\uc218\uc640 KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec
\uc774 \ucf54\ub4dc\ub97c \ud0d0\uc0c9\ud558\uae30 \uc704\ud574 \ud544\uc694\ud55c \uae30\ubcf8 \ud14c\uc2a4\ud2b8 \ud558\ub124\uc2a4(main()<\/strong>)\uac00 \ud3ec\ud568\ub418\uc5b4 \uc788\ub2e4.
\uc18c\uc2a4 \ucf54\ub4dc\uc758 \ubc84\uc804\uc744 \uc5ec\uae30\uc11c<\/a> \ubcfc \uc218 \uc788\ub2e4.<\/p>\n\n\n\n

\uc774 \uc608\uc81c\ub294 KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec \uc608\uc81c\ub97c \ube4c\ub4dc\ud558\uace0 \uc2e4\ud589\ud558\ub294 \ubc29\ubc95,
\uadf8\ub9ac\uace0 \ucd9c\ub825\uc744 \ud574\uc11d\ud558\ub294 \ubc29\ubc95\uacfc \ud14c\uc2a4\ud2b8 \ub4dc\ub77c\uc774\ubc84\ub97c \uc218\ub3d9\uc73c\ub85c \uc791\uc131\ud560 \ub54c \uc0ac\uc6a9\ud560 \uc218 \uc788\ub294 \uba87 \uac00\uc9c0 \ucd94\uac00\ub41c KLEE \uae30\ub2a5\uc744 \ubcf4\uc5ec\uc900\ub2e4.<\/p>\n\n\n\n

\uba3c\uc800 \uc608\uc81c\ub97c \ube4c\ub4dc\ud558\uace0 \uc2e4\ud589\ud558\ub294 \ubc29\ubc95,
\uadf8\ub9ac\uace0 \ud14c\uc2a4\ud2b8 \ud558\ub124\uc2a4\uac00 \uc5b4\ub5bb\uac8c \uc791\ub3d9\ud558\ub294\uc9c0 \uc790\uc138\ud788 \uc124\uba85\ud574\ubcf4\uaca0\ub2e4.<\/p>\n\n\n\n

\"\"<\/figure>\n\n\n\n

\uc608\uc81c \ube4c\ub4dc\ud558\uae30<\/h2>\n\n\n\n

\uccab \ubc88\uc9f8 \ub2e8\uacc4\ub294 LLVM bitCode \ud615\uc2dd\uc758 \uc624\ube0c\uc81d\ud2b8 \ud30c\uc77c\uc744 \uc0dd\uc131\ud560 \uc218 \uc788\ub294 \ucef4\ud30c\uc77c\ub7ec\ub97c \uc0ac\uc6a9\ud558\uc5ec \uc18c\uc2a4 \ucf54\ub4dc\ub97c \ucef4\ud30c\uc77c\ud558\ub294 \uac83\uc774\ub2e4.<\/p>\n\n\n\n

examples\/regexp<\/strong> \ub514\ub809\ud1a0\ub9ac \ub0b4\uc5d0\uc11c \ub2e4\uc74c \uba85\ub839\uc744 \uc2e4\ud589\ud558\uc790:<\/p>\n\n\n\n

\n
\n
$ clang-11 -I \/snap\/klee\/6\/usr\/local\/include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone Regexp.c<\/pre>\n<\/div>\n<\/div>\n\n\n\n
\uc704 \uba85\ub839\uc744 \uc2e4\ud589\ud558\uba74, LLVM bitCode \ud615\uc2dd\uc758 Regexp.bc<\/strong> \ud30c\uc77c\uc774 \uc0dd\uc131\ub41c\ub2e4.<\/p>\n\n\n\n
-I <\/strong>\uc778\uc218\ub294 \ucef4\ud30c\uc77c\ub7ec\uac00 KLEE \uac00\uc0c1 \uba38\uc2e0\uacfc \uc0c1\ud638 \uc791\uc6a9\ud558\ub294 \ub370 \uc0ac\uc6a9\ub418\ub294 \ub0b4\uc7a5 \ud568\uc218\uc5d0 \ub300\ud55c \uc815\uc758\ub97c \ud3ec\ud568\ud558\ub294 klee\/klee.h<\/a> \ud5e4\ub354 \ud30c\uc77c\uc744 \ucc3e\uc744 \uc218 \uc788\ub3c4\ub85d \uc0ac\uc6a9\ub41c\ub2e4.<\/p>\n\n\n\n
-c<\/strong>\ub294 \ucf54\ub4dc\ub97c \ub124\uc774\ud2f0\ube0c \uc2e4\ud589 \ud30c\uc77c\uc774 \uc544\ub2cc \uc624\ube0c\uc81d\ud2b8 \ud30c\uc77c\ub85c \ucef4\ud30c\uc77c\ud558\ub824\ub294 \uac83\uc744 \ub098\ud0c0\ub0b4\uba70,<\/p>\n\n\n\n
\ub9c8\uc9c0\ub9c9\uc73c\ub85c -g<\/strong>\ub294 \uc624\ube0c\uc81d\ud2b8 \ud30c\uc77c\uc5d0 \ucd94\uac00 \ub514\ubc84\uadf8 \uc815\ubcf4\ub97c \uc800\uc7a5\ud558\ub3c4\ub85d \ud558\uba70, KLEE\uac00 \uc18c\uc2a4 \ucf54\ub4dc \ub77c\uc778 \ubc88\ud638 \uc815\ubcf4\ub97c \ub098\ud0c0\ub0b4\uae30 \uc704\ud574 \uc0ac\uc6a9\ud55c\ub2e4.<\/p>\n\n\n\n
-O0 -Xclang -disable-O0-optnone<\/strong>\uc740 \ucd5c\uc801\ud654 \uc5c6\uc774 \ucef4\ud30c\uc77c\ud558\ub418, KLEE\uac00 \uc790\uccb4 \ucd5c\uc801\ud654\ub97c \uc218\ud589\ud558\uc9c0 \ubabb\ud558\ub3c4\ub85d \ud558\ub294 \ub370 \uc0ac\uc6a9\ub418\uc5c8\ub2e4.<\/p>\n\n\n\n
LLVM \ub3c4\uad6c\uac00 \uacbd\ub85c\uc5d0 \uc124\uce58\ub418\uc5b4 \uc788\ub2e4\uba74, \uc774 \ub2e8\uacc4\uac00 \uc791\ub3d9\ud588\ub294\uc9c0 \uc0dd\uc131\ub41c \ud30c\uc77c\uc5d0\uc11c llvm-nm<\/strong>\uc744 \ud1b5\ud574 \ud655\uc778\ud560 \uc218 \uc788\ub2e4.<\/p>\n\n\n\n
\"\"<\/figure>\n\n\n\n
\ubcf4\ud1b5 \uc774 \ud504\ub85c\uadf8\ub7a8\uc744 \uc2e4\ud589\ud558\uae30 \uc804\uc5d0 \ub124\uc774\ud2f0\ube0c \uc2e4\ud589 \ud30c\uc77c\uc744 \uc0dd\uc131\ud558\uae30 \uc704\ud574 \ub9c1\ud06c\ud574\uc57c \ud560 \uac83\uc774\ub2e4.<\/p>\n\n\n\n
\uadf8\ub7ec\ub098 KLEE\ub294 \uc9c1\uc811 LLVM \ube44\ud2b8\ucf54\ub4dc \ud30c\uc77c\uc5d0\uc11c \uc2e4\ud589\ub41c\ub2e4.<\/p>\n\n\n\n
\uc774 \ud504\ub85c\uadf8\ub7a8\uc740 \ub2e8\uc77c \ud30c\uc77c\ub9cc \uac00\uc9c0\uace0 \uc788\uc73c\ubbc0\ub85c \ub9c1\ud06c\uac00 \ud544\uc694\ud558\uc9c0 \uc54a\ub2e4.<\/p>\n\n\n\n
\uc5ec\ub7ec \uc785\ub825\uc744 \uac00\uc9c4 “\uc2e4\uc81c” \ud504\ub85c\uadf8\ub7a8\uc758 \uacbd\uc6b0 \uc77c\ubc18\uc801\uc778 \ub9c1\ud06c \ub2e8\uacc4 \ub300\uc2e0 llvm-link<\/strong> \ub3c4\uad6c\ub97c \uc0ac\uc6a9\ud558\uc5ec \uc5ec\ub7ec LLVM \ube44\ud2b8\ucf54\ub4dc \ud30c\uc77c\uc744 \ud558\ub098\uc758 \ubaa8\ub4c8\ub85c \ubcd1\ud569\ud558\uc5ec KLEE\uc5d0\uc11c \uc2e4\ud589\ud560 \uc218 \uc788\ub2e4.<\/p>\n\n\n\n
KLEE\ub97c \ud1b5\ud574 \ucf54\ub4dc \uc2e4\ud589\ud558\uae30<\/h2>\n\n\n\n
\ub2e4\uc74c \ub2e8\uacc4\ub294 KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec \ucf54\ub4dc\ub97c \uc2e4\ud589\ud558\ub294 \uac83\uc774\ub2e4. (\uba85\ub839\uc5b4\uc758 \uc218\ub294 LLVM \ubc84\uc804 \ubc0f \ucd5c\uc801\ud654 \uc218\uc900\uc5d0 \ub530\ub77c \ub2e4\ub97c \uc218 \uc788\uc74c)<\/p>\n\n\n\n
\n
\n
$ klee --only-output-states-covering-new Regexp.bc\nKLEE: output directory is \"\/home\/ubuntu\/whitehat\/IOT-research\/klee-study\/tutorial_2\/klee-out-0\"\nKLEE: Using STP solver backend\nKLEE: SAT solver: MiniSat\nKLEE: ERROR: Regexp.c:14: memory error: out of bound pointer\nKLEE: NOTE: now ignoring this error at this location\nKLEE: ERROR: Regexp.c:16: memory error: out of bound pointer\nKLEE: NOTE: now ignoring this error at this location\n\nKLEE: done: total instructions = 4849788\nKLEE: done: completed paths = 6675\nKLEE: done: partially completed paths = 763\nKLEE: done: generated tests = 18\n<\/pre>\n<\/div>\n<\/div>\n\n\n\n
KLEE\ub97c \uc2dc\uc791\ud558\uba74 \ucd9c\ub825\uc744 \uc800\uc7a5\ud558\ub294 \ub514\ub809\ud1a0\ub9ac\ub97c \ud45c\uc2dc\ud55c\ub2e4. (ex: klee-out-0)<\/p>\n\n\n\n
KLEE\ub294 \uae30\ubcf8\uc801\uc73c\ub85c \uccab \ubc88\uc9f8 \ube48 klee-out-N<\/strong> \ub514\ub809\ud1a0\ub9ac\ub97c \uc0ac\uc6a9\ud558\uace0, 
\uac00\uc7a5 \ucd5c\uadfc\uc5d0 \uc0dd\uc131\ub41c \ub514\ub809\ud1a0\ub9ac\ub97c \uac00\ub9ac\ud0a4\ub294 klee-last <\/strong>\uc2ec\ubcfc\ub9ad \ub9c1\ud06c\ub3c4 \ub9cc\ub4e0\ub2e4.
\ucd9c\ub825\uc5d0 \uc0ac\uc6a9\ud560 \ub514\ub809\ud1a0\ub9ac\ub97c \uc9c0\uc815\ud558\ub824\uba74, \uba85\ub839\uc904 \uc778\uc218 -output-dir=path<\/strong>\ub97c \uc0ac\uc6a9\ud560 \uc218\ub3c4 \uc788\ub2e4.<\/p>\n\n\n\n
KLEE\uac00 \uc2e4\ud589 \uc911\uc77c \ub54c “\uc911\uc694\ud55c” \uc774\ubca4\ud2b8\uc5d0 \ub300\ud55c \uc0c1\ud0dc \uba54\uc2dc\uc9c0\ub97c \ucd9c\ub825\ud574\uc900\ub2e4.
\uc608\ub97c \ub4e4\uc5b4 \ud504\ub85c\uadf8\ub7a8\uc5d0\uc11c \uc624\ub958\ub97c \ubc1c\uacac\ud588\uc744 \ub54c \uba54\uc2dc\uc9c0\uac00 \ud45c\uc2dc\ub41c\ub2e4.
\uc774 \uacbd\uc6b0 KLEE\ub294 \ud14c\uc2a4\ud2b8 \ud504\ub85c\uadf8\ub7a8\uc758 14\ubc88\uc9f8\uc640 16\ubc88\uc9f8 \ub77c\uc778\uc5d0\uc11c memory error: out of bound pointer (\ub450 \uac1c\uc758 \uc798\ubabb\ub41c \uba54\ubaa8\ub9ac \uc561\uc138\uc2a4)<\/strong>\ub97c \uac10\uc9c0\ud588\ub2e4\uace0 \ub098\ud0c0\ub09c\ub2e4.
\uc774\uc5d0 \ub300\ud574\uc11c\ub294 \uc7a0\uc2dc\ud6c4 \uc790\uc138\ud788 \ub2e4\uc2dc \ud55c\ubc88 \uc0b4\ud3b4\ubcfc \uac83\uc774\ub2e4.<\/p>\n\n\n\n
\ub9c8\uc9c0\ub9c9\uc73c\ub85c, KLEE \uc2e4\ud589\uc774 \uc644\ub8cc\ub418\uba74 \uc2e4\ud589\uc5d0 \uad00\ud55c \uba87 \uac00\uc9c0 \ud1b5\uacc4\ub97c \ucd9c\ub825\ud55c\ub2e4.
\uc5ec\uae30\uc5d0\uc11c \ubcfc \uc218 \uc788\ub4ef\uc774 KLEE\ub294 \ucd1d \uc57d 4.8 \ubc31\ub9cc <\/strong>\uac1c\uc758 \uba85\ub839\uc5b4\ub97c \uc2e4\ud589\ud558\uace0 7,438<\/strong>\uac1c\uc758 \uacbd\ub85c\ub97c \ud0d0\uc0c9\ud558\uba70 16<\/strong>\uac1c\uc758 \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc0dd\uc131\ud574\ub0c8\ub2e4.
KLEE\ub294 \uc0c8\ub85c\uc6b4 \ucf54\ub4dc\ub97c \uc2e4\uc81c\ub85c \ud3ec\ud568\ud558\ub294 \uc0c1\ud0dc\uc5d0 \ub300\ud55c \ud14c\uc2a4\ud2b8 \uc0dd\uc131\uc744 –only-output-states-covering-new<\/strong>\ub85c \uc81c\ud55c\ud588\uae30 \ub54c\ubb38\uc5d0 16\uac1c\uc758 \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub9cc \uc0dd\uc131\ud588\ub2e4.<\/p>\n\n\n\n
\uc774 \ud50c\ub798\uadf8\ub97c \uc81c\uc678\ud558\uba74 KLEE\ub294 6,677<\/strong>\uac1c\uc758 \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc0dd\uc131\ud560 \uac83\uc774\ub2e4.
\uadf8\ub7fc\uc5d0\ub3c4 \ubd88\uad6c\ud558\uace0 KLEE\ub294 \ubaa8\ub4e0 \uacbd\ub85c\uc5d0 \ub300\ud574 \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc0dd\uc131\ud558\uc9c0 \uc54a\ub294\ub2e4.<\/p>\n\n\n\n
\ubc84\uadf8\ub97c \ubc1c\uacac\ud558\uba74 \ud574\ub2f9 \ubc84\uadf8\uc5d0 \ub3c4\ub2ec\ud558\ub294 \uccab \ubc88\uc9f8 \uc0c1\ud0dc\uc5d0 \ub300\ud55c \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc0dd\uc131\ud55c\ub2e4.
\ud574\ub2f9 \uc704\uce58\uc5d0\uc11c \ub3d9\uc77c\ud55c \ubc84\uadf8\uc5d0 \ub3c4\ub2ec\ud558\ub294 \ub2e4\ub978 \ubaa8\ub4e0 \uacbd\ub85c\ub294 \uc870\uc6a9\ud788 \uc885\ub8cc\ub418\uace0 \ubd80\ubd84\uc801\uc73c\ub85c \uc644\ub8cc\ub41c \uacbd\ub85c\ub85c \ubcf4\uace0\ub41c\ub2e4.<\/p>\n\n\n\n
\uc624\ub958 \ucf00\uc774\uc2a4\uc758 \uc911\ubcf5\uc744 \uc2e0\uacbd \uc4f0\uc9c0 \uc54a\ub294\ub2e4\uba74, –emit-all-errors<\/strong> \uc635\uc158\uc744 \uc0ac\uc6a9\ud558\uc5ec 7,438<\/strong>\uac1c\uc758 \uacbd\ub85c\uc5d0 \ub300\ud55c \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc0dd\uc131\uc2dc\ud0ac \uc218\ub3c4 \uc788\ub2e4.<\/p>\n\n\n\n
\ub9ce\uc740 \ud604\uc2e4\uc801\uc778 \ud504\ub85c\uadf8\ub7a8\ub4e4\uc740 \ubb34\ud55c\ud558\uac70\ub098(\ub610\ub294 \uadf9\ud788 \ud070) \ub9ce\uc740 \uacbd\ub85c\ub97c \uac00\uc9c0\uba70, KLEE\uac00 \uc885\ub8cc\ub418\uc9c0 \uc54a\ub294 \uac83\uc774 \uc77c\ubc18\uc801\uc774\ub2e4.
\uae30\ubcf8\uc801\uc73c\ub85c KLEE\ub294 \uc0ac\uc6a9\uc790\uac00 Control-C<\/strong>\ub97c \ub204\ub97c \ub54c\uae4c\uc9c0 \uacc4\uc18d \uc2e4\ud589\ub41c\ub2e4.(\uc989, KLEE\uac00 SIGINT<\/strong>\ub97c \ubc1b\uc744 \ub54c\uae4c\uc9c0\ub97c \uc758\ubbf8)<\/p>\n\n\n\n
\uadf8\ub7ec\ub098 KLEE\uc758 \uc2e4\ud589 \uc2dc\uac04\uacfc \uba54\ubaa8\ub9ac \uc0ac\uc6a9\ub7c9\uc744 \uc81c\ud55c\ud558\ub294 \ubd80\uac00 \uc635\uc158\ub4e4\uc774 \uc874\uc7ac\ud55c\ub2e4.<\/p>\n\n\n\n