CRII: SaTC: Analyzing and verifying the security of TCP stacks under multi-entity interactions

该项目的目标是加强传输控制协议（TCP），一个无处不在的核心互联网协议，在新兴的威胁模型下，使其足够强大和安全，以满足通信，汽车，医疗设备和其他每天接触我们生活的设备中的“智能”技术的需求。想象一下，智能汽车可能由于TCP连接上的拒绝服务攻击而无法自动报告事故，或者智能医疗设备可能无法报告患者的病情变化，这是非常可怕的。更不用说利用全球强大互联网的日益增长的网络攻击。该项目将系统地分析最近的安全漏洞的根源，并概括它们。研究结果将为如何避免这些问题提供有价值的见解。此外，该研究有望导致主要操作系统中TCP实现的变化。具体而言，该研究的动机是以下观察。首先，TCP协议栈中忽略了一些更微妙的问题，如侧信道。其次，新的威胁模型已经融合，例如，相互不信任的协同定位实体。第三，TCP的端到端假设由于网络中间盒、基于主机的防火墙和审查防火墙的流行而被打破。该研究将利用模型检查来系统地搜索各种威胁模型和网络设置下的漏洞。这些模型将从流行的操作系统（具有最新和代表性的版本）以及网络中间盒构建。它们可以作为测试和验证未来TCP堆栈实现的基础。

The objective of this project is to strengthen the Transmission Control Protocol (TCP), a ubiquitous core Internet protocol, under emerging threat models to make it robust and secure enough to serve the needs of 'smart' technologies in communications, automobiles, medical devices, and other devices that touch our lives every day. It is terrifying to imagine that a smart car could fail to report an accident automatically due to a denial of service attack on its TCP connections, or a smart medical device could fail to report a patient's change in condition. This is not to mention the ever growing cyber attacks that leverage the global and powerful Internet. This project will systematically analyze the root causes of recent security vulnerabilities and generalize them. The results will offer valuable insights on how to avoid the problems. Further, the research is expected to lead to changes to the TCP implementations in major operating systems.Specifically, the research is motivated by the following observations. First, more subtle problems such as side channels have been overlooked in TCP stacks. Second, new threat models have merged, e.g., co-located entities that do not trust each other. Third, the end-to-end assumption of TCP is broken due to the prevalence of network middleboxes, host-based firewalls, and censorship firewalls. The research will leverage model checking to systematically search for vulnerabilities under a variety of threat models and network settings. The models will be constructed from popular operating systems (with recent and representative versions) as well as network middleboxes. They can serve as the basis for testing and verifying future TCP stack implementations.