Modern operating system kernels are too complex to be free of bugs. Fuzzing is a promising approach for vulnerability detection and has been applied to kernel testing. However, existing work does not consider the influence relations between system calls when generating and mutating inputs, resulting in difficulties when trying to reach into the kernel's deeper logic effectively.

Clone detection is widely exploited for software vulnerability search. The approaches based on source code analysis cannot be applied to binary clone detection because the same source code can produce significantly different binaries due to different operating systems, microprocessor architectures and compilers. In this paper, we presentBinSeeker, a cross-platform binary seeker that integrates semantic learning and emulation. With the help of the labeled semantic flow graph,BinSeekercan quickly identify$M$candidate functions that are most similar to the vulnerability from the target binary. The value of$M$is relatively large so this semantic learning procedure essentially eliminates those functions that are very unlikely to have the vulnerability. Then, semantic emulation is conducted on these$M$candidates to obtain their dynamic signature sequences. By comparing signature sequences,BinSeekerproduces top-$N$functions that exhibit most similar behavior to that of the vulnerability. With fast filtering of semantic learning and accurate comparison of semantic emulation,BinSeekerseeks vulnerability precisely with little overhead. The experiments on six widely used programs with fifteen known CVE vulnerabilities demonstrate thatBinSeekeroutperforms three state-of-the-art toolsGenius,GeminiandCACompare. Regarding search accuracy,BinSeekerachieves an MRR value of 0.65 in the target programs, whereas the MRR values byGenius,GeminiandCACompareare 0.17, 0.07 and 0.42, respectively. If we consider ranking a function with the targeted vulnerability in the top-5 as accurate,BinSeekerachieves the accuracy of 93.33 percent, while the accuracy of the other three tools is merely 33.33, 13.33 and 53.33 percent, respectively. Such accuracy is achieved with 0.27s on average to determine whether the target binary function contains a known vulnerability, and the time for the other three tools are 1.57s, 0.15s and 0.98s, respectively. Compared to the time used to manually identify the true positive vulnerability from the false positive candidates reported by Gemini, the time overhead ofBinSeekeris negligible. Evidently, the proposedBinSeekerachieves a better balance between accuracy and efficiency.

Assertions are helpful in program analysis, such as software testing and verification. The oracles encoded in the assertions help detect potential flaws and release engineers from the manually check of the reported weaknesses, which is error-prone, burdensome and time-consuming. While in practice, few engineers would write assertions during programming, and it is challenging to generate assert statements, and insert them into proper locations automatically. In this paper, we propose a statically directed assertion recommendation approach for C programs. It combines static analysis, dynamic testing, and program verification to automatically recommend and validate weakness-oriented assertions, which is defined as an assert statement used to detect program weaknesses. Firstly, we integrate a static analysis tool such as FlawFinder and some learned patterns about CWE (Common Weakness Enumeration) to report potential program flaws. Secondly, we insert the corresponding assertions into the suspicious locations of those flaws. Then, we validate the program inserted with the assertions through two methods, the first is to execute the code with some test cases generated by automatic test-case generators such as Klee and Dart, and the second is to verify the program with some automatic verifier such as CPAchecker and Smack. Finally, we report on whether those flaws could be a real weakness. Experimental results show that our approach helps to find 125 real weaknesses in open source software from Github. Furthermore, our performance in detecting static analysis' true positives can reach 81.42%.

Golang (short for Go programming language) is a fast and compiled language, which has been increasingly used in industry due to its excellent performance on concurrent programming. Golang redefines concurrent programming grammar, making it a challenge for traditional clone detection tools and techniques. However, there exist few tools for detecting duplicates or copy-paste related bugs in Golang. Therefore, an effective and efficient code clone detector on Golang is especially needed.

Formal program verification is a powerful technique to ensure the correctness of programs. To perform this technique, one oftentimes needs to manually specify assertions, which is a time-consuming and error-prone task. Generating assertions automatically can significantly improve the usability of formal program verification. To decide where an assertion is needed heavily and which value range of the variable should be checked are the most challenging parts of assertion recommendation. This paper proposes the first assertion recommendation approach for program verification. With the help of machine learning techniques, the approach automatically decides whether a program function needs to add assertions. If an assertion is needed, the approach automatically recommends a variable that is most likely to occur in this assertion. Meanwhile, a value range of the variable is suggested. Our method of assertion recommendation has been integrated into Ceagle Online (a program verifier) and evaluated on the benchmarks of SV-COMP and CProver. Our best performance in assertion necessity classification can reach 92.1192% accuracy rate, 84.2281% precision rate and 86.8512% recall rate.