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，在顶级网络和编程语言会议上发布其研究成果，并通过将其纳入课程来教育学生开发的研究方法，从而加速研究的采用。它还将使代表性不足的群体和本科生参与研究。