We present a rigorous framework for automatically testing application-layer protocols. The key innovation is a domain-specific embedded language for writing nondeterministic models of the behavior of networked servers. These models are defined in Gallina, the language of the Coq interactive theorem prover, supporting a smooth transition from testing to formal verification. Given a server model, we show how to automatically derive a testing program that probes the server for unexpected behaviors. We address the uncertainties caused by both the server's internal choices and the network delaying messages nondeterministically. The derived tester accepts server implementations whose possible behaviors are a subset of those allowed by the nondeterministic model. We demonstrate the effectiveness of this framework by using it to specify and test a fragment of HTTP/1.1, showing that the automatically derived tester can capture RFC violations in buggy server implementations, including the latest versions of Apache and Nginx.


翻译:我们为自动测试应用程序层协议提出了一个严格的框架。 关键的创新是用于撰写网络服务器行为非决定性模型的域内嵌入语言。 这些模型在Coq互动理论验证器的语言Gallina中定义, 支持从测试向正式验证的平稳过渡。 在服务器模型中, 我们展示了如何自动生成一个检测服务器意外行为的测试程序。 我们处理服务器内部选择和网络不肯定地拖延信息造成的不确定性。 衍生的测试器接受服务器实施, 其可能的行为是非定义模型允许的行为的一部分。 我们通过使用它来指定和测试 HTTPP/1.1的碎片来展示这一框架的有效性, 显示自动生成的测试器可以捕捉到服务器执行错误的 RFC 违规现象, 包括最新版本的 Apache 和 Nginx 。

0
下载
关闭预览

相关内容

Networking:IFIP International Conferences on Networking。 Explanation:国际网络会议。 Publisher:IFIP。 SIT: http://dblp.uni-trier.de/db/conf/networking/index.html
如何构建你的推荐系统?这份21页ppt教程为你讲解
专知会员服务
64+阅读 · 2021年2月12日
专知会员服务
39+阅读 · 2020年9月6日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
大数据 | 顶级SCI期刊专刊/国际会议信息7条
Call4Papers
10+阅读 · 2018年12月29日
Ray RLlib: Scalable 降龙十八掌
CreateAMind
9+阅读 · 2018年12月28日
医学 | 顶级SCI期刊专刊/国际会议信息4条
Call4Papers
5+阅读 · 2018年12月28日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
【推荐】深度学习目标检测全面综述
机器学习研究会
21+阅读 · 2017年9月13日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
0+阅读 · 2021年3月24日
VIP会员
相关VIP内容
如何构建你的推荐系统?这份21页ppt教程为你讲解
专知会员服务
64+阅读 · 2021年2月12日
专知会员服务
39+阅读 · 2020年9月6日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
相关资讯
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
大数据 | 顶级SCI期刊专刊/国际会议信息7条
Call4Papers
10+阅读 · 2018年12月29日
Ray RLlib: Scalable 降龙十八掌
CreateAMind
9+阅读 · 2018年12月28日
医学 | 顶级SCI期刊专刊/国际会议信息4条
Call4Papers
5+阅读 · 2018年12月28日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
【推荐】自然语言处理(NLP)指南
机器学习研究会
35+阅读 · 2017年11月17日
【推荐】深度学习目标检测全面综述
机器学习研究会
21+阅读 · 2017年9月13日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员