{"id":1151,"date":"2023-11-13T13:09:02","date_gmt":"2023-11-13T04:09:02","guid":{"rendered":"https:\/\/h4ck.kr\/?p=1151"},"modified":"2023-11-13T13:15:55","modified_gmt":"2023-11-13T04:15:55","slug":"%ec%8b%ac%eb%b3%bc%eb%a6%ad-%ed%99%98%ea%b2%bd-%ec%82%ac%ec%9a%a9-%ed%85%8c%ec%8a%a4%ed%8a%b8-%eb%8c%80%ec%83%81-%ed%94%84%eb%a1%9c%ea%b7%b8%eb%9e%a8%ec%97%90-%eb%8c%80%ed%95%9c-%ec%8b%ac%eb%b3%bc","status":"publish","type":"post","link":"https:\/\/h4ck.kr\/?p=1151","title":{"rendered":"\uc2ec\ubcfc\ub9ad \ud658\uacbd \uc0ac\uc6a9: \ud14c\uc2a4\ud2b8 \ub300\uc0c1 \ud504\ub85c\uadf8\ub7a8\uc5d0 \ub300\ud55c \uc2ec\ubcfc\ub9ad \ud30c\uc77c \ubc0f \uba85\ub839\uc904 \uc778\uc218\uc640 \uac19\uc740 \uc2ec\ubcfc\ub9ad \ud658\uacbd\uc744 \uc0ac\uc6a9\ud558\ub294 \ubc29\ubc95\uc5d0 \ub300\ud55c \uac00\uc774\ub4dc \ubc0f \uc608\uc81c"},"content":{"rendered":"\n<p class=\"wp-block-paragraph\"><a href=\"https:\/\/klee.github.io\/docs\/options\/\">KLEE\uc758 \uae30\ubcf8 \uba85\ub839\uc904 \uc635\uc158 \uac1c\uc694<\/a>\uc5d0\uc11c \uc5b8\uae09\ud55c \ub300\ub85c, KLEE\ub294 \uc2ec\ubcfc\ub9ad \ud658\uacbd\uc758 \uc77c\ubd80\ub85c \uc5ec\ub7ec \uc635\uc158\uc744 \uc81c\uacf5\ud55c\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uadf8\ub7ec\ub098 \uc774\ub7ec\ud55c \uc635\uc158\uc758 \uc0ac\uc6a9\uc740 \uc0c8\ub85c\uc6b4 \uc0ac\uc6a9\uc790\uc5d0\uac8c\ub294 \uc885\uc885 \uc774\ud574\ud558\uae30 \uc5b4\ub835\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uc774 \ud29c\ud1a0\ub9ac\uc5bc\uc740 <strong>-sym-arg<\/strong> \ubc0f <strong>-sym-files<\/strong> \uc635\uc158 \uc911 \uac00\uc7a5 \uc911\uc694\ud55c \uac83\uc73c\ub85c \uc0dd\uac01\ub418\ub294 \uc635\uc158\uc5d0 \ub300\ud55c \uae30\ubcf8 \uc0ac\uc6a9 \uc608\uc81c\ub97c \uc81c\uacf5\ud55c\ub2e4.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">-sym-arg <strong>\uc635\uc158<\/strong><\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">\uc6b0\ub9ac\ub294 <strong>-sym-arg &lt;N&gt;<\/strong> \uc635\uc158\uc774 \ud14c\uc2a4\ud2b8 \ub300\uc0c1 \ud504\ub85c\uadf8\ub7a8\uc5d0 \uae38\uc774 <strong>N<\/strong>\uc758 \uba85\ub839\uc904 \uc778\uc218\ub97c \uc81c\uacf5\ud55c\ub2e4\ub294 \uac83\uc744 \uc54c \uc218 \uc788\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uc774 \uc635\uc158\uc758 \ubcc0\ud615\uc778<strong> -sym-args &lt;MIN&gt; &lt;MAX&gt; &lt;N&gt;<\/strong>\uc740 \uc801\uc5b4\ub3c4 <strong>MIN<\/strong>\uac1c\uc758 \uc778\uc218\uc640 \ucd5c\ub300 <strong>MAX<\/strong>\uac1c\uc758 \uc2ec\ubcfc\ub9ad \uc778\uc218\ub97c \uc81c\uacf5\ud558\uba70 \uac01\uac01\uc758 \ucd5c\ub300 \uae38\uc774\uac00<strong> N<\/strong>\uc744 \uc758\ubbf8\ud55c\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>-sym-arg<\/strong> \uc635\uc158\uc744 \uc124\uba85\ud558\uae30 \uc704\ud574 \uba3c\uc800 \ud558\ub4dc\ucf54\ub529\ub41c \ube44\ubc00\ubc88\ud638\uc640 \uba85\ub839\uc904 \uc778\uc218\ub97c \ube44\uad50\ud558\ub294 \ub2e4\uc74c\uc758 \ud504\ub85c\uadf8\ub7a8 \uc18c\uc2a4\ucf54\ub4dc\uc778 <strong>password.c<\/strong>\ub97c \uc608\ub85c \ub4e4\uaca0\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-8f761849 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"c\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">#include &lt;stdio.h>\n\nint check_password(char *buf) {\n  if (buf[0] == 'h' &amp;&amp; buf[1] == 'e' &amp;&amp;\n      buf[2] == 'l' &amp;&amp; buf[3] == 'l' &amp;&amp;\n      buf[4] == 'o')\n    return 1;\n  return 0;\n}\n\nint main(int argc, char **argv) {\n  if (argc &lt; 2)\n     return 1;\n  \n  if (check_password(argv[1])) {\n    printf(\"Password found!\\\\n\");\n    return 0;\n  }\n\n  return 1;\n}<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p class=\"wp-block-paragraph\">\uc2ec\ubcfc\ub9ad \ud658\uacbd\uc744 \ud65c\uc131\ud654\ud558\ub824\uba74, KLEE\uc5d0 <strong>-posix-runtime<\/strong> \uc635\uc158\uc744 \uc9c0\uc815\ud574\uc57c \ud55c\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>password.c<\/strong>\uc758 bitCode\ub97c \uc785\ub825\uc73c\ub85c \uc0ac\uc6a9\ud558\uace0, <strong>-sym-arg<\/strong> \uc635\uc158\uc744 \ub2e4\uc74c\uacfc \uac19\uc774 \uc0ac\uc6a9\ud558\uc5ec KLEE\ub97c \uc2e4\ud589\ud55c\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-8f761849 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"raw\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">$ clang-11 -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone password.c\n$ klee -posix-runtime password.bc -sym-arg 5\nKLEE: NOTE: Using POSIX model: \/snap\/klee\/6\/usr\/local\/lib\/klee\/runtime\/libkleeRuntimePOSIX64_Debug+Asserts.bca\nKLEE: output directory is \"\/home\/ubuntu\/whitehat\/IOT-research\/klee-study\/tutorial_3\/klee-out-0\"\nKLEE: Using STP solver backend\nKLEE: SAT solver: MiniSat\nwarning: Linking two modules of different target triples: 'password.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'klee_range64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'memcpy64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'memset64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'klee_overshift_check64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nKLEE: WARNING: undefined reference to function: printf\nKLEE: WARNING: undefined reference to function: strlen\nKLEE: WARNING: undefined reference to function: strncmp\nKLEE: WARNING ONCE: Alignment of memory from call \"malloc\" is not modelled. Using alignment of 8.\nKLEE: WARNING ONCE: calling external: syscall(4, 93888559554320, 93888557024960) at klee_src\/runtime\/POSIX\/fd.c:530 12\nKLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.\nKLEE: WARNING ONCE: calling external: printf(93888562012160) at password.c:17 5\nPassword found!\n\nKLEE: done: total instructions = 2028\nKLEE: done: completed paths = 6\nKLEE: done: partially completed paths = 0\nKLEE: done: generated tests = 6<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p class=\"wp-block-paragraph\">\ubcf4\ub2e4\uc2dc\ud53c, \uba85\ub839\uc904 \uc778\uc218\uac00 \uc2ec\ubcfc\ub9ad\uc778 \uacbd\uc6b0, KLEE\ub294 \ud558\ub098\uc758 \uacbd\ub85c\uc5d0\uc11c \uba85\ub839\uc904 \uc778\uc218\uac00 \ube44\ubc00\ubc88\ud638\uc640 \uc77c\uce58\ud558\ub294 \uacbd\uc6b0\ub97c \ud3ec\ud568\ud558\uc5ec \uc5ec\uc12f \uac1c\uc758 \uacbd\ub85c\ub97c \uc2e4\ud589\ud588\ub2e4.<\/p>\n\n\n\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"861\" src=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-9-1024x861.png\" alt=\"\" class=\"wp-image-1153\" srcset=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-9-1024x861.png 1024w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-9-300x252.png 300w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-9-768x646.png 768w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-9.png 1115w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<h2 class=\"wp-block-heading\"><strong>-sym-files \uc635\uc158<\/strong><\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">\uc635\uc158 <strong>-sym-files &lt;NUM&gt; &lt;N&gt;<\/strong>\ub294 <strong>NUM<\/strong>\uac1c\uc758 \uc2ec\ubcfc\ub9ad \ud30c\uc77c\uc744 \uc0dd\uc131\ud558\uba70, \uccab \ubc88\uc9f8 \ud30c\uc77c\uc740 <strong>&#8216;A&#8217;<\/strong>\ub85c \uc774\ub984 \uc9c0\uc5b4\uc9c0\uace0 \ub450 \ubc88\uc9f8 \ud30c\uc77c\uc740 <strong>&#8216;B&#8217;<\/strong>\ub85c \uc774\ub984 \uc9c0\uc5b4\uc9c0\uba70 \uc774\uc5b4\uc11c \uc9c4\ud589\ub41c\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uac01 \ud30c\uc77c\uc758 \ud06c\uae30\ub294 <strong>N<\/strong>\uc73c\ub85c \uc9c0\uc815\ud560 \uc218 \uc788\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uc774 \uc635\uc158\uc758 \uc720\uc0ac\ud55c \uc635\uc158\uc73c\ub85c <strong>-sym-stdin<\/strong>\uacfc <strong>-sym-stdout<\/strong>\uac00 \uc788\uc73c\uba70, \uac01\uac01 \ud45c\uc900 \uc785\ub825 \ubc0f \ud45c\uc900 \ucd9c\ub825\uc744 \uc2ec\ubcfc\ub9ad\ud558\uac8c \ub9cc\ub4e0\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uc774\uc81c \uc0ac\uc6a9\uc790\uac00 \uc9c0\uc815\ud55c \ud30c\uc77c\uc5d0\uc11c \ubb38\uc790\uc5f4\uc744 \uc77d\uc5b4 \ud558\ub4dc \ucf54\ub529\ub41c \ube44\ubc00\ubc88\ud638\uc640 \uc77c\uce58\ud558\ub294\uc9c0 \ud655\uc778\ud558\ub294 <strong>password2.c<\/strong> \uc18c\uc2a4\ucf54\ub4dc\uc778 \uc774\ub984\uc758 \ud328\uc2a4\uc6cc\ub4dc \uac80\uc0ac\uae30\ub97c \uace0\ub824\ud574\ubcf4\uc790.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\ud30c\uc77c \uc774\ub984\uc774 \uc9c0\uc815\ub418\uc9c0 \uc54a\uac70\ub098 \ud30c\uc77c\uc744 \uc5f4 \ub54c \uc624\ub958\uac00 \ubc1c\uc0dd\ud558\uba74 \ud45c\uc900 \uc785\ub825\uc5d0\uc11c \ubb38\uc790\uc5f4\uc744 \uc77d\ub294\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-8f761849 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"c\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">#include &lt;sys\/types.h>\n#include &lt;sys\/stat.h>\n#include &lt;fcntl.h>\n#include &lt;stdio.h>\n#include &lt;unistd.h>\n\nint check_password(int fd) {\n  char buf[5];\n  if (read(fd, buf, 5) != -1) {\n    if (buf[0] == 'h' &amp;&amp; buf[1] == 'e' &amp;&amp;\n\tbuf[2] == 'l' &amp;&amp; buf[3] == 'l' &amp;&amp;\n\tbuf[4] == 'o')\n      return 1;\n  }\n  return 0;\n}\n\nint main(int argc, char **argv) {\n  int fd;\n\n  if (argc >= 2) {\n    if ((fd = open(argv[1], O_RDONLY)) != -1) {\n      if (check_password(fd)) {\n        printf(\"Password found in %s\\\\n\", argv[1]);\n        close(fd);\n        return 0;\n      }\n      close(fd);\n      return 1;\n    }\n  }\n\n  if (check_password(0)) {\n    printf(\"Password found in standard input\\\\n\");\n    return 0;\n  }\n\n  return 1;\n}<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p class=\"wp-block-paragraph\">\uc774\uc81c KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec \ud504\ub85c\uadf8\ub7a8\uc744 \uc2e4\ud589\ud55c\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\ub370\uc774\ud130\ub97c \uc77d\uc73c\ub824\uace0 \uc2dc\ub3c4\ud558\ub2e4\uac00 \ud504\ub85c\uadf8\ub7a8\uc774 \uba48\ucd94\ub294 \uac83\uc744 \ubc29\uc9c0\ud558\ub824\uba74 \uc785\ub825\uc744 \uc81c\uacf5\ud574\uc57c \ud55c\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uccab \ubc88\uc9f8 \uc2e4\ud589\uc5d0\uc11c\ub294<strong> -sym-stdin<\/strong> \uc635\uc158\uc744 \uc0ac\uc6a9\ud558\uc5ec \uc2ec\ubcfc\ub9ad \ud45c\uc900 \uc785\ub825\uc744 \uc81c\uacf5\ud55c\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uc2ec\ubcfc\ub9ad \uc785\ub825\uc744 \uc81c\uacf5\ud568\uc73c\ub85c\uc368 KLEE\ub294 \ube44\ubc00\ubc88\ud638 \ud655\uc778\uc774 \uc131\uacf5\ud558\ub294 \uacbd\ub85c\ub97c \ud0d0\uc0c9\ud560 \uac83\uc774\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-8f761849 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"raw\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">$ clang-11 -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone password2.c\n$ klee -posix-runtime password2.bc -sym-stdin 10\nKLEE: NOTE: Using POSIX model: \/snap\/klee\/6\/usr\/local\/lib\/klee\/runtime\/libkleeRuntimePOSIX64_Debug+Asserts.bca\nKLEE: output directory is \"\/home\/ubuntu\/whitehat\/IOT-research\/klee-study\/tutorial_3\/klee-out-1\"\nKLEE: Using STP solver backend\nKLEE: SAT solver: MiniSat\nwarning: Linking two modules of different target triples: 'password2.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'klee_range64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'memcpy64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'memmove64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'memset64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'klee_overshift_check64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nKLEE: WARNING: undefined reference to function: printf\nKLEE: WARNING: undefined reference to function: strlen\nKLEE: WARNING: undefined reference to function: strncmp\nKLEE: WARNING ONCE: Alignment of memory from call \"malloc\" is not modelled. Using alignment of 8.\nKLEE: WARNING ONCE: calling external: syscall(4, 94631781707192, 94631778752272) at klee_src\/runtime\/POSIX\/fd.c:530 12\nKLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.\nKLEE: WARNING ONCE: calling external: printf(94631781840032) at password2.c:35 5\nPassword found in standard input\n\nKLEE: done: total instructions = 2934\nKLEE: done: completed paths = 6\nKLEE: done: partially completed paths = 0\nKLEE: done: generated tests = 6<\/pre>\n<\/div>\n<\/div>\n\n\n\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"861\" src=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-10-1024x861.png\" alt=\"\" class=\"wp-image-1155\" srcset=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-10-1024x861.png 1024w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-10-300x252.png 300w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-10-768x646.png 768w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-10.png 1115w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<p class=\"wp-block-paragraph\">\uc774\uc81c KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec \ube44\ubc00\ubc88\ud638\ub97c \ubc1c\uacac\ud574\ub0c8\ub2e4!<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uc6b0\ub9ac\uc758 \ud504\ub85c\uadf8\ub7a8\uc740 \ub514\uc2a4\ud06c \ud30c\uc77c\uc5d0\uc11c \ube44\ubc00\ubc88\ud638\ub97c \uc77d\uc744 \uc218\ub3c4 \uc788\uc9c0\ub9cc, \ube44\ubc00\ubc88\ud638 \ud655\uc778\uc774 \uc131\uacf5\ud558\ub294 \uacbd\ub85c\ub97c \uc2e4\ud589\ud558\ub3c4\ub85d KLEE\uac00 \ud30c\uc77c\uc758 \uc2ec\ubcfc\ub9ad \ub0b4\uc6a9\uc744 \uc77d\uae30\ub97c \uc6d0\ud55c\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>-sym-files<\/strong> \uc635\uc158\uc740 <strong>&#8216;A&#8217;, &#8216;B&#8217;, &#8216;C&#8217; <\/strong>\ub4f1\uc758 \uc774\ub984\uc744 \uac00\uc9c4 \uc5ec\ub7ec \uc2ec\ubcfc\ub9ad \ud30c\uc77c\uc744 \uc81c\uacf5\ud55c\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uc544\ub798\uc758 <strong>-sym-files<\/strong> <strong>1 10<\/strong> \uc635\uc158\uc744 \uc9c0\uc815\ud568\uc73c\ub85c\uc368, KLEE\uc5d0\uac8c \ud06c\uae30\uac00 <strong>10\ubc14\uc774\ud2b8\uc778 \uc2ec\ubcfc\ub9ad \ud30c\uc77c \ud558\ub098<\/strong>\ub97c \uc81c\uacf5\ud558\ub3c4\ub85d \uc694\uccad\ud558\uace0, KLEE\ub294 \uc774 \ud30c\uc77c\uc744<strong> &#8216;A&#8217;<\/strong>\ub85c \uc774\ub984\uc744 \uc9c0\uc5b4\uc900\ub2e4.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">\uadf8\ub7ec\ubbc0\ub85c \uc774 \ud30c\uc77c \uc774\ub984\uc744 \uc6b0\ub9ac\uc758 \ud504\ub85c\uadf8\ub7a8\uc5d0 \uc778\uc218\ub85c \uc81c\uacf5\ud55c\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-8f761849 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"raw\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">$ klee -posix-runtime password2.bc A -sym-files 1 10\nKLEE: NOTE: Using POSIX model: \/snap\/klee\/6\/usr\/local\/lib\/klee\/runtime\/libkleeRuntimePOSIX64_Debug+Asserts.bca\nKLEE: output directory is \"\/home\/ubuntu\/whitehat\/IOT-research\/klee-study\/tutorial_3\/klee-out-2\"\nKLEE: Using STP solver backend\nKLEE: SAT solver: MiniSat\nwarning: Linking two modules of different target triples: 'password2.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'klee_range64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'memcpy64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'memmove64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'memset64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nwarning: Linking two modules of different target triples: 'klee_overshift_check64_Debug+Asserts.bc' is 'x86_64-pc-linux-gnu' whereas 'klee_init_env64_Debug+Asserts.bc' is 'x86_64-unknown-linux-gnu'\n\nKLEE: WARNING: undefined reference to function: printf\nKLEE: WARNING: undefined reference to function: strlen\nKLEE: WARNING: undefined reference to function: strncmp\nKLEE: WARNING ONCE: Alignment of memory from call \"malloc\" is not modelled. Using alignment of 8.\nKLEE: WARNING ONCE: calling external: syscall(4, 94091070492128, 94091067545360) at klee_src\/runtime\/POSIX\/fd.c:530 12\nKLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.\nKLEE: WARNING ONCE: calling external: printf(94091070597920, 94091070491088) at password2.c:25 15\nPassword found in A\n\nKLEE: done: total instructions = 6351\nKLEE: done: completed paths = 6\nKLEE: done: partially completed paths = 0\nKLEE: done: generated tests = 6<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p class=\"wp-block-paragraph\">\ube44\ubc00\ubc88\ud638\ub294 \uc2e4\ud589 \uacbd\ub85c \uc911 \ud558\ub098\uc5d0\uc11c \uc2ec\ubcfc\ub9ad \ud30c\uc77c<strong> A<\/strong>\ub85c\ubd80\ud130 \uc131\uacf5\uc801\uc73c\ub85c \uc77d\uc744 \uc218 \uc788\uc5c8\ub2e4.<\/p>\n\n\n\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"893\" src=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-11-1024x893.png\" alt=\"\" class=\"wp-image-1156\" srcset=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-11-1024x893.png 1024w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-11-300x262.png 300w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-11-768x670.png 768w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-11.png 1075w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<h2 class=\"wp-block-heading\">\ucd9c\ucc98 \ubc0f \ubc88\uc5ed<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\"><a href=\"https:\/\/klee.github.io\/tutorials\/using-symbolic\/\">https:\/\/klee.github.io\/tutorials\/using-symbolic\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>KLEE\uc758 \uae30\ubcf8 \uba85\ub839\uc904 \uc635\uc158 \uac1c\uc694\uc5d0\uc11c \uc5b8\uae09\ud55c \ub300\ub85c, KLEE\ub294 \uc2ec\ubcfc\ub9ad \ud658\uacbd\uc758 \uc77c\ubd80\ub85c \uc5ec\ub7ec \uc635\uc158\uc744 \uc81c\uacf5\ud55c\ub2e4. \uadf8\ub7ec\ub098 \uc774\ub7ec\ud55c \uc635\uc158\uc758 \uc0ac\uc6a9\uc740 \uc0c8\ub85c\uc6b4 \uc0ac\uc6a9\uc790\uc5d0\uac8c\ub294 \uc885\uc885 \uc774\ud574\ud558\uae30 \uc5b4\ub835\ub2e4. \uc774 \ud29c\ud1a0\ub9ac\uc5bc\uc740 -sym-arg \ubc0f -sym-files \uc635\uc158 \uc911 \uac00\uc7a5 \uc911\uc694\ud55c \uac83\uc73c\ub85c \uc0dd\uac01\ub418\ub294 \uc635\uc158\uc5d0 \ub300\ud55c \uae30\ubcf8 \uc0ac\uc6a9 \uc608\uc81c\ub97c \uc81c\uacf5\ud55c\ub2e4. -sym-arg \uc635\uc158 \uc6b0\ub9ac\ub294 -sym-arg &lt;N&gt; \uc635\uc158\uc774 \ud14c\uc2a4\ud2b8 \ub300\uc0c1 \ud504\ub85c\uadf8\ub7a8\uc5d0 \uae38\uc774 N\uc758 \uba85\ub839\uc904 \uc778\uc218\ub97c \uc81c\uacf5\ud55c\ub2e4\ub294 \uac83\uc744&hellip;&nbsp;<a href=\"https:\/\/h4ck.kr\/?p=1151\" rel=\"bookmark\">\ub354 \ubcf4\uae30 &raquo;<span class=\"screen-reader-text\">\uc2ec\ubcfc\ub9ad \ud658\uacbd \uc0ac\uc6a9: \ud14c\uc2a4\ud2b8 \ub300\uc0c1 \ud504\ub85c\uadf8\ub7a8\uc5d0 \ub300\ud55c \uc2ec\ubcfc\ub9ad \ud30c\uc77c \ubc0f \uba85\ub839\uc904 \uc778\uc218\uc640 \uac19\uc740 \uc2ec\ubcfc\ub9ad \ud658\uacbd\uc744 \uc0ac\uc6a9\ud558\ub294 \ubc29\ubc95\uc5d0 \ub300\ud55c \uac00\uc774\ub4dc \ubc0f \uc608\uc81c<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"neve_meta_sidebar":"","neve_meta_container":"","neve_meta_enable_content_width":"","neve_meta_content_width":0,"neve_meta_title_alignment":"","neve_meta_author_avatar":"","neve_post_elements_order":"","neve_meta_disable_header":"","neve_meta_disable_footer":"","neve_meta_disable_title":"","_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[15],"tags":[20],"class_list":["post-1151","post","type-post","status-publish","format-standard","hentry","category-whitehat1","tag-klee"],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/posts\/1151","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/h4ck.kr\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=1151"}],"version-history":[{"count":4,"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/posts\/1151\/revisions"}],"predecessor-version":[{"id":1160,"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/posts\/1151\/revisions\/1160"}],"wp:attachment":[{"href":"https:\/\/h4ck.kr\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=1151"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/h4ck.kr\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=1151"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/h4ck.kr\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=1151"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}