A μ-kernel is an operating system (OS) paradigm that facilitates a strong cybersecurity posture for embedded systems. Unlike a monolithic OS such as Linux, a μ-kernel reduces overall system privilege by deploying most OS functionality within isolated, userspace protection domains. Moreover, a μ-kernel ensures confidentiality and integrity between protection domains (i.e., spatial isolation), and offers timing predictability for real-time tasks in mixed-criticality systems (i.e., temporal isolation). One popular μ-kernel is seL4 which offers extensive formal guarantees of implementation correctness and flexible temporal budgeting mechanisms.

Embedded and real-time systems are increasingly attached to networks. This enables broader coordination beyond the physical system, but also opens the system to attacks. The increasingly complex workloads of these systems include software of varying assurance levels, including that which might be susceptible to compromise by remote attackers. To limit the impact of compromise, μ-kernels focus on maintaining strong memory protection domains between different bodies of software, including system services. They enable limited coordination between processes through Inter-Process Communication (IPC). Real-time systems also require strong temporal guarantees for tasks, and thus need temporal isolation to limit the impact of malicious software. This is challenging as multiple client threads that use IPC to request service from a shared server will impact each other’s response times.To constrain the temporal interference between threads, modern μ-kernels often build priority and budget awareness into the system. Unfortunately, this paper demonstrates that this is more challenging than previously thought. Adding priority awareness to IPC processing can lead to significant interference due to the kernel’s prioritization logic. Adding budget awareness similarly creates opportunities for interference due to the budget tracking and management operations. In both situations, a Thundering Herd of malicious threads can significantly delay the activation of mission-critical tasks. The Thundering Herd effects are evaluated on seL4 and results demonstrate that high-priority threads can be delayed by over 100,000 cycles per malicious thread. This paper reveals a challenging dilemma: the temporal protections μ-kernels add can, themselves, provide means of threatening temporal isolation. Finally, to defend the system, we identify and empirically evaluate possible mitigations, and propose an admission-control test based upon an interference-aware analysis.

Many embedded systems have evolved from simple bare-metal control systems to highly complex network-connected systems. These systems increasingly demand rich and feature-full operating-systems (OS) functionalities. Furthermore, the network connectedness offers attack vectors that require stronger security designs. To that end, this paper defines a prototypical RTOS API called Patina that provides services common in featurerich OSes (e.g., Linux) but absent in more trustworthy μ -kernel based systems. Examples of such services include communication channels, timers, event management, and synchronization. Two Patina implementations are presented, one on Composite and the other on seL4, each of which is designed based on the Principle of Least Privilege (PoLP) to increase system security. This paper describes how each of these μ -kernels affect the PoLP based design, as well as discusses security and performance tradeoffs in the two implementations. Results of comprehensive evaluations demonstrate that the performance of the PoLP based implementation of Patina offers comparable or superior performance to Linux, while offering heightened isolation.

Conventional network access control approaches are static (e.g., user roles in Active Directory), coarse-grained (e.g., 802.1x), or both (e.g., VLANs). Such systems are unable to meaningfully stop or hinder motivated attackers seeking to spread throughout an enterprise network. To address this threat, we present Dynamic Flow Isolation (DFI), a novel architecture for supporting dynamic, fine-grained access control policies enforced in a Software-Defined Network (SDN). These policies can emit and revoke specific access control rules automatically in response to network events like users logging off, letting the network adaptively reduce unnecessary reachability that could be potentially leveraged by attackers. DFI is oblivious to the SDN controller implementation and processes new packets prior to the controller, making DFI's access control resilient to a malicious or faulty controller or its applications. We implemented DFI for OpenFlow networks and demonstrated it on an enterprise SDN testbed with around 100 end hosts and servers. Finally, we evaluated the performance of DFI and how it enables a novel policy, which is otherwise difficult to enforce, that protects against a surrogate of the recent NotPetya malware in an infection scenario. We found that the threat was most limited in its ability to spread using our policy, which automatically restricted network flows over the course of the attack, compared to no access control or a static role-based policy.

Software-defined networking (SDN) continues to grow in popularity because of its programmable and extensible control plane realized through network applications (apps). However, apps introduce significant security challenges that can systemically disrupt network operations, since apps must access or modify data in a shared control plane state. If our understanding of how such data propagate within the control plane is inadequate, apps can co-opt other apps, causing them to poison the control plane's integrity. We present a class of SDN control plane integrity attacks that we call cross-app poisoning (CAP), in which an unprivileged app manipulates the shared control plane state to trick a privileged app into taking actions on its behalf. We demonstrate how role-based access control (RBAC) schemes are insufficient for preventing such attacks because they neither track information flow nor enforce information flow control (IFC). We also present a defense, ProvSDN, that uses data provenance to track information flow and serves as an online reference monitor to prevent CAP attacks. We implement ProvSDN on the ONOS SDN controller and demonstrate that information flow can be tracked with low-latency overheads.

As Software-Defined Networking has gained increasing prominence, new attacks have been demonstrated which can corrupt the SDN controller's view of network topology. These topology poisoning attacks, most notably host-location hijacking and link fabrication attacks, enable adversaries to impersonate end-hosts or inter-switch links in order to monitor, corrupt, or drop network flows. In response, defenses have been developed to detect such attacks and raise an alert. In this paper, we analyze two such defenses, TopoGuard and Sphinx, and present two new attacks, Port Probing and Port Amnesia, that can successfully bypass them. We then develop and present extensions to TopoGuard to make it resilient to such attacks.

Computer security has long been an arms race between attacks and defenses. While new defenses are proposed and built to stop specific vectors of attacks, novel, sophisticated attacks are devised by attackers to bypass them. This rapid cycle of defenses and attacks has made it difficult to strategically reason about the protection offered by each defensive technique, the coverage of a set of defenses, and possible new vectors of attack for which to design future defenses. In this work, we present QUASAR, a framework that systematically analyzes attacks and defenses at the granularity of the capabilities necessary to mount the attacks. We build a model of attacks in the memory corruption domain, and represent various prominent defenses in this domain. We demonstrate that QUASAR can be used to compare defenses at a fundamental level (what they do instead of how they do it), reason about the coverage of a defensive configuration, and hypothesize about possible new attack strategies. We show that of the top five hypothesized new attack strategies, in fact, four have been published in security venues over the past two years. We investigate the fifth hypothesized vector ourselves and demonstrate that it is, in fact, a viable vector of attack.

Recent work on integration of SDNs with application-layer systems like Hadoop has created a class of system, SDN-Enabled Applications, which implement application-specific functionality on the network layer by exposing network monitoring and control semantics to application developers. This requires domain-specific knowledge to correctly reason about network behavior and properties, as the SDN is now tightly coupled to the larger system. Existing tools for SDN verification and analysis are insufficiently expressive to capture this composition of network and domain models. Unfortunately, it is exactly this kind of automated reasoning and verification that is necessary to develop robust SDN-enabled applications for real-world systems. In this paper, we present ongoing work on Verificare, a verification platform being built to enable formal verification of SDNs as components of a larger domain-specific system. SLA, safety, and security requirements can selected from a variety of formal libraries and automatically verified using a variety of off-the-shelf tools. This approach not only extends the flexibility of existing SDN verification systems, but can actually provide more fine-grained analysis of possible network states due to extra information supplied by the domain model.