Securing software systems via fuzz testing and verification

• Main Author: Chen, Hongxu
• Other Authors: Liu Yang
• Format: Thesis-Doctor of Philosophy
• Language: English
• Published: Nanyang Technological University 2020
• Subjects: Engineering::Computer science and engineering
• Online Access: https://hdl.handle.net/10356/136764
• Institution: Nanyang Technological University

Software security has been growing in importance due to the increasing reliance on various systems such as computers, smartphones, and Internet-of-Things devices. Security weaknesseses, or vulnerabilities, range in various aspects, from the systematic levels such as designing defects, to implementation errors such as language-specific program crashes. The multifaceted nature of vulnerabilities poses significant challenges to secure different systems. In fact, multilevel approaches have to be applied to reveal vulnerabilities or solidify the systems. Generally, there are two categories of approaches to securing a system, namely testing and verification. The former tries to generate test cases to trigger erroneous behaviors in the underlying programs. The latter models the system in an abstracted description to prove the absence of certain security defects. In this thesis, we will describe our efforts in greybox fuzz testing and type checking based verification in securing different levels of software systems. Firstly, we apply greybox fuzz testing (or fuzzing) to detect implementation vulnerabilities. These vulnerabilities are usually subtle that it is rather complicated to formally verify the absence of the corresponding defects. We target on two levels of vulnerabilities. One is to improve the fuzzing directedness of executing towards specific target program locations to reveal crash induced vulnerabilities such as buffer-overflow, use-after-free, etc. To emphasize existing challenges in directed fuzzing, we propose Hawkeye to feature four desired properties for directedness. With the statically analyzed results on the target program and its target locations, Hawkeye applies multiple dynamic strategies for seed prioritization, power scheduling and mutation. The experimental results on various real-world programs showed that Hawkeye significantly outperforms the state-of-the-art greybox fuzzers AFL and AFLGo in reaching target locations and reproducing specific crashes. The other scenario is to enhance fuzzing to reveal multithreading-relevant bugs. These bugs may root from logic errors which exhibit abnormal behaviors in the target program. They may or may not cause immediate crashes however implicate certain security defects. We present Doublade, a novel thread-aware technique which effectively generates multithreading-relevant seeds. Doublade relies on a set of thread-aware techniques, consisting of a stratified exploration-oriented instrumentation and two complementary instrumentations, as well as dynamic adaptive strategies based on feedbacks. Experiments on 12 real-world programs showed that Doublade significantly outperforms the state-of-the-art fuzzer AFL in generating high-quality seeds, detecting vulnerabilities, and exposing concurrency bugs. To integrate Hawkeye , Doublade, and other recently proposed fuzzing techniques, we have built our own general-purpose fuzzing framework, Fuzzing Orchestration Toolkit (FOT). Compared to other fuzzing frameworks, FOT is versatile in its functionalities and can be easily configured or extended for various fuzzing purposes. Till now, FOT has detected 200+ zero-day vulnerabilities in more than 40 world-famous projects, among which 51 CVEs have been assigned. Secondly, we apply type checking based verification to detect those vulnerabilities introduced by designing defects where testing usually fails to reveal. Particularly, we focus on the information leakage vulnerability caused by inter-app communications on an Android system. We propose a lightweight security type system that models permission mechanism on Android, where the permissions are assigned statically and facilitated to enforce access control across applications. We proved the soundness of the proposed type system in terms of non-interference, with which we are able to prove the absence of information leakage among various apps in an Android system. We also presented a deterministic type inference algorithm for the underlying type system. Finally, based on these attempts we have made so far, we briefly discuss the differ- ences between the two categories of applied approaches in terms of the capability, the practicality, and their potential combinations in securing modern software systems.