The OKL4 microvisor Heiser, Gernot; Leslie, Ben
Proceedings of the first ACM asia-pacific workshop on Workshop on systems,
08/2010
Conference Proceeding
We argue that recent hypervisor-vs-microkernel discussions completely miss the point. Fundamentally, the two classes of systems have much in common, and provide similar abstractions. We assert that ...the requirements for both types of systems can be met with a single set of abstractions, a single design, and a single implementation. We present partial proof of the existence of this convergence point, in the guise of the OKL4 microvisor, an industrial-strength system designed as a highly-efficient hypervisor for use in embedded systems. It is also a third-generation microkernel that aims to support the construction of similarly componentised systems as classical microkernels. Benchmarks show that the microvisor's virtualization performance is highly competitive.
A scalable lock manager for multicores Jung, Hyungsoo; Han, Hyuck; Fekete, Alan D. ...
Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data,
06/2013
Conference Proceeding
Modern implementations of DBMS software are intended to take advantage of high core counts that are becoming common in high-end servers. However, we have observed that several database platforms, ...including MySQL, Shore-MT, and a commercial system, exhibit throughput collapse as load increases, even for a workload with little or no logical contention for locks. Our analysis of MySQL identifies latch contention within the lock manager as the bottleneck responsible for this collapse.
We design a lock manager with reduced latching, implement it in MySQL, and show that it avoids the collapse and generally improves performance. Our efficient implementation of a lock manager is enabled by a staged allocation and de-allocation of locks. Locks are pre-allocated in bulk, so that the lock manager only has to perform simple list-manipulation operations during the acquire and release phases of a transaction. De-allocation of the lock data-structures is also performed in bulk, which enables the use of fast implementations of lock acquisition and release, as well as concurrent deadlock checking.
Sichere IT ohne Schwachstellen und Hintertüren Weber, Arnd; Heiser, Gernot; Kuhlmann, Dirk ...
TATuP - Zeitschrift für Technikfolgenabschätzung in Theorie und Praxis (Online),
04/2020, Letnik:
29, Številka:
1
Journal Article
Recenzirano
Unsere zunehmende Abhängigkeit von Informationstechnik erhöht kontinuierlich die Safety- und Security-Anforderungen bei deren Einsatz. Ein zentrales Problem hierbei sind Schwachstellen von Hard- und ...Software. Marktkräfte konnten diese Situation bislang nicht grundsätzlich beheben. Eine Gegenstrategie sollte deshalb folgende Optionen erwägen: (1) private und staatliche Förderung offener und sicherer IT‑Produktion, (2) Verbesserung der souveränen Kontrolle bei der Produktion aller kritischen IT‑Komponenten innerhalb eines Wirtschaftsraumes sowie (3) verbesserte und durchgesetzte Regulierung. Dieser Beitrag analysiert Vor- und Nachteile dieser Optionen. Es wird vorgeschlagen, die Sicherheit der Schlüsselkomponenten einer Lieferkette durch weltweit verteilte, offene und ggf. mathematisch bewiesene Komponenten zu gewährleisten. Der beschriebene Ansatz erlaubt die Nutzung existierender und neuer proprietärer Komponenten.
Time Protection Ge, Qian; Yarom, Yuval; Chothia, Tom ...
Proceedings of the Fourteenth EuroSys Conference 2019,
03/2019
Conference Proceeding
Odprti dostop
Timing channels enable data leakage that threatens the security of computer systems, from cloud platforms to smartphones and browsers executing untrusted third-party code. Preventing unauthorised ...information flow is a core duty of the operating system, however, present OSes are unable to prevent timing channels. We argue that OSes must provide time protection, the temporal equivalent of the established memory protection, for isolating security domains. We examine the requirements of time protection, present a design and its implementation in the seL4 microkernel, and evaluate efficacy and cost on x86 and Arm processors.
A paper by Hand
et al.
at the recent HotOS workshop re-examined microkernels and contrasted them to virtual-machine monitors (VMMs). It found that the two kinds of systems share architectural ...commonalities but also have a number of technical differences which the paper examined. It concluded that VMMs are a special case of microkernels, "microkernels done right".A closer examination of that paper shows that it contains a number of statements which are poorly justified or even refuted by the literature. While we believe that it is indeed timely to reexamine the merits and issues of microkernels, such an examination needs to be based on facts.
This paper presents a quantitative analysis of perimeter losses in high‐efficiency silicon solar cells. A new method of numerical modelling is used, which provides the means to simulate a full‐sized ...solar cell, including its perimeter region. We analyse the reduction in efficiency due to perimeter losses as a function of the distance between the active cell area and the cut edge. It is shown how the optimum distance depends on whether the cells in the panel are shingled or not. The simulations also indicate that passivating the cut‐face with a thermal oxide does not increase cell efficiency substantially. Therefore, doping schemes for the perimeter domain are suggested in order to increase efficiency levels above present standards. Finally, perimeter effects in cells that remain embedded in the wafer during the efficiency measurement are outlined.
Multi-criticality real-time systems require protected-mode operating systems with bounded interrupt latencies and guaranteed isolation between components. A tight WCET analysis of such systems ...requires trustworthy information about loop bounds and infeasible paths. We propose sequoll, a framework for employing model checking of binary code to determine loop counts and infeasible paths, as well as validating manual infeasible path annotations which are often error-prone. We show that sequoll automatically determines many of the loop counts in the Malardalen WCET benchmarks. We also show that sequoll computes loop bounds and validates several infeasible path annotations used to reduce the computed WCET bound of seL4, a high-assurance protected microkernel for multi-criticality systems.
No Security Without Time Protection Ge, Qian; Yarom, Yuval; Heiser, Gernot
Proceedings of the 9th Asia-Pacific Workshop on Systems,
08/2018
Conference Proceeding
The recent Spectre exploits demonstrated that covert timing channels are a mainstream security threat. Their prevention requires that operating systems provide time protection, in addition to the ...established memory protection. We propose OS mechanisms and designs which provide time protection, and define requirements on the hardware to enable them. We demonstrate that present mainstream processors do not meet these requirements, making them inherently insecure. We argue the need for a new security-oriented hardware-software contract, which we call the aISA as it augments the ISA, in order to enable time protection.
PDF
