SBIR Phase I: Dynamic Data-Plane Verification in Heterogeneous Networks

SBIR 第一阶段：异构网络中的动态数据平面验证

• 批准号: 1315095
• 负责人: Serena Chan
• 金额: $ 15万
• 依托单位: Veriflow Systems
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-07-01 至 2013-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1315095&HistoricalAwards=false
• 关键词: SBIR; Phase; Dynamic; Data; Plane

The innovation of this work is a platform for automatic verification of network behavior. Every aspect of our society is now tightly intertwined with the functioning of computer networks such as the Internet. Unfortunately, modern networks are also extremely complex, leading to a rich variety of failure modes and outages. These errors have very high costs for businesses, including lost revenue and customers, fines from violating regulations such as HIPAA, leaks of sensitive information, and decline in corporate image. Automated tools to help operators by verifying network-wide correctness do not exist. To address this need, Veriflow will build a system, which automatically verifies security and correctness of computer networks in real time, discovers vulnerabilities, and assists network operators in determining their cause. Veriflow functions by scanning a network, constructing a formal model of the network's behavior, and using custom formal logic algorithms to automatically derive whether the network contains faults. Veriflow's algorithms are real-time, able to vet networks continuously as the network state evolves, detect transient errors and signal immediate alarms, and scale to large and highly dynamic environments.The broader/commercial impact of Veriflow's work will significantly enhance reliability and security of critical network infrastructure, and ease network management tasks. The strong formal foundations of our tool coupled with its high-speed and advanced scaling properties will enable us to gain an important part of this emerging market. The company's past research has demonstrated potential of the system through two working prototypes, which have found 23 real bugs in a campus deployment serving over 70,000 machines, and perform real-time network-wide verification within one millisecond. Veriflow's work will produce new tools and implementations which Veriflow will make freely available for non-commercial use. Veriflow also hopes this work will serve towards enabling interdisciplinary research across formal methods and networking, with the common goal of enabling highly available networking infrastructures. Veriflow will work with the University of Illinois CITES group to deploy the system in their campus network, and in the Urbana-Champaign Big Broadband (UC2B) network, a community broadband project to provide gigabit fiber-to-the-premise to 2700 under-served residences and 350 community anchor institutions. Veriflow has also established working relationships with several large companies that serve large user populations as well as provide outreach to academic and research institutions.

这项工作的创新之处在于一个自动验证网络行为的平台。我们社会的每一个方面现在都与计算机网络的功能紧密地交织在一起，比如互联网。不幸的是，现代网络也非常复杂，导致各种各样的故障模式和中断。这些错误会给企业带来很高的成本，包括收入和客户的损失、违反HIPAA等法规的罚款、敏感信息的泄露以及企业形象的下降。目前还不存在通过验证网络范围内的正确性来帮助操作员的自动化工具。为了满足这一需求，Veriflow将建立一个系统，该系统可以实时自动验证计算机网络的安全性和正确性，发现漏洞，并帮助网络运营商确定其原因。通过扫描网络，构建网络行为的形式化模型，并使用自定义的形式化逻辑算法自动导出网络是否存在故障来验证功能。Veriflow的算法是实时的，能够随着网络状态的发展不断审查网络，检测瞬态错误并发出即时警报，并扩展到大型和高度动态的环境。Veriflow的广泛/商业影响将显著提高关键网络基础设施的可靠性和安全性，并简化网络管理任务。我们的工具强大的正式基础，加上其高速和先进的缩放特性，将使我们能够在这个新兴市场中获得重要的一部分。该公司过去的研究已经通过两个工作原型展示了该系统的潜力，这两个原型在为7万多台机器提供服务的校园部署中发现了23个真正的错误，并在一毫秒内进行了实时的全网验证。Veriflow的工作将产生新的工具和实现，Veriflow将免费提供给非商业用途。Veriflow还希望这项工作将有助于实现跨正式方法和网络的跨学科研究，其共同目标是实现高度可用的网络基础设施。Veriflow将与伊利诺伊大学CITES小组合作，在其校园网络和厄巴纳-香槟大宽带（UC2B）网络中部署该系统，这是一个社区宽带项目，为2700个服务不足的住宅和350个社区固定机构提供千兆光纤到户。Veriflow还与几家大公司建立了合作关系，这些公司为大量用户提供服务，并为学术和研究机构提供外联服务。