Software model checking is a verification technique which is widely used for checking temporal properties of software systems. Even though it is a property verification technique, its common usage in practice is in "bug finding", that is, finding violations of temporal properties. Motivated by this observation and leveraging the recent progress in fuzzing, we build a greybox fuzzing framework to find violations of Linear-time Temporal Logic (LTL) properties. Our framework takes as input a sequential program written in C/C++, and an LTL property. It finds violations, or counterexample traces, of the LTL property in stateful software systems; however, it does not achieve verification. Our work substantially extends directed greybox fuzzing to witness arbitrarily complex event orderings. We note that existing directed greybox fuzzing approaches are limited to witnessing reaching a location or witnessing simple event orderings like use-after-free. At the same time, compared to model checkers, our approach finds the counterexamples faster, thereby finding more counterexamples within a given time budget. Our LTL-Fuzzer tool, built on top of the AFL fuzzer, is shown to be effective in detecting bugs in well-known protocol implementations, such as OpenSSL and Telnet. We use LTL-Fuzzer to reproduce known vulnerabilities (CVEs), to find 15 zero-day bugs by checking properties extracted from RFCs (for which 10 CVEs have been assigned), and to find violations of both safety as well as liveness properties in real-world protocol implementations. Our work represents a practical advance over software model checkers -- while simultaneously representing a conceptual advance over existing greybox fuzzers. Our work thus provides a starting point for understanding the unexplored synergies between software model checking and greybox fuzzing.


翻译:软件模式检查是一种核查技术, 它被广泛用于检查软件系统的时间属性。 尽管它是一种财产核查技术, 它在实际中通常的使用是“ 错误发现”, 也就是说, 发现侵犯时间属性的行为。 受此观察的驱使, 利用最近在模糊化方面的进展, 我们建立了一个灰盒模糊框架, 以查找违反线形时时时时逻辑( LTL) 属性的行为。 我们的框架将C/ C+++ 和一个 LTL 属性的相继程序作为输入。 它在状态化软件系统中发现LTL 属性的违规或反例迹; 但是, 它没有实现核查。 我们的工作大大扩展了灰盒的模糊模糊, 以见证任意复杂的事件。 我们注意到, 现有的Greedbox flzz 模糊方法仅限于看到到达一个位置, 或见证简单事件, 类似“ 免费” 。 与此同时, 我们的模型找到反光碟软件格式, 从而在特定预算中找到更多的反镜; 我们的LTL- Fzer 运行工具, 代表了我们所知道的“ 常规” 。

0
下载
关闭预览

相关内容

ACM/IEEE第23届模型驱动工程语言和系统国际会议,是模型驱动软件和系统工程的首要会议系列,由ACM-SIGSOFT和IEEE-TCSE支持组织。自1998年以来,模型涵盖了建模的各个方面,从语言和方法到工具和应用程序。模特的参加者来自不同的背景,包括研究人员、学者、工程师和工业专业人士。MODELS 2019是一个论坛,参与者可以围绕建模和模型驱动的软件和系统交流前沿研究成果和创新实践经验。今年的版本将为建模社区提供进一步推进建模基础的机会,并在网络物理系统、嵌入式系统、社会技术系统、云计算、大数据、机器学习、安全、开源等新兴领域提出建模的创新应用以及可持续性。 官网链接:http://www.modelsconference.org/
专知会员服务
17+阅读 · 2020年9月6日
专知会员服务
60+阅读 · 2020年3月19日
深度强化学习策略梯度教程,53页ppt
专知会员服务
178+阅读 · 2020年2月1日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
无监督元学习表示学习
CreateAMind
27+阅读 · 2019年1月4日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
LibRec 精选:连通知识图谱与推荐系统
LibRec智能推荐
3+阅读 · 2018年8月9日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
【论文】图上的表示学习综述
机器学习研究会
14+阅读 · 2017年9月24日
【推荐】SVM实例教程
机器学习研究会
17+阅读 · 2017年8月26日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Arxiv
0+阅读 · 2022年2月6日
Arxiv
0+阅读 · 2022年2月4日
Arxiv
0+阅读 · 2022年2月3日
Arxiv
5+阅读 · 2018年4月22日
VIP会员
相关资讯
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
无监督元学习表示学习
CreateAMind
27+阅读 · 2019年1月4日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
LibRec 精选:连通知识图谱与推荐系统
LibRec智能推荐
3+阅读 · 2018年8月9日
【计算机类】期刊专刊/国际会议截稿信息6条
Call4Papers
3+阅读 · 2017年10月13日
【论文】图上的表示学习综述
机器学习研究会
14+阅读 · 2017年9月24日
【推荐】SVM实例教程
机器学习研究会
17+阅读 · 2017年8月26日
强化学习 cartpole_a3c
CreateAMind
9+阅读 · 2017年7月21日
Top
微信扫码咨询专知VIP会员