SBIR Phase II: Reliable and Efficient Data-Plane Verification

这个小型企业创新研究（SBIR）第二阶段项目的更广泛的影响/商业潜力将大大提高关键网络基础设施的可靠性和安全性，并简化网络管理任务。通过在实时网络上的多次试点部署，该公司软件工具的原型版本发现了一些现有最先进的审计技术和监控工具所遗漏的严重错误和漏洞，并且能够在短短一毫秒内执行实时网络范围的验证。当在该项目下得到更充分的开发时，该公司的技术将有助于确保高度可用的网络基础设施。为此，该公司将与厄巴纳-香槟大宽带（UC 2B）合作，这是一个社区网络，预计将为2700个服务不足的住宅和350个社区锚机构提供千兆光纤到户。该公司还将与全球网络创新环境（GENI）合作，该环境正在建立一个协作网络环境，以促进新兴全球网络的突破性发现和创新。这个小型企业创新研究（SBIR）第二阶段项目将继续开发和商业化的新方法来分析和保护计算机网络。我们社会的每一个方面，从商业到政府，再到医学和科学，现在都与互联网等计算机网络的功能紧密交织在一起。然而，现代网络极其复杂，导致各种各样的故障模式和中断。这些错误可能会导致企业付出高昂的成本，包括SLA带来的收入损失、客户和合同的流失、违反HIPAA等法规的罚款、敏感信息的泄露以及企业形象的下降。为了应对这一挑战，该公司正在构建一个系统，该系统可以实时自动验证计算机网络的安全性和正确性，发现漏洞，并协助网络运营商确定其原因。该技术通过扫描网络，构建网络行为的形式模型，并使用自定义形式逻辑算法来自动确定网络是否包含故障。它可以随着网络状态的发展不断检查网络，检测瞬时错误并发出即时警报，并扩展到大型和高度动态的环境。其目的是向网络运营商提供即时的实际援助。

The broader impact/commercial potential of this Small Business Innovation Research (SBIR) Phase II project will be to significantly enhance reliability and security of critical network infrastructure, and ease network management tasks. Through multiple pilot deployments on live networks, a prototype version of the company's software tool has found a number of serious errors and vulnerabilities that were missed by existing state-of-the-art auditing techniques and monitoring tools, and was able to perform real-time network-wide verification within as little as one millisecond. When more fully developed under this project, the company's technology will help ensure highly available networking infrastructures. To this end the company will work with Urbana-Champaign Big Broadband (UC2B), a community network expected to provide gigabit fiber-to-the-premise to 2700 under-served residences and 350 community anchor institutions. The company will also work with the Global Environment for Network Innovations (GENI), which is building a collaborative network environment to catalyze groundbreaking discoveries and innovation in emerging global networks. This Small Business Innovation Research (SBIR) Phase II project will continue the development and commercialization of a new approach to analyzing and protecting computer networks. Every aspect of our society, from business, to government, to medicine and the sciences, is now tightly intertwined with the functioning of computer networks such as the Internet. However, modern networks are extremely complex, leading to a rich variety of failure modes and outages. These errors can result in very high costs for businesses, including lost revenue from SLAs, lost customers and contracts, fines for violating regulations such as HIPAA, leaks of sensitive information, and decline in corporate image. To address this challenge, the company is building a system that automatically verifies security and correctness of computer networks in real-time, discovers vulnerabilities, and assists network operators in determining their cause. The technology functions by scanning a network, constructing a formal model of the network's behavior, and using custom formal logic algorithms to automatically determine whether the network contains faults. It can vet networks continuously as the network state evolves, detect transient errors and signal immediate alarms, and scale to large and highly dynamic environments. It is intended to provide immediate practical assistance to network operators.