eurecom-s3 / symcc

SymCC: efficient compiler-based symbolic execution
http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
GNU General Public License v3.0
773 stars 135 forks source link

Additional Questions (sorry, don't know where to put them) #27

Closed straightblast closed 3 years ago

straightblast commented 3 years ago

So i suspect my compilation of my target under symcc is not working correctly. I went back to the 'whiteboard' and try to build some basic code to ensure it generates some output under /tmp/output.

(1) I first played with the sample.cpp that came with the docker file. I noticed the solution is only discovered if i provided an input with a string length equal to the value that is being compared (root). If i tried anything else such as echo 'a' or echo 'aaaaa' and pass it to the sample binary. the generated solution under /tmp/output does not contain 'root'. Is this the correct behaviour?

(2) The second thing I tried is to compile the sample.cpp through sym++. I understand the libc++ stuff have to also be instrumented, and that the docker container have already setup and environment variable SYMCC_LIBCXX_PATH which points to "/libcxx_symcc_install". However, when i compiled the sample.cpp, i get the following error:

ubuntu@symcc:~$ sym++ -o sample sample.cpp In file included from sample.cpp:1: In file included from /libcxx_symcc_install/include/c++/v1/iostream:37: In file included from /libcxx_symcc_install/include/c++/v1/ios:214: /libcxx_symcc_install/include/c++/v1/iosfwd:189:14: error: use of undeclared identifier 'mbstate_t' typedef fpos streampos; ^ /libcxx_symcc_install/include/c++/v1/iosfwd:190:14: error: use of undeclared identifier 'mbstate_t' typedef fpos wstreampos; ^ /libcxx_symcc_install/include/c++/v1/iosfwd:195:14: error: use of undeclared identifier 'mbstate_t' typedef fpos u16streampos; ^ /libcxx_symcc_install/include/c++/v1/iosfwd:196:14: error: use of undeclared identifier 'mbstate_t' typedef fpos u32streampos; ^ In file included from sample.cpp:1: In file included from /libcxx_symcc_install/include/c++/v1/iostream:37: In file included from /libcxx_symcc_install/include/c++/v1/ios:215: In file included from /libcxx_symcc_install/include/c++/v1/locale:14: In file included from /libcxx_symcc_install/include/c++/v1/string:504: In file included from /libcxx_symcc_install/include/c++/v1/string_view:175: In file included from /libcxx_symcc_install/include/c++/v1/string:57: In file included from /libcxx_symcc_install/include/c++/v1/algorithm:641: In file included from /libcxx_symcc_install/include/c++/v1/cstring:60: /libcxx_symcc_install/include/c++/v1/string.h:73:64: error: use of undeclared identifier 'strchr' char* libcpp_strchr(const char* s, int c) {return (char*)strchr(s, c);} ^ /libcxx_symcc_install/include/c++/v1/string.h:80:75: error: use of undeclared identifier 'strpbrk' char* libcpp_strpbrk(const char __s1, const char s2) {return (char*)strpbrk(s1, s2);} ^ /libcxx_symcc_install/include/c++/v1/string.h:87:65: error: use of undeclared identifier 'strrchr'; did you mean 'strchr'? char* libcpp_strrchr(const char s, int c) {return (char)strrchr(s, c);} ^ /libcxx_symcc_install/include/c++/v1/string.h:75:13: note: 'strchr' declared here const char strchr(const char s, int c) {return libcpp_strchr(s, c);} ^ /libcxx_symcc_install/include/c++/v1/string.h:94:76: error: use of undeclared identifier 'memchr' void __libcpp_memchr(const void s, int c, size_t n) {return (void*)memchr(s, c, n);} ^ /libcxx_symcc_install/include/c++/v1/string.h:101:74: error: use of undeclared identifier 'strstr'; did you mean 'strchr'? char __libcpp_strstr(const char s1, const char __s2) {return (char)strstr(s1, s2);} ^ /libcxx_symcc_install/include/c++/v1/string.h:77:13: note: 'strchr' declared here char strchr( char s, int c) {return libcpp_strchr(s, c);} ^ /libcxx_symcc_install/include/c++/v1/string.h:101:74: error: no matching function for call to 'strchr' char __libcpp_strstr(const char s1, const char __s2) {return (char)strstr(s1, s2);} ^ /libcxx_symcc_install/include/c++/v1/string.h:77:13: note: candidate disabled: char strchr( char s, int c) {return libcpp_strchr(s, c);} ^ /libcxx_symcc_install/include/c++/v1/string.h:101:81: error: cannot initialize a parameter of type 'char ' with an lvalue of type 'const char ' char __libcpp_strstr(const char s1, const char __s2) {return (char)strstr(s1, s2);} ^~~~ /libcxx_symcc_install/include/c++/v1/string.h:77:32: note: passing argument to parameter 's' here char strchr( char s, int c) {return libcpp_strchr(s, c);} ^ In file included from sample.cpp:1: In file included from /libcxx_symcc_install/include/c++/v1/iostream:37: In file included from /libcxx_symcc_install/include/c++/v1/ios:215: In file included from /libcxx_symcc_install/include/c++/v1/locale:14: In file included from /libcxx_symcc_install/include/c++/v1/string:504: In file included from /libcxx_symcc_install/include/c++/v1/string_view:175: In file included from /libcxx_symcc_install/include/c++/v1/string:57: In file included from /libcxx_symcc_install/include/c++/v1/algorithm:641: /libcxx_symcc_install/include/c++/v1/cstring:69:9: error: no member named 'memcpy' in the global namespace; did you mean 'memchr'? using ::memcpy; ~~^ /libcxx_symcc_install/include/c++/v1/string.h:96:13: note: 'memchr' declared here const void memchr(const void s, int __c, size_t n) {return libcpp_memchr(s, c, n);} ^ In file included from sample2.cpp:1: In file included from /libcxx_symcc_install/include/c++/v1/iostream:37: In file included from /libcxx_symcc_install/include/c++/v1/ios:215: In file included from /libcxx_symcc_install/include/c++/v1/locale:14: In file included from /libcxx_symcc_install/include/c++/v1/string:504: In file included from /libcxx_symcc_install/include/c++/v1/string_view:175: In file included from /libcxx_symcc_install/include/c++/v1/string:57: In file included from /libcxx_symcc_install/include/c++/v1/algorithm:641: /libcxx_symcc_install/include/c++/v1/cstring:70:9: error: no member named 'memmove' in the global namespace using ::memmove; ~~^ /libcxx_symcc_install/include/c++/v1/cstring:71:9: error: no member named 'strcpy' in the global namespace; did you mean 'strchr'? using ::strcpy; ~~^ /libcxx_symcc_install/include/c++/v1/string.h:75:13: note: 'strchr' declared here const char strchr(const char s, int c) {return libcpp_strchr(s, c);} ^ In file included from sample.cpp:1: In file included from /libcxx_symcc_install/include/c++/v1/iostream:37: In file included from /libcxx_symcc_install/include/c++/v1/ios:215: In file included from /libcxx_symcc_install/include/c++/v1/__locale:14: In file included from /libcxx_symcc_install/include/c++/v1/string:504: In file included from /libcxx_symcc_install/include/c++/v1/string_view:175: In file included from /libcxx_symcc_install/include/c++/v1/string:57: In file included from /libcxx_symcc_install/include/c++/v1/algorithm:641: /libcxx_symcc_install/include/c++/v1/cstring:72:9: error: no member named 'strncpy' in the global namespace using ::strncpy; ~~^ /libcxx_symcc_install/include/c++/v1/cstring:73:9: error: no member named 'strcat' in the global namespace; did you mean 'strchr'? using ::strcat; ~~^ /libcxx_symcc_install/include/c++/v1/string.h:75:13: note: 'strchr' declared here const char strchr(const char s, int c) {return libcpp_strchr(s, c);} ^ In file included from sample.cpp:1: In file included from /libcxx_symcc_install/include/c++/v1/iostream:37: In file included from /libcxx_symcc_install/include/c++/v1/ios:215: In file included from /libcxx_symcc_install/include/c++/v1/__locale:14: In file included from /libcxx_symcc_install/include/c++/v1/string:504: In file included from /libcxx_symcc_install/include/c++/v1/string_view:175: In file included from /libcxx_symcc_install/include/c++/v1/string:57: In file included from /libcxx_symcc_install/include/c++/v1/algorithm:641: /libcxx_symcc_install/include/c++/v1/cstring:74:9: error: no member named 'strncat' in the global namespace using ::strncat; ~~^ /libcxx_symcc_install/include/c++/v1/cstring:75:9: error: no member named 'memcmp' in the global namespace; did you mean 'memchr'? using ::memcmp; ~~^ /libcxx_symcc_install/include/c++/v1/string.h:96:13: note: 'memchr' declared here const void memchr(const void s, int c, size_t n) {return libcpp_memchr(s, c, n);} ^ In file included from sample.cpp:1: In file included from /libcxx_symcc_install/include/c++/v1/iostream:37: In file included from /libcxx_symcc_install/include/c++/v1/ios:215: In file included from /libcxx_symcc_install/include/c++/v1/locale:14: In file included from /libcxx_symcc_install/include/c++/v1/string:504: In file included from /libcxx_symcc_install/include/c++/v1/string_view:175: In file included from /libcxx_symcc_install/include/c++/v1/string:57: In file included from /libcxx_symcc_install/include/c++/v1/algorithm:641: /libcxx_symcc_install/include/c++/v1/cstring:76:9: error: no member named 'strcmp' in the global namespace; did you mean 'strchr'? using ::strcmp; ~~^ /libcxx_symcc_install/include/c++/v1/string.h:75:13: note: 'strchr' declared here const char strchr(const char s, int c) {return libcpp_strchr(s, c);} ^ fatal error: too many errors emitted, stopping now [-ferror-limit=] 20 errors generated.

(3) Lastly, I tried to build a 'sample' under C with the following code:

include

int main(int argc, char argv[]) { //char name = argv[1]; char name[100]; printf("What is your name?\n"); gets(name); if (strcmp(name, "root") == 0) printf("What is your command?\n"); else printf("Hello %s\n", name);

return 0; }

I ran symcc -o sample3 sample3.c The build is successful, but when i run it like: "echo 'aaaa' | ./sample3", nothing gets generated in the /tmp/output folder.

buntu@symcc:~$ echo 'aaaa' | ./sample3 This is SymCC running with the QSYM backend Reading program input until EOF (use Ctrl+D in a terminal)... What is your name? Hello aaaa ubuntu@symcc:~$ ls /tmp/output/ ubuntu@symcc:~$ ls -al /tmp/output/ total 12 drwxr-xr-x 1 ubuntu ubuntu 4096 Oct 2 14:10 . drwxrwxrwt 1 root root 4096 Oct 2 14:21 .. ubuntu@symcc:~$

Any suggestion as to why this is not working?

Thanks.

sebastianpoeplau commented 3 years ago

I think it's perfectly fine to create issues for these questions so that others can find the answers as well :)

(1) I first played with the sample.cpp that came with the docker file. I noticed the solution is only discovered if i provided an input with a string length equal to the value that is being compared (root). If i tried anything else such as echo 'a' or echo 'aaaaa' and pass it to the sample binary. the generated solution under /tmp/output does not contain 'root'. Is this the correct behaviour?

Yes, and I should document it better: SymCC never changes the length of the input (which is the same behavior as, for example, QSYM or S2E). We rely on the fuzzer to vary the input length. If you want to run only concolic execution, you can pick an input that is known to be long enough - in the case of the example program, SymCC will insert null characters in various positions and eventually produce a string of length 4 that leads to the interesting code path (see the helper script to automate the process of repeatedly running SymCC on a target, and #14 for some drawbacks of this approach).

(2) The second thing I tried is to compile the sample.cpp through sym++. I understand the libc++ stuff have to also be instrumented, and that the docker container have already setup and environment variable SYMCC_LIBCXX_PATH which points to "/libcxx_symcc_install". However, when i compiled the sample.cpp, i get the following error:

ubuntu@symcc:~$ sym++ -o sample sample.cpp In file included from sample.cpp:1: In file included from /libcxx_symcc_install/include/c++/v1/iostream:37: In file included from /libcxx_symcc_install/include/c++/v1/ios:214: /libcxx_symcc_install/include/c++/v1/iosfwd:189:14: error: use of undeclared identifier 'mbstate_t' typedef fpos streampos; ^ [...] fatal error: too many errors emitted, stopping now [-ferror-limit=] 20 errors generated.

So this is outside the Docker container? Could you show me the SymCC-related output of env in that shell? The errors look as if you don't have an instrumented libc++, or maybe the path isn't correct. If you want to use the system's regular libc++ instead, you can export SYMCC_REGULAR_LIBCXX=1.

(3) Lastly, I tried to build a 'sample' under C with the following code:

include

int main(int argc, char argv[]) { //char name = argv[1]; char name[100]; printf("What is your name?\n"); gets(name); if (strcmp(name, "root") == 0) printf("What is your command?\n"); else printf("Hello %s\n", name);

return 0; }

[...]

Any suggestion as to why this is not working?

This is because we currently don't have wrappers for the string-related functions in libc; see #23. My comment on the issue mentions three possible solutions; I agree that the first should be implemented at least for the most common functions (which should be really easy), but I haven't had the time yet. (Note that the C++ equivalent will work because the instrumented libc++ enables SymCC to see the internals of the string comparison; it is, unfortunately, much harder to get users to work with an instrumented libc...)

straightblast commented 3 years ago

Below is the content for 'env'. This is within the docker container created from the Dockerfile

ubuntu@symcc:~$ env AFL_CXX=clang++-10 HOSTNAME=symcc AFL_CC=clang-10 AFL_SKIP_CPUFREQ=1 PWD=/home/ubuntu LLVM_CONFIG=llvm-config-10 CXX=g++-10 HOME=/home/ubuntu LS_COLORS=rs=0:di=01;34:ln=01;36:mh=00:pi=40;33:so=01;35:do=01;35:bd=40;33;01:cd=40;33;01:or=40;31;01:mi=00:su=37;41:sg=30;43:ca=30;41:tw=30;42:ow=34;42:st=37;44:ex=01;32:.tar=01;31:.tgz=01;31:.arc=01;31:.arj=01;31:.taz=01;31:.lha=01;31:.lz4=01;31:.lzh=01;31:.lzma=01;31:.tlz=01;31:.txz=01;31:.tzo=01;31:.t7z=01;31:.zip=01;31:.z=01;31:.dz=01;31:.gz=01;31:.lrz=01;31:.lz=01;31:.lzo=01;31:.xz=01;31:.zst=01;31:.tzst=01;31:.bz2=01;31:.bz=01;31:.tbz=01;31:.tbz2=01;31:.tz=01;31:.deb=01;31:.rpm=01;31:.jar=01;31:.war=01;31:.ear=01;31:.sar=01;31:.rar=01;31:.alz=01;31:.ace=01;31:.zoo=01;31:.cpio=01;31:.7z=01;31:.rz=01;31:.cab=01;31:.wim=01;31:.swm=01;31:.dwm=01;31:.esd=01;31:.jpg=01;35:.jpeg=01;35:.mjpg=01;35:.mjpeg=01;35:.gif=01;35:.bmp=01;35:.pbm=01;35:.pgm=01;35:.ppm=01;35:.tga=01;35:.xbm=01;35:.xpm=01;35:.tif=01;35:.tiff=01;35:.png=01;35:.svg=01;35:.svgz=01;35:.mng=01;35:.pcx=01;35:.mov=01;35:.mpg=01;35:.mpeg=01;35:.m2v=01;35:.mkv=01;35:.webm=01;35:.ogm=01;35:.mp4=01;35:.m4v=01;35:.mp4v=01;35:.vob=01;35:.qt=01;35:.nuv=01;35:.wmv=01;35:.asf=01;35:.rm=01;35:.rmvb=01;35:.flc=01;35:.avi=01;35:.fli=01;35:.flv=01;35:.gl=01;35:.dl=01;35:.xcf=01;35:.xwd=01;35:.yuv=01;35:.cgm=01;35:.emf=01;35:.ogv=01;35:.ogx=01;35:.aac=00;36:.au=00;36:.flac=00;36:.m4a=00;36:.mid=00;36:.midi=00;36:.mka=00;36:.mp3=00;36:.mpc=00;36:.ogg=00;36:.ra=00;36:.wav=00;36:.oga=00;36:.opus=00;36:.spx=00;36:*.xspf=00;36: REAL_CXX=g++-10 SYMCC_LIBCXX_PATH=/libcxx_symcc_install TERM=xterm SHLVL=1 AFL_PATH=/afl PATH=/symccbuild:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin CC=gcc-10 OLDPWD=/tmp =/usr/bin/env

sebastianpoeplau commented 3 years ago

So the build issues that you asked about in (2) are inside the Docker container? That's curious - I double-checked the Docker image after reading your message, and it worked fine for me. Maybe some changes in the base image that affect SymCC? :thinking: But if building inside the container doesn't work for you, does that mean you did the experiments that you mentioned in (1) outside the container? Sorry for the confusion, I think I'm missing something...

straightblast commented 3 years ago

The first experiment was performed within docker as well. After the container was successfully built, i see a built copy of the file. I will redo the entire container later today to see I am seeing the same behaviour.

straightblast commented 3 years ago

I rebuilt docker and I can compile sample.cpp fine again.