Biblio
Many applications are bandwidth consuming but may tolerate longer flow completion times. Multipath protocols, such as multipath TCP (MPTCP), can offer bandwidth aggregation and resilience to link failures for such applications, and low priority congestion control (LPCC) mechanisms can make these applications yield to other time-sensitive ones. Properly combining the above two can improve the overall user experience. However, the existing LPCC mechanisms are not adequate for MPTCP. They do not take into account the characteristics of multiple network paths, and cannot ensure fairness among the same priority flows. Therefore, we propose a multipath LPCC mechanism, i.e., Dynamic Coupled Low Extra Delay Background Transport, named DC-LEDBAT. Our scheme is designed based on a standardized LPCC mechanism LEDBAT. To avoid unfairness among the same priority flows, DC-LEDBAT trades little throughput for precisely measuring the minimum delay. Moreover, to be friendly to single-path LEDBAT, our scheme leverages the correlation of the queuing delay to detect whether multiple paths go through a shared bottleneck. Then, DC-LEDBAT couples the congestion window at shared bottlenecks to control the sending rate. We implement DC-LEDBAT in a Linux kernel and experimental results show that DC-LEDBAT can not only utilize the excess bandwidth of MPTCP but also ensure fairness among the same priority flows.
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.
The Internet, originally an academic network for the rapid exchange of information, has moved over time into the commercial media, business and later industrial communications environment. Recently, it has been included as a part of cyberspace as a combat domain. Any device connected to the unprotected Internet is thus exposed to possible attacks by various groups and individuals pursuing various criminal, security and political objectives. Therefore, each such device must be set up to be as resistant as possible to these attacks. For the implementation of small home, academic or industrial systems, people very often use small computing system Raspberry PI, which is usually equipped with the operating system Raspbian Linux. Such a device is often connected to an unprotected Internet environment and if successfully attacked, can act as a gateway for an attacker to enter the internal network of an organization or home. This paper deals with security configuration of Raspbian Linux operating system for operation on public IP addresses in an unprotected Internet environment. The content of this paper is the conduction and analysis of an experiment in which five Raspbian Linux/Raspberry PI accounts were created with varying security levels; the easiest to attack is a simulation of the device of a user who has left the system without additional security. The accounts that follow gradually add further protection and security. These accounts are used to simulate a variety of experienced users, and in a practical experiment the effects of these security measures are evaluated; such as the number of successful / unsuccessful attacks; where the attacks are from; the type and intensity of the attacks; and the target of the attack. The results of this experiment lead to formulated conclusions containing an analysis of the attack and subsequent design recommendations and settings to secure such a device. The subsequent section of the paper discusses the implementation of a simple TCP server that is configured to listen to incoming traffic on preset ports; it simulates the behaviour of selected services on these ports. This server's task is to intercept unauthorized connection attempts to these ports and intercepting attempts to communicate or attack these services. These recorded attack attempts are analyzed in detail and formulated in the conclusion, including implications for the security settings of such a device. The overall result of this paper is the recommended set up of operating system Raspbian Linux to work on public IP addresses in an unfiltered Internet environment.
Commodity hypervisors are widely deployed to support virtual machines (VMs) on multiprocessor hardware. Their growing complexity poses a security risk. To enable formal verification over such a large codebase, we introduce microverification, a new approach that decomposes a commodity hypervisor into a small core and a set of untrusted services so that we can prove security properties of the entire hypervisor by verifying the core alone. To verify the multiprocessor hypervisor core, we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification, and the top layer specification is refined by all layers of the core implementation. To verify commodity hypervisor features that require dynamically changing information flow, we introduce data oracles to mask intentional information flow. We can then prove noninterference at the top layer specification and guarantee the resulting security properties hold for the entire hypervisor implementation. Using microverification, we retrofitted the Linux KVM hypervisor with only modest modifications to its codebase. Using Coq, we proved that the hypervisor protects the confidentiality and integrity of VM data, while retaining KVM’s functionality and performance. Our work is the first machine-checked security proof for a commodity multiprocessor hypervisor.