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

NeTS：媒介：协作研究：协议实现的系统分析

• 批准号: 1161595
• 负责人: Todd Millstein
• 金额: $ 44.69万
• 依托单位: University of California-Los Angeles
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-05-01 至 2017-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1161595&HistoricalAwards=false
• 关键词: NeTS; Medium; Collaborative; Research; Systematic

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.

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