The Linux kernel adopts a large number of security checks to prevent security-sensitive operations from being executed under unsafe conditions. If a security-sensitive operation is unchecked, a missing-check issue arises. Missing check is a class of severe bugs in software programs especially in operating system kernels, which may cause a variety of security issues, such as out-of-bound accesses, permission bypasses, and privilege escalations. Due to the lack of security specifications, how to automatically identify security-sensitive operations and their required security checks in the Linux kernel becomes a challenge for missing-check analysis. In this paper, we present an accurate missing-check analysis method for Linux kernel, which can automatically infer possible security-sensitive operations. Particularly, we first automatically identify all possible security check functions of Linux. Then according to their callsites, a two-direction analysis method is leveraged to identify possible security-sensitive operations. A missing-check bug is reported when the security-sensitive operation is not protected by its corresponding security check. We have implemented our method as a tool, named AMCheX, on top of the LLVM (Low Level Virtual Machine) framework and evaluated it on the Linux kernel. AMCheX reported 12 new missing-check bugs which can cause security issues. Five of them have been confirmed by Linux maintainers.

Program synthesis is an exciting topic that desires to generate programs satisfying user intent automatically. But in most cases, only small programs for simple or domain-specific tasks can be synthesized. The major obstacle of synthesis lies in the huge search space. A common practice in addressing this problem is using a domain-specific language, while many approaches still wish to synthesize programs in general programming languages. With the rapid growth of reusable libraries, component-based synthesis provides a promising way, such as synthesizing Java programs which are only composed of APIs (application programming interfaces). However, the efficiency of searching for proper solutions for complex tasks is still a challenge. Given an unfamiliar programming task, programmers would search for API usage knowledge from various coding resources to reduce the search space. Considering this, we propose a novel approach named ProSy to synthesize API-based programs in Java. The key novelty is to retrieve related knowledge from Javadoc and Stack Overflow and then construct a probabilistic reachability graph. It assigns higher probabilities to APIs that are more likely to be used in implementing the given task. In the synthesis process, the program sketch with a higher probability will be considered first; thus, the number of explored reachable paths would be decreased. Some extension and optimization strategies are further studied in the paper. We implement our approach and conduct several experiments on it. We compare ProSy with SyPet and other state-of-the-art API-based synthesis approaches. The experimental results show that ProSy reduces the synthesis time of SyPet by up to 80%.