协议一致性测试

我们基于SIGCOMM 2019论文《QUIC的形式化规范和测试》中方法进行协议一致性测试。我们对其形式化规范进行了升级以支持QUIC v1，同时解决了ivy工具链存在的问题。

QUIC形式化规范

QUIC协议的形式化规范基于Ivy语言编写。该形式化规范可用于组合式基于规范的测试方法，来测试QUIC实现。

目前支持的版本是IETF QUIC v1。

工作原理

QUIC的形式化规范采用了专门的编写方式，允许在网络上监视数据包，以及对QUIC实现进行模块化测试。

也就是说，我们可以根据规范，生成的自动化测试程序，作为客户端或服务端角色。测试程序使用符号执行和SMT求解器随机生成符合规范的协议流量。例如，如果测试程序扮演客户端角色，那么它将生成客户端可以发送的合法数据包，并将这些数据包发送到被测试的服务器。然后检查服务器回复的响应是否符合规范。

优势

与互操作性测试相比，这种方法有一定的优势。

• 基于规范的测试程序可以生成任何当前实现无法产生的报文序列，可能只会由攻击者产生。因为它是随机的，它倾向于生成规范制定者可能没有考虑到的不寻常情况。

• 它可以检查实际的规范符合性，而不仅仅是正确的互操作。 对于未来需要确保与遗留实现兼容的协议开发人员来说，遵守规范非常重要。

• 形式化规范可以看作是文档，因为它对使用自然语言编写的IETF规范文档给出了明确的解释。

使用方法

我们计划开源QUIC v1的形式化规范，在其项目文档中将详细说明使用方法。