Packaging applications in Containers, dynamically managed using a cluster orchestrator, is the de-facto approach for deployment of cloud-native applications. When Containers run inside Virtual Machines (VMs) to protect infrastructural assets, Network Policies at the Container layer and Security Groups at the VM layer provide complementary firewall mechanisms that strengthen defenses against lateral movement of attackers. However, least-privilege network policies at the Container layer may not always be consistent with statically defined, over-permissive Security Groups at the VM layer. This is especially a problem with low-latency configuration of Container networking solutions that requires every opened Container protocol, port and traffic direction also to be opened at the VM layer. In any post-exploitation scenario where attackers escape from within an already compromised or infected Container, such over-permissive Security Groups do not prevent the attacker from spreading across VMs to find powerful tokens for accessing the cluster orchestrator. In this paper, we introduce GrassHopper, a fast and dynamic cross-layer enforcement approach for Network Policies, which automatically generates Security Group configurations from dynamically verified Network Policies and Container scheduling decisions. Given the low-latency context, the design of GrassHopper must ensure that dynamically generated Security Group rules come in a timely manner to effect before the newly scheduled Containers become ready to serve traffic. We evaluate the performance of GrassHopper on a Kubernetes cluster running on OpenStack at the network and application level. In comparison to a Security Group management approach that is not scheduling-aware, our findings show that for low-latency applications GrassHopper can reduce the network attack surface between VMs at a ratio of 78-to-99%, while causing no network performance overhead at the application level with respect to latency and throughput.

Packaging applications in containers and managing them dynamically using a cluster orchestrator is the de-facto approach for deployment of cloud-native applications. When containers run inside virtual machines (VMs) to protect infrastructural assets, network policies (NPs) at the container layer and security groups (SGs) at the VM layer provide complementary firewall mechanisms that strengthen defenses against lateral movement of attackers. However, least-privilege NPs at the container layer may not always be consistent with statically defined, over-permissive SGs at the VM layer. This is especially a problem with low-latency configuration of container networking solutions that requires every opened container protocol, port and traffic direction also to be opened at the VM layer. In any post-exploitation scenario where attackers escape from within an already compromised or infected container, such over-permissive SGs do not prevent the attacker from spreading across VMs to find powerful tokens for accessing the cluster orchestrator. In this paper, we introduce GrassHopper (GH), a fast and dynamic cross-layer enforcement approach for NPs, which automatically generates SG configurations from dynamically verified NPs. Given the low-latency context, the design of GH must ensure that dynamically generated SG rules are applied fast before the newly scheduled containers become ready to serve traffic. We evaluate GH on a Kubernetes cluster running on OpenStack. For a wide range of relevant low-latency applications and cluster setups, GH can reduce the network attack surface between VMs at a ratio of 75-to-99% while causing no application level performance overhead with respect to latency, throughput, and CPU utilization.

Well-known defenses exist to detect and mitigate common faults and memory safety vulnerabilities in software. Yet, many of these mitigations do not address the challenge of software resilience and availability, i.e., whether a system can continue to carry out its function and remain responsive, while being under attack and subjected to malicious inputs. In this paper we propose secure rewind and discard of isolated domains as an efficient and secure method of improving the resilience of software that is targeted by run-time attacks. In difference to established approaches, we rely on compartmentalization instead of replication and checkpointing. We show the practicability of our methodology by realizing a software library for Secure Domain Rewind and Discard (SDRaD) and demonstrate how SDRaD can be applied to real-world software.

This article presents an approach to provide strong assurance of the secure execution of distributed event-driven applications on shared infrastructures, while relying on a small Trusted Computing Base. We build upon and extend security primitives provided by Trusted Execution Environments (TEEs) to guarantee authenticity and integrity properties of applications, and to secure control of input and output devices. More specifically, we guarantee that if an output is produced by the application, it was allowed to be produced by the application’s source code based on an authentic trace of inputs. We present an integrated open-source framework to develop, deploy, and use such applications across heterogeneous TEEs. Beyond authenticity and integrity, our framework optionally provides confidentiality and a notion of availability, and facilitates software development at a high level of abstraction over the platform-specific TEE layer. We support event-driven programming to develop distributed enclave applications in Rust and C for heterogeneous TEE, including Intel SGX, ARM TrustZone, and Sancus. In this article we discuss the workings of our approach, the extensions we made to the Sancus processor, and the integration of our development model with commercial TEEs. Our evaluation of security and performance aspects show that TEEs, together with our programming model, form a basis for powerful security architectures for dependable systems in domains such as Industrial Control Systems and the Internet of Things, illustrating our framework’s unique suitability for a broad range of use cases which combine cloud processing, mobile and edge devices, and lightweight sensing and actuation.

The concepts of information flow security and refinement are known to have had a troubled relationship ever since the seminal work of McLean. In this work we study refinements that support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We propose a new epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system's permitted information flows, that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. Our study is set in the context of a class of shared variable multiagent models similar to interpreted systems in epistemic logic. We demonstrate the expressiveness of our framework through a series of small examples and compare our approach to existing, stricter notions of information-flow secure refinement based on bisimulations and noninterference preservation. Interestingly, noninterference preservation is not supported “out of the box” in our setting, because refinement steps may introduce new secrets that are independent of secrets already present at abstract level. To support verification, we first introduce a “cube-shaped” unwinding condition related to conditions recently studied in the context of value-dependent noninterference, kernel verification, and secure compilation. A fundamental problem with ignorance-preserving refinement, caused by the support for general data and observation refinement, is that sequential composability is lost. We propose a solution based on relational pre-and postconditions and illustrate its use together with unwinding on the oblivious RAM construction of Chung and Pass.

Caches pose a significant challenge to formal proofs of security for code executing on application processors, as the cache access pattern of security-critical services may leak secret information. This paper reveals a novel attack vector, exposing a low-noise cache storage channel that can be exploited by adapting well-known timing channel analysis techniques. The vector can also be used to attack various types of security-critical software such as hypervisors and application security monitors. The attack vector uses virtual aliases with mismatched memory attributes and self-modifying code to misconfigure the memory system, allowing an attacker to place incoherent copies of the same physical address into the caches and observe which addresses are stored in different levels of cache. We design and implement three different attacks using the new vector on trusted services and report on the discovery of an 128-bit key from an AES encryption service running in TrustZone on Raspberry Pi 2. Moreover, we subvert the integrity properties of an ARMv7 hypervisor that was formally verified against a cache-less model. We evaluate well-known countermeasures against the new attack vector and propose a verification methodology that allows to formally prove the effectiveness of defence mechanisms on the binary code of the trusted software.

The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a memory virtualization platform for ARMv7-A processors. The design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen. It is shown that this mechanism can be implemented using a compact design, suitable for formal verification down to a low level of abstraction, without penalizing system performance. The verification is performed using the HOL4 theorem prover and uses a detailed model of the processor. We prove memory isolation along with information flow security for an abstract top-level model of the virtualization mechanism. The abstract model is refined down to a transition system closely resembling a C implementation. Additionally, it is demonstrated how the gap between the low-level abstraction and the binary level-can be filled, using tools that check Hoare contracts. The virtualization mechanism is demonstrated on real hardware via a hypervisor hosting Linux and supporting a tamper-proof run-time monitor that provably prevents code injection in the Linux guest.