NeTS: Medium: Collaborative Research: Systematic Analysis of Protocol Implementations

协议实现的系统分析长期以来，互联网协议的开发和标准化一直是由“粗略共识和运行代码”的理念驱动的。这种方法的缺点是很少严格验证协议规范，即使对于属于协议验证技术能力范围内的属性也是如此。此外，该方法的“粗糙”性质意味着一些重要的设计决策不可避免地从规范中省略或定义含糊。因此，在实践中，网络协议的正确性、性能和弹性是由协议规范的供应商和开源实现隐式定义的，这些实现基于开发人员对标准文档的不同解释。这让开发人员陷入了困境：他们不确定协议规范的属性，也没有工具来推断复杂协议实现的属性。知识价值。该项目将开发一种通用方法和相关工具，使开发人员和专家用户能够系统地分析一系列协议实现上的各种属性。该方法建立在程序分析技术最新进展的基础上，采用了针对协议实现的特殊属性和需求量身定制的新颖方法。此外，该项目将实例化通用方法，并对重要任务进行新的分析，这些任务目前主要是手工的，而且非常容易出错，包括互操作性测试和随着时间的推移对状态变化的精确跟踪（例如，识别异常状态序列或表征协议复杂性）。该项目基于协议实现具有隐式内部结构的观察，该结构以状态机的形式体现了实现的关键行为属性。由于协议实现的复杂性，该状态机通常无法通过程序分析完全推断出来。为了解决这个问题，该项目将在协议实现上开发操作符，允许开发人员指定底层状态机的可伸缩和精确视图。开发人员还可以使用这些视图在实际拓扑上执行协议的目标具体执行，以便调查所考虑的特定属性。该项目的成果将是一个名为Spa的软件系统。开发人员将提供协议实现，并使用他们对协议及其感兴趣的属性的专业知识来指定适当的操作符并指导有针对性的具体执行。该项目将通过将Spa应用于之前未考虑过的几个协议分析中获得的经验来发展Spa运营商，并将从一系列运营商开始，这些运营商已经从pi的初步研究中获得信息。更广泛的影响。作为我们网络世界访问基础的协议必须可靠、抗攻击能力强，并且必须在一系列条件和动态环境中表现良好。该项目将使开发人员和专家能够系统地分析其协议的行为，并将导致部署协议的可靠性、健壮性和性能的全面改进。该项目将通过向研究人员和开发人员提供Spa，在顶级网络和编程语言会议上发布其研究成果，并通过将其纳入课程来教育学生开发的研究方法，从而加速研究的采用。它还将让代表性不足的群体和本科生参与研究。

Systematic Analysis of Protocol ImplementationsInternet protocol development and standardization has long been driven by the philosophy of 'rough consensus and running code.' The downside to this approach is that protocol specifications are rarely rigorously verified, even for properties that fall within the capabilities of protocol verification techniques. Further, the 'rough' nature of the approach means that some important design decisions are inevitably omitted from the specification or are defined ambiguously. Therefore, in practice the correctness, performance, and resilience of network protocols are implicitly defined by vendor and open-source implementations of the protocol specification, and these implementations are based upon the developers' varying interpretations of the standards document. This leaves developers in a bind: they are unsure of the properties of the protocol specification, and do not have tools to reason about the properties of complex protocol implementations.Intellectual Merit. This project will develop a general approach and an associated tool that will enable developers and expert users to systematically analyze a variety of properties on a range of protocol implementations. The approach builds upon recent advances in program analysis techniques in novel ways that are tailored towards the special properties and requirements of protocol implementations. Moreover, the project will instantiate the general approach with new analyses for important tasks that are largely manual and highly error-prone today, including interoperability testing and precise tracking of state changes over time (e.g., to identify anomalous state sequences or characterize protocol complexity).The project is based on the observation that protocol implementations have an implicit internal structure, in the form of a state machine that embodies the key behavioral properties of the implementation. Due to the complexity of protocol implementations, this state machine will typically not be completely inferable by program analysis. To address this problem, the project will develop operators on a protocol implementation that allow developers to specify scalable and precise views of the underlying state machine. Developers can additionally use these views to perform a targeted concrete execution of the protocol on a real topology in order to investigate the particular property under consideration.The outcome of the project will be a software system called Spa. Developers will provide protocol implementations and use their expertise about the protocol and its properties of interest to specify appropriate operators and guide targeted concrete execution. The project will evolve Spa operators using experiences gained from applying Spa to several protocol analyses that have not been previously considered, and will start with a set of operators that have been informed by the PIs' preliminary research.Broader Impact. The protocols that underlie access to our networked world must be reliable, robust to attacks, and must perform well over a range of conditions and in dynamic environments. This project will equip developers and experts to systematically analyze the behavior of their protocols, and will result in an overall improvement in the reliability, robustness, and performance of deployed protocols. The project will accelerate the adoption of the research by making Spa available to researchers and developers, publishing its research results in top networking and programming language conferences, and educating students on the developed research methods by incorporating them in curricula. It will also engage underrepresented groups and undergraduates in research.