Computer Science Mercury Talk
| Starts: | 14:00 31 Mar 2021 |
|---|
| Ends: | 15:00 31 Mar 2021 |
|---|
| What is it: | Seminar |
|---|
| Organiser: | Department of Computer Science |
|---|
| Who is it for: | University staff, Adults, Current University students |
|---|
| Speaker: | Kaled Alshmrany |
|---|
|
Join us for the next Computer Science Mercury Talk (online):
https://zoom.us/j/98440686007
Speaker: Kaled Alshmrany
Host: Lucas Cordeiro
Title:
FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in Network Protocol Implementations
Abstract:
Implementations of network protocols are often prone to security vulnerabilities, typically caused by developers' mistakes when accessing memory regions and dealing with arithmetic operations. This paper proposes a novel approach named FuSeBMC that combines FUzzing with Symbolic Execution via Bounded Model Checking to verify intricate properties in network protocol implementations. FuSeBMC explores and analyzes the target C programs by incrementally injecting labels to guide the symbolic execution to produce counterexamples. These counterexamples are used to produce test-cases automatically. We also exploit fuzzing to produce test-cases for the labels that symbolic execution could not produce counterexamples. As a result, FuSeBMC guides the symbolic execution and fuzzing to explore a vast region of the state-space from the target C programs. It then produces test-cases that give high-coverage for the C programs and thus raise a chance to detect bugs. The experimental results show that our approach, FuSeBMC, leads to promising results compared with other tools such as KLEE, CPAchecker, LibKluzzer, and VeriFuzz, which are state-of-the-art in the software testing field. The experiments were performed on the benchmark of the 2nd Competition on Software Testing (Test-Comp 2020) for the two categories Cover-Error and Cover-Branches. We have also evaluated an open-source implementation of the file transfer protocol. Our experimental results show that FuSeBMC can detect security vulnerabilities efficiently and effectively in C programs. In particular, FuSeBMC ranks third in the overall category of Test-Comp 2020 and finds security vulnerabilities in open-source protocol implementations, where existing approaches are unable to find them.
Speaker
Kaled Alshmrany
Role: PhD student
Organisation: University of Manchester
Travel and Contact Information
Find event
https://zoom.us/j/98440686007
