Improving Protocol Standards for a more Trustworthy Internet

该项目将通过改进网络设计的工程流程，使互联网的基础设施和应用程序更可靠、更安全、更值得信赖、更不容易受到网络攻击。互联网由大量笔记本电脑、智能手机和其他边缘设备组成，通过大量互联链路和交换设备连接到位于世界各地数据中心的服务器。要做到这一点，所有的设备必须就它们应该如何通信达成一致。也就是说，它们必须使用一种公共语言，称为“协议”，它描述了发送的信息格式和要执行的操作。有许多这样的协议，描述了不同类型的通信。例如，HTTP协议描述了浏览器如何从网站获取页面。为了确保来自不同制造商的设备之间的互操作性，这些协议在一系列标准文件中进行了描述，这些标准文件由互联网工程任务组(IETF)等组织发布。这些标准是由工程师团队在几个月甚至几年的时间里逐步开发的，以产生描述协议应该如何工作的书面规范。然而，尽管制定标准的人尽了最大努力，但结果往往包含不一致和模棱两可的地方。这可能会导致不同制造商的设备无法协同工作，因为对标准的不同解释，在最糟糕的情况下，可能会导致漏洞，使设备面临网络攻击。这些不一致和模棱两可的原因很大程度上是因为协议标准是用英语编写的，因此没有自动检查其正确性的方法。研究人员提出了使用更像计算机编程语言的方法(称为“形式语言”)来描述协议的方法，这将允许进行自动化的一致性检查，但这些方法尚未被标准界广泛采用。该项目将研究采用这些新技术的社会、文化和教育障碍，以了解为什么标准继续用英语编写。我们将探索可选方案的明显局限性，以了解为什么它们在某些特定领域和特定目的中被采用，但在标准开发中没有被更广泛地使用。然后，我们将在协议标准社区中制定一个采用正式语言及其支持工具的模型，并使用它来确定准备在其标准中增加此类技术使用的领域。最后，我们将使用获得的知识来提出正式语言，这些语言旨在适应标准开发人员的工作方式，并开始将这些语言引入标准过程，以改进协议规范，使其不容易受到攻击。工作将在IETF进行，因为它是制定互联网协议标准的关键国际技术标准机构。其目的是提高IETF开发的标准的质量和可信度，并增加互联网的安全性、健壮性和互操作性。我们将探索的新的工程学研究思想是，形式语言需要适应感兴趣的社区。然而，它们不能帮助解决如何指定协议的技术问题：它们必须以一种适合需要使用它们的人的专业知识和文化的方式来这样做。对协议设计的结构化方法和正式语言的研究尚未考虑到标准过程的性质，因此没有得到广泛的理解。我们从对标准过程的深刻认识入手，考虑了社会和技术障碍，并提出了改进标准制定方式的新技术。

This project will make the Internet's infrastructure and applications morereliable and secure, more trustworthy and less vulnerable to cyber attack,by improving the engineering processes by which the network is designed.The Internet comprises a large number of laptops, smartphones, and otheredge devices, connecting to servers located in data centres around theworld via numerous interconnecting links and switching devices. To makethis work, all the devices must agree on how they should communicate. Thatis, they must speak a common language, known as a "protocol" that describesthe format of the information that is sent and the operations to beperformed. There are many such protocols, describing the different types of communication. For example, the HTTP protocol describes how browsersfetch pages from websites.To ensure interoperability between devices from different manufacturers,these protocols are described in a series of standards documents, publishedby organisations such as the Internet Engineering Task Force (IETF). Thesestandards are developed incrementally by teams of engineers working overseveral months, or perhaps years, to produce a written specification thatdescribes how the protocol should work. Despite the best efforts of thosedeveloping the standards, however, the results are often found to containinconsistencies and ambiguities. These can lead to devices from differentmanufacturers failing to work together, due to differing interpretations ofthe standard, and in the worst cases can lead to vulnerabilities that opendevices up to cyber attack.Much of the reason for these inconsistencies and ambiguities is that theprotocol standards are written in English, and hence there's no automatedway of checking them for correctness. Researchers have proposed ways ofdescribing protocols using methods (known as "formal languages") that aremore like computer programming languages, and that would allow automatedconsistency checks to be made, but these have not been widely adopted bythe standards community. This project will study the social, cultural, and educational barriers toadoption of these new techniques, to understand why standards continue tobe written in English. We will explore the perceived limitations of thealternatives, to understand why they've been adopted in certain niches, and for certain purposes, but are not used more broadly in standardsdevelopment.We'll then formulate a model for the adoption of formal languages and theirsupporting tools in the protocol standards community, and use it identifyareas that are ready to increase use of such techniques in their standards.Finally, we'll use the knowledge gained to propose formal languages, thatare designed to fit the way the standards developers work, and begin theprocess of introducing these into the standards process, to improveprotocol specifications and make them less vulnerable to attack.The work will be conduced in the IETF, since it's the key internationaltechnical standards body developing Internet protocol standards. The aim isto improve the quality and trustworthiness of the standards that the IETFdevelops, and increase security, robustness, and interoperability of theInternet. The novel engineering research idea we will explore is thatformal languages need to be adapted to the community of interest. It is notenough that they help solve the technical problem of how to specify aprotocol: they must do so in a way that fits the expertise and culture ofthose who need to use them. Research into structured approaches and formallanguages for protocol design has not yet considered the nature of thestandards process, and hence has not seen wide uptake. We start with a deepawareness of the standards process, consider social and technical barriersto uptake, and propose new techniques to improve the way standards aredeveloped.