In network management, when it comes to security breaches, human error constitutes a dominant factor. We present our tool topoS which automatically synthesizes low-level network configurations from high-level security goals. The automation and a feedback loop help to prevent human errors. Except for a last serialization step, topoS is formally verified with Isabelle HOL, which prevents implementation errors. In a case study, we demonstrate topoS by example. For the first time, the complete transition from high-level security goals to both firewall and SDN configurations is presented.
Craven al @cite_0 present a generalized (not network-specific) process to translate access control policies, enhanced with several aspects, to enforceable device-specific policies; the implementation requires a model repository of box semantics and their interplay. Pahl delivers a data-centric, network-specific approach for managing and implementing such a repository, further focusing on things @cite_9 . FortNOX @cite_22 horizontally enhances the access control abstraction as it assures that rules by security apps are not overwritten by other apps. Technically, it hooks up at the access control interface abstraction translation. Kinetic @cite_25 is an SDN language which lifts static policies (as constructed by ) to dynamic policies. To accomplish this, an administrator can define a simple FSM which dynamically (triggered by network events) switches between static policies. In addition, the FSM can be verified with a model checker. Features are horizontally added to the interface abstraction: a routing policy allows specifying of network traffic @cite_6 . Merlin @cite_24 additionally supports bandwidth assignments and network function chaining. Both translate from a global policy to local enforcement and Merlin provides a feature-rich language for interface abstraction policies.
@cite_22 @cite_9 @cite_6 @cite_0 @cite_24 @cite_25
2137845741 1591487020 2106863923 2539478360 2021234005 2163593754
Software-defined networks facilitate rapid and open innovation at the network control layer by providing a programmable network infrastructure for computing flow policies on demand. However, the dynamism of programmable networks also introduces new security challenges that demand innovative solutions. A critical challenge is efficient detection and reconciliation of potentially conflicting flow rules imposed by dynamic OpenFlow (OF) applications. To that end, we introduce FortNOX, a software extension that provides role-based authorization and security constraint enforcement for the NOX OpenFlow controller. FortNOX enables NOX to check flow rule contradictions in real time, and implements a novel analysis algorithm that is robust even in cases where an adversarial OF application attempts to strategically insert flow rules that would otherwise circumvent flow rules imposed by OF security applications. We demonstrate the utility of FortNOX through a prototype implementation and use it to examine performance and efficiency aspects of the proposed framework. With the Internet of Things, more and more devices become remotely manageable. The amount and heterogeneity of managed devices make the task of implementing management functionality challenging. Future Pervasive Computing scenarios require implementing a plethora of services to provide management functionality. With growing demand on services, reducing the emerging complexity becomes increasingly important. A simple-to-use programming model for implementing complex management scenarios is essential to enable developers to create the growing amount of required management software at high quality. The paper presents how data-centric mechanisms, as known from network management, can be utilized to create a service-oriented architecture (SOA) for management services. The resulting shift of complexity from access functionality towards data structures introduces new flexibility and facilitates the programming of management applications significantly. This is evaluated with a user study on the reference implementation. Software Defined Networks (SDNs) support diverse network policies by offering direct, network-wide control over how switches handle traffic. Unfortunately, many controller platforms force applications to grapple simultaneously with end-to-end connectivity constraints, routing policy, switch memory limits, and the hop-by-hop interactions between forwarding rules. We believe solutions to this complex problem should be factored in to three distinct parts: (1) high-level SDN applications should define their end-point connectivity policy on top of a "one big switch" abstraction; (2) a mid-level SDN infrastructure layer should decide on the hop-by-hop routing policy; and (3) a compiler should synthesize an effective set of forwarding rules that obey the user-defined policies and adhere to the resource constraints of the underlying hardware. In this paper, we define and implement our proposed architecture, present efficient rule-placement algorithms that distribute forwarding policies across general SDN networks while managing rule-space constraints, and show how to support dynamic, incremental update of policies. We evaluate the effectiveness of our algorithms analytically by providing complexity bounds on their running time and rule space, as well as empirically, using both synthetic benchmarks, and real-world firewall and routing policies. This paper presents Merlin, a new framework for managing resources in software-defined networks. With Merlin, administrators express high-level policies using programs in a declarative language. The language includes logical predicates to identify sets of packets, regular expressions to encode forwarding paths, and arithmetic formulas to specify bandwidth constraints. The Merlin compiler maps these policies into a constraint problem that determines bandwidth allocations using parameterizable heuristics. It then generates code that can be executed on the network elements to enforce the policies. To allow network tenants to dynamically adapt policies to their needs, Merlin provides mechanisms for delegating control of sub-policies and for verifying that modifications made to sub-policies do not violate global constraints. Experiments demonstrate the expressiveness and effectiveness of Merlin on real-world topologies and applications. Overall, Merlin simplifies network administration by providing high-level abstractions for specifying network policies that provision network resources. Network conditions are dynamic; unfortunately, current approaches to configuring networks. Network operators need tools to express how a network's data-plane behavior should respond to a wide range of events and changing conditions, ranging from unexpected failures to shifting traffic patterns to planned maintenance. Yet, to update the network configuration today, operators typically rely on a combination of manual intervention and ad hoc scripts. In this paper, we present Kinetic, a domain specific language and network control system that enables operators to control their networks dynamically in a concise, intuitive way. Kinetic also automatically verifies the correctness of these control programs with respect to user-specified temporal properties. Our user study of Kinetic with several hundred network operators demonstrates that Kinetic is intuitive and usable, and our performance evaluation shows that realistic Kinetic programs scale well with the number of policies and the size of the network.