CPFuzz: Combining Fuzzing and Falsification of Cyber-Physical Systems
Coverage-guided grey-box fuzzing for computer systems has been explored for decades. However, existing techniques do not adequately explore the space of continuous behaviors in Cyber-Physical Systems (CPSs), which may miss safety-critical bugs. Optimization-guided falsification is promising to find...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2020-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/9193936/ |
| _version_ | 1818624230996049920 |
|---|---|
| author | Fute Shang Buhong Wang Tengyao Li Jiwei Tian Kunrui Cao |
| author_facet | Fute Shang Buhong Wang Tengyao Li Jiwei Tian Kunrui Cao |
| author_sort | Fute Shang |
| collection | DOAJ |
| description | Coverage-guided grey-box fuzzing for computer systems has been explored for decades. However, existing techniques do not adequately explore the space of continuous behaviors in Cyber-Physical Systems (CPSs), which may miss safety-critical bugs. Optimization-guided falsification is promising to find violations of safety specifications, but not suitable for identifying traditional program bugs. This article presents a fuzzing process for finding safety violations at the development phase, which is guided by two quantities: a branch coverage metric to explore discrete program behaviors and a Linear Temporal Logic (LTL) robust satisfaction metric to identify undesirable continuous plant behaviors. We implement CPFuzz to demonstrate the utility of the idea and estimate its effectiveness on seven control system benchmarks. The results show up to a better performance in average time to find violations on all benchmarks than S-TaLiRo and six benchmarks than S3CAMX. Finally, we exploit CPFuzz to synthesize the sensor spoofing attack on a DC motor with fixed-point overflow vulnerability as a case study. |
| first_indexed | 2024-12-16T18:53:40Z |
| format | Article |
| id | doaj.art-f1ae1c09aff44f87b14fd17a7bb76828 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-16T18:53:40Z |
| publishDate | 2020-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-f1ae1c09aff44f87b14fd17a7bb768282022-12-21T22:20:36ZengIEEEIEEE Access2169-35362020-01-01816695116696210.1109/ACCESS.2020.30232509193936CPFuzz: Combining Fuzzing and Falsification of Cyber-Physical SystemsFute Shang0https://orcid.org/0000-0002-1169-6643Buhong Wang1https://orcid.org/0000-0001-7425-0502Tengyao Li2https://orcid.org/0000-0001-6921-6174Jiwei Tian3https://orcid.org/0000-0002-1485-7465Kunrui Cao4https://orcid.org/0000-0001-6021-8798School of Information and Navigation, Air Force Engineering University, Xi’an, ChinaSchool of Information and Navigation, Air Force Engineering University, Xi’an, ChinaSchool of Information and Navigation, Air Force Engineering University, Xi’an, ChinaSchool of Information and Navigation, Air Force Engineering University, Xi’an, ChinaSchool of Information and Navigation, Air Force Engineering University, Xi’an, ChinaCoverage-guided grey-box fuzzing for computer systems has been explored for decades. However, existing techniques do not adequately explore the space of continuous behaviors in Cyber-Physical Systems (CPSs), which may miss safety-critical bugs. Optimization-guided falsification is promising to find violations of safety specifications, but not suitable for identifying traditional program bugs. This article presents a fuzzing process for finding safety violations at the development phase, which is guided by two quantities: a branch coverage metric to explore discrete program behaviors and a Linear Temporal Logic (LTL) robust satisfaction metric to identify undesirable continuous plant behaviors. We implement CPFuzz to demonstrate the utility of the idea and estimate its effectiveness on seven control system benchmarks. The results show up to a better performance in average time to find violations on all benchmarks than S-TaLiRo and six benchmarks than S3CAMX. Finally, we exploit CPFuzz to synthesize the sensor spoofing attack on a DC motor with fixed-point overflow vulnerability as a case study.https://ieeexplore.ieee.org/document/9193936/Coverage guided fuzzingcyber-physical systemslinear temporal logicoptimization-guided falsification |
| spellingShingle | Fute Shang Buhong Wang Tengyao Li Jiwei Tian Kunrui Cao CPFuzz: Combining Fuzzing and Falsification of Cyber-Physical Systems IEEE Access Coverage guided fuzzing cyber-physical systems linear temporal logic optimization-guided falsification |
| title | CPFuzz: Combining Fuzzing and Falsification of Cyber-Physical Systems |
| title_full | CPFuzz: Combining Fuzzing and Falsification of Cyber-Physical Systems |
| title_fullStr | CPFuzz: Combining Fuzzing and Falsification of Cyber-Physical Systems |
| title_full_unstemmed | CPFuzz: Combining Fuzzing and Falsification of Cyber-Physical Systems |
| title_short | CPFuzz: Combining Fuzzing and Falsification of Cyber-Physical Systems |
| title_sort | cpfuzz combining fuzzing and falsification of cyber physical systems |
| topic | Coverage guided fuzzing cyber-physical systems linear temporal logic optimization-guided falsification |
| url | https://ieeexplore.ieee.org/document/9193936/ |
| work_keys_str_mv | AT futeshang cpfuzzcombiningfuzzingandfalsificationofcyberphysicalsystems AT buhongwang cpfuzzcombiningfuzzingandfalsificationofcyberphysicalsystems AT tengyaoli cpfuzzcombiningfuzzingandfalsificationofcyberphysicalsystems AT jiweitian cpfuzzcombiningfuzzingandfalsificationofcyberphysicalsystems AT kunruicao cpfuzzcombiningfuzzingandfalsificationofcyberphysicalsystems |