Dr. Indradeep Ghosh, Fujitsu

Utilization and Evolution of KLEE-based Technologies for Embedded Software Testing at Fujitsu

Indradeep Ghosh
Abstract: This talk will describe the efforts on automatic software testing at Fujitsu using KLEE-based symbolic execution. Initially KLEE was extended within Fujitsu to create tests for C++ programs in a tool named KLOVER. The talk will highlight the subtle modifications to KLEE required to handle symbolic execution of C++ programs efficiently. Subsequently KLEE was customized into a tool named FSX targeting automatic unit test generation of C and C++ programs. This tool addressed some of the performance bottlenecks that were encountered while using KLEE in an industrial setting. It also implemented a novel technique for automated and fine-grained incremental generation of unit tests through minimal augmentation of an existing test suite. The technique uses iterative, incremental refinement of test-drivers and symbolic execution, guided by a diagnostics engine. Actual use case results will be provided to demonstrate the efficacy of this technique on industrial examples leading to productivity improvements and software quality improvements within Fujitsu.

Bio: Indradeep Ghosh received the Bachelor of Technology degree in Computer Science and Engineering from the Indian Institute of Technology, Kharagpur in 1993. He received the M.A. and Ph.D. degree in Electrical Engineering from Princeton University, New Jersey, USA, in 1995 and 1998 respectively. Since 1998 he has been working on various research topics at Fujitsu Laboratories of America in Sunnyvale, California, USA, where he is currently a Director leading a team of 10 researchers working on various aspects of software quality and security. He has authored or co-authored more than 50 technical articles in international journals and conferences and holds over 40 US patents. His research interests include various areas of verification, validation and testing of software and hardware systems.

Dr. Peng Li, Baidu

ConcFuzzer: An Effective Hybrid Fuzzing System Leveraging Greybox Fuzzing and Concolic Execution

Peng Li
Abstract: We present ConcFuzzer, a hybrid vulnerability detection tool which leverages greybox fuzzing and concolic execution in a complementary manner, to catch deeper bugs in C/C++ programs. Greybox fuzzing system is inexpensive and effective at catching bugs in realistic software, however, it is always prevented from exploring deeper code space by complex checks, and it may also miss some bugs which can only be exposed dependent on particular inputs. Concolic execution is more expensive and efficient to expose deeper bugs, but it suffers from scalability issues, for example, the well-known state explosion problem. By combining the strengths of the two techniques, we mitigate their weaknesses, relieving the path explosion in concolic execution and the incompleteness in fuzzing. We use AFL and KLEE, which are both state of art in greybox fuzzing and concolic execution respectively, to construct ConcFuzzer. Base on compiler instrumentation AFL is able to compute and prioritize inputs, the concrete inputs produced by AFL are used to guide concolic execution; once new inputs generated by KLEE are found, they are provided to AFL to exercise new compartments of an application. In this talk I will introduce the architecture of ConcFuzzer and KLEE’s extension we contributed to. Notably, we extended ConcFuzzer to well support fuzzing C++ programs. Our application of ConcFuzzer upon Apollo (Baidu’s open-source autonomous driving platform) proves its efficacy and effectiveness. We will further show concrete coverage stats and some vulnerability discoveries in testing well-known libraries, such as Libjpeg, mBedtLS etc.

Bio: Peng Li is a staff security scientist in Baidu X-Lab. His research lies in applying static analysis, dynamic analysis and formal verification methodologies to improve correctness, reliability and security of complex software systems. Currently he is building a system named ConcFuzzer which is a hybrid system which leverages concolic execution and greybox fuzzing.