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 。