SaTC: CORE: Small: Collaborative: A New Approach to Federated Network Security

现代网络通常在本质上是联合的——即，它们是跨多个管理域的独立网络之间的互操作。例如，在许多企业中，不同的业务单元控制着网络的各种逻辑段，但共享公共资源，如路由器、防火墙和负载平衡器。在这样的联邦系统中，网络安全策略的正确实施依赖于跨多个管理域的交互。该项目正在开发使用一种专门用于网络领域的新形式的携带证明代码（PCC）在联邦网络中执行安全策略的技术。这种强制机制将确保只有经过授权的参与者才能重新配置联邦网络中的设备，并将保证组态软件保留“行为”策略，如访问控制、片隔离等。本研究的技术贡献将包括(i)为NetKAT开发PCC技术，NetKAT是一种用于SDN编程的语言，配备了健全完整的方程推理系统；以及（ii）将NetKAT PCC集成到Nexus授权语言（NAL）中，该框架提供了指定和执行分布式授权策略的方法。关键的挑战将包括如何生成、表示和转换NetKAT证明，以及如何处理动态行为，如网络配置变化和不断发展的信任模型。该项目的广泛影响包括：(1)开发开源软件，该软件将在由BTV Ignite项目主办的GENI平台上进行测试，并在佛蒙特州伯灵顿当地社区产生更广泛的影响；(2)通过与纽约州4-H和科学领导学院合作开发的高中生外展项目，为代表性不足的群体提供教育机会。

Modern networks are often federated in nature---i.e., they are an interoperation between independent networks spanning multiple administrative domains. For example, in many enterprises, different business units control various logical segments of the network, but share common resources, such as routers, firewalls, and load-balancers. In such federated systems, the correct enforcement of network security policies relies on interactions that span multiple administrative domains. This project is developing techniques for enforcing security policies in federated networks using a new form of Proof Carrying Code (PCC), specialized to the networking domain. This enforcement mechanism will ensure that only authorized actors can reconfigure devices in federated networks, and will guarantee that configuration software preserves "behavioral" policies such as access control, slice isolation, etc.The technical contributions of this research will include (i) developing PCC techniques for NetKAT, a language for SDN programming that comes equipped with a sound and complete equational reasoning system, and (ii) integrating NetKAT PCC into the Nexus Authorization Language (NAL), a framework that provides methods for specifying and enforcing distributed authorization policies. Key challenges will include how to generate, represent, and transform NetKAT proofs, and how to deal with dynamic behaviors such as network configuration changes and evolving trust models. The broader impacts of this project include (i) developing open-source software that will be tested on a GENI rack hosted by the BTV Ignite program with broader impacts in the local Burlington, VT community, and (ii) presenting education opportunities for underrepresented groups via an outreach program for high school students developed in partnership with the New York State 4-H and Science Leadership Academy.