Securing software systems via fuzz testing and verification
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 implemen...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis-Doctor of Philosophy |
| Language: | English |
| Published: |
Nanyang Technological University
2020
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/136764 |
| _version_ | 1826112156058255360 |
|---|---|
| author | Chen, Hongxu |
| author2 | Liu Yang |
| author_facet | Liu Yang Chen, Hongxu |
| author_sort | Chen, Hongxu |
| collection | NTU |
| description | 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. |
| first_indexed | 2024-10-01T03:02:21Z |
| format | Thesis-Doctor of Philosophy |
| id | ntu-10356/136764 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2024-10-01T03:02:21Z |
| publishDate | 2020 |
| publisher | Nanyang Technological University |
| record_format | dspace |
| spelling | ntu-10356/1367642020-10-28T08:40:58Z Securing software systems via fuzz testing and verification Chen, Hongxu Liu Yang School of Computer Science and Engineering yangliu@ntu.edu.sg Engineering::Computer science and engineering 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. Doctor of Philosophy 2020-01-23T02:57:24Z 2020-01-23T02:57:24Z 2019 Thesis-Doctor of Philosophy Chen, H. (2019). Securing software systems via fuzz testing and verification. Doctoral thesis, Nanyang Technological University, Singapore. https://hdl.handle.net/10356/136764 10.32657/10356/136764 en This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License (CC BY-NC 4.0). application/pdf Nanyang Technological University |
| spellingShingle | Engineering::Computer science and engineering Chen, Hongxu Securing software systems via fuzz testing and verification |
| title | Securing software systems via fuzz testing and verification |
| title_full | Securing software systems via fuzz testing and verification |
| title_fullStr | Securing software systems via fuzz testing and verification |
| title_full_unstemmed | Securing software systems via fuzz testing and verification |
| title_short | Securing software systems via fuzz testing and verification |
| title_sort | securing software systems via fuzz testing and verification |
| topic | Engineering::Computer science and engineering |
| url | https://hdl.handle.net/10356/136764 |
| work_keys_str_mv | AT chenhongxu securingsoftwaresystemsviafuzztestingandverification |