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.