qsym vs klee

[oneCoderMan]

the klee can't scale to real soft, I want to know why not choose qsym ?

[junxzm1990]

I fully agree QSYM is also a very good choice, but I did not see a major difference in "scalability" between KLEE and QSYM. And the truth is our klee-concolic-executor is optimized to be faster than QSYM. We are open to further discussions -:)

…

-Jun

________________________________ From: oneCoderMan <notifications@github.com> Sent: Saturday, September 26, 2020 3:40 AM To: evanmak/savior-source <savior-source@noreply.github.com> Cc: Subscribed <subscribed@noreply.github.com> Subject: [evanmak/savior-source] qsym vs klee (#10) the klee can't scale to real soft, I want to know why not choose qsym ? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub<https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fevanmak%2Fsavior-source%2Fissues%2F10&data=02%7C01%7Cjxu69%40stevens.edu%7Cdf415b763d9e4ad293b908d862089351%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637367136254924818&sdata=6%2BPHnWv75CLxKVgtMaXqrl6QH1eN7vz0QyYFyK5TS%2Bg%3D&reserved=0>, or unsubscribe<https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FABMOZAMLO5GSRLYXUURXRHDSHXAJPANCNFSM4R22JEMA&data=02%7C01%7Cjxu69%40stevens.edu%7Cdf415b763d9e4ad293b908d862089351%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637367136254934813&sdata=r1VdGtJfZybOxl5Iq6r0Ha3Tr9orv1IGHi9ztxHqan0%3D&reserved=0>.

[oneCoderMan]

thanks a lot

[oneCoderMan]

I'm new to this field。After getting crash, what kind of tools are used to analyze? Is GDB used to analyze vulnerability location?

thanks a lot again!

[evanmak]

GDB is fine. BTW, it is pretty easy to integrate QSYM into SAVIOR, we have an internal support for that, it will be released soon, stay tune!

[LebronX]

I fully agree QSYM is also a very good choice, but I did not see a major difference in "scalability" between KLEE and QSYM. And the truth is our klee-concolic-executor is optimized to be faster than QSYM. We are open to further discussions -:)
…
-Jun
________________________________ From: oneCoderMan notifications@github.com Sent: Saturday, September 26, 2020 3:40 AM To: evanmak/savior-source savior-source@noreply.github.com Cc: Subscribed subscribed@noreply.github.com Subject: [evanmak/savior-source] qsym vs klee (#10) the klee can't scale to real soft, I want to know why not choose qsym ? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fevanmak%2Fsavior-source%2Fissues%2F10&data=02%7C01%7Cjxu69%40stevens.edu%7Cdf415b763d9e4ad293b908d862089351%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637367136254924818&sdata=6%2BPHnWv75CLxKVgtMaXqrl6QH1eN7vz0QyYFyK5TS%2Bg%3D&reserved=0, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FABMOZAMLO5GSRLYXUURXRHDSHXAJPANCNFSM4R22JEMA&data=02%7C01%7Cjxu69%40stevens.edu%7Cdf415b763d9e4ad293b908d862089351%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637367136254934813&sdata=r1VdGtJfZybOxl5Iq6r0Ha3Tr9orv1IGHi9ztxHqan0%3D&reserved=0.

It surprise me that the optimized version of KLEE is even better than QSYM

[junxzm1990]

It is not that surprising: QSYM interprets every machine instruction but KLEE just interprets every LLVM IR instruction. The number of machine instructions is many times of LLVM IR instructions. I admit that QSYM's optimization will skip the symbolic execution of many instructions and interpreting a machine instruction can be faster than interpreting an LLVM IR; but these two things cannot offset the cost of the larger amount of instructions. KLEE replaces many frequently-executed library functions like fread with extremely simplified wrappers that require no interpretation, while QSYM has to interpret the instructions in the stock version of those functions. Our KLEE includes a fork-server mode (not sure if it is enabled in the released version): it can continuously run multiple seeds without repeating the linking process before the execution of the entry point (or main). There are more other factors like KLEE has a very-well optimized cache system for constraint solving.

…

-Jun

________________________________ From: LeBron <notifications@github.com> Sent: Wednesday, September 30, 2020 9:26 AM To: evanmak/savior-source <savior-source@noreply.github.com> Cc: Jun Xu <jxu69@stevens.edu>; Comment <comment@noreply.github.com> Subject: Re: [evanmak/savior-source] qsym vs klee (#10) I fully agree QSYM is also a very good choice, but I did not see a major difference in "scalability" between KLEE and QSYM. And the truth is our klee-concolic-executor is optimized to be faster than QSYM. We are open to further discussions -:) … -Jun

________________________________ From: oneCoderMan notifications@github.com<mailto:notifications@github.com> Sent: Saturday, September 26, 2020 3:40 AM To: evanmak/savior-source savior-source@noreply.github.com<mailto:savior-source@noreply.github.com> Cc: Subscribed subscribed@noreply.github.com<mailto:subscribed@noreply.github.com> Subject: [evanmak/savior-source] qsym vs klee (#10<https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fevanmak%2Fsavior-source%2Fissues%2F10&data=02%7C01%7Cjxu69%40stevens.edu%7Cfdc67208db4f4138f49d08d8655d91fe%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637370799855478340&sdata=nP5y7E2srXF2wGrgn5JC0t1ZBNxw6fkQqPhEQXlqOwc%3D&reserved=0>) the klee can't scale to real soft, I want to know why not choose qsym ? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fevanmak%2Fsavior-source%2Fissues%2F10&data=02%7C01%7Cjxu69%40stevens.edu%7Cdf415b763d9e4ad293b908d862089351%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637367136254924818&sdata=6%2BPHnWv75CLxKVgtMaXqrl6QH1eN7vz0QyYFyK5TS%2Bg%3D&reserved=0<https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fevanmak%2Fsavior-source%2Fissues%2F10&data=02%7C01%7Cjxu69%40stevens.edu%7Cfdc67208db4f4138f49d08d8655d91fe%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637370799855488339&sdata=RCT2WEhZOzFfQMTKkcZ8t6G53syDVzCdY3%2BqCmYTEic%3D&reserved=0>, or unsubscribehttps://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FABMOZAMLO5GSRLYXUURXRHDSHXAJPANCNFSM4R22JEMA&data=02%7C01%7Cjxu69%40stevens.edu%7Cdf415b763d9e4ad293b908d862089351%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637367136254934813&sdata=r1VdGtJfZybOxl5Iq6r0Ha3Tr9orv1IGHi9ztxHqan0%3D&reserved=0<https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FABMOZAMLO5GSRLYXUURXRHDSHXAJPANCNFSM4R22JEMA&data=02%7C01%7Cjxu69%40stevens.edu%7Cfdc67208db4f4138f49d08d8655d91fe%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637370799855488339&sdata=WR2XFdg0jkliW7NvCHvBbRBShzKvmRD8tDW90XEzinE%3D&reserved=0>. It surprise me that the optimized version of KLEE is even better than QSYM — You are receiving this because you commented. Reply to this email directly, view it on GitHub<https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fevanmak%2Fsavior-source%2Fissues%2F10%23issuecomment-701499781&data=02%7C01%7Cjxu69%40stevens.edu%7Cfdc67208db4f4138f49d08d8655d91fe%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637370799855498327&sdata=jX7R5bGBMIbmpTtA8KaLmQksLgt7YuxXMrxlZgC1oT4%3D&reserved=0>, or unsubscribe<https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FABMOZAJLRI66XXSDB4VQNOTSINL25ANCNFSM4R22JEMA&data=02%7C01%7Cjxu69%40stevens.edu%7Cfdc67208db4f4138f49d08d8655d91fe%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C637370799855498327&sdata=or2pklKDxe7Uzog%2Bj1RTF97dDtDRn40MPbUjT8uZm%2FI%3D&reserved=0>.

[LebronX]

I remember a paper last year evaluate the inflation rate of LLVM instruction and machine instruction and it does not look like the difference between the amount of these two kinds of instruction is that big. Perhaps KLEE's simplified version of library functions indeed saves much time.
Systematic Comparison of Symbolic Execution Systems:
Intermediate Representation and its Generation

Anyway, looking forward to the release of your optimized version of KLEE with fork-server mode.

[junxzm1990]

I remember a paper last year evaluate the inflation rate of LLVM instruction and machine instruction and it does not look like the difference between the amount of these two kinds of instruction is that big. Perhaps KLEE's simplified version of library functions indeed saves much time.
Systematic Comparison of Symbolic Execution Systems: Intermediate Representation and its Generation

Anyway, looking forward to the release of your optimized version of KLEE with fork-server mode.

That's an interesting paper, despite my experience was the difference might be larger.

We have not done a systematic comparison, but when we evaluated SAVIOR against QSYM, our KLEE can run a much larger corpus of seeds.