Complete formal verification is the only known way to guarantee that a system free of programming errors.We present our experience in performing formal, machine-checked seL4 microkernel from an abstract specification down its C implementation. We assume correctness compiler, assembly code, and hardware, we used unique design approach fuses operating systems techniques. To knowledge, this first proof functional complete, general-purpose operating-system kernel. Functional means here...

We present an effective implementation of the Prime+Probe side-channel attack against last-level cache. measure capacity covert channel creates and demonstrate a cross-core, cross-VM on multiple versions GnuPG. Our technique achieves high resolution without relying weaknesses in OS or virtual machine monitor sharing memory between attacker victim.

Cache side channel attacks are serious threats to multi-tenant public cloud platforms. Past work showed how secret information in one virtual machine (VM) can be extracted by another co-resident VM using such attacks. Recent research demonstrated the feasibility of high-bandwidth, low-noise on last-level cache (LLC), which is shared all cores processor package, enabling even when VMs scheduled different cores. This paper shows LLC defeated a performance optimization feature recently...

We present an in-depth coverage of the comprehensive machine-checked formal verification seL4, a general-purpose operating system microkernel. discuss kernel design we used to make its tractable. then describe functional correctness proof kernel's C implementation and cover further steps that transform this result into kernel: formally verified IPC fastpath, binary code correctly implements semantics, correct access-control enforcement, information-flow noninterference, sound worst-case...

research-article seL4: formal verification of an operating-system kernel Authors: Gerwin Klein National ICT Australia (NICTA), University South Wales (UNSW), Sydney SydneyView Profile , June Andronick NICTA, UNSW UNSWView Kevin Elphinstone Gernot Heiser UNSW, Open Kernel Labs LabsView David Cock NICTA NICTAView Philip Derrin now at Dhammika Elkaduwe Peradeniya, Sri Lanka LankaView Kai Engelhardt Rafal Kolanski Michael Norrish Australian University, Canberra CanberraView Thomas Sewell Harvey...

System virtualization, which enjoys immense popularity in the enterprise and personal computing spaces, is recently gaining significant interest embedded domain. Starting from a comparison of key characteristics systems systems, we will examine difference motivation for use system virtual machines, resulting differences requirements technology. We find that these are quite substantial, virtualization unable to meet special systems. Instead, more general operating-systems technologies...

Direct and Fowler-Nordheim tunneling through ultra-thin gate dielectrics is modeled based on an approach for the transmission coefficient (TC) of a potential barrier that modified by image force. Under constraint equal actions true mapped to trapezoidal pseudobarrier resulting in TC very close numerical solution Schrödinger equation all insulator thicknesses energies electron. The height pseudopotential used as free parameter becomes function energy balancing actions. This can be...

The commonly used value of the intrinsic carrier density crystalline silicon at 300 K is ni=1.00×1010 cm−3. It was experimentally determined by Sproul and Green, J. Appl. Phys. 70, 846 (1991), using specially designed solar cells. In this article, we demonstrate that Green experiment influenced band-gap narrowing, even though dopant their samples low (1014 to 1016 cm−3). We reinterpret measurements numerical simulations with a random-phase approximation model for thereby obtaining...

Managing the power consumption of computing platforms is a complicated problem thanks to multitude hardware configuration options and characteristics. Much academic research based on unrealistic assumptions, has, therefore, seen little practical uptake. We provide an overview difficulties facing management schemes when used in real systems.

We argue that recent hypervisor-vs-microkernel discussions completely miss the point. Fundamentally, two classes of systems have much in common, and provide similar abstractions. assert requirements for both types can be met with a single set abstractions, design, implementation. present partial proof existence this convergence point, guise OKL4 microvisor, an industrial-strength system designed as highly-efficient hypervisor use embedded systems. It is also third-generation microkernel aims...

The L4 microkernel has undergone 20 years of use and evolution. It an active user developer community, there are commercial versions which deployed on a large scale in safety-critical systems. In this paper we examine the lessons learnt those about design implementation. We revisit papers, evolution implementation from original to latest generation kernels, especially seL4, pushed model furthest was first OS kernel undergo complete formal verification its as well sound analysis worst-case...

We have established a simulation model for phosphorus-doped silicon emitters using Fermi–Dirac statistics. Our is based on set of independently measured material parameters and quantum mechanical calculations. In contrast to commonly applied models, which use Boltzmann statistics apparent band-gap narrowing data, we theoretically derived band shifts, therefore account the degeneracy effects physically sounder basis. This leads unprecedented consistency precision even at very high dopant...

A parametrization of the density states (DOS) near band edge phosphorus-doped crystalline silicon is derived from photoluminescence and conductance measurements, using a recently developed theory gap narrowing. It shown that dopant only “touches” conduction at Mott (metal-insulator) transition it merges with considerably higher densities. This resolves well-known contradictions between conclusions drawn various measurement techniques. With proposed DOS, incomplete ionization phosphorus...

In traditional band-to-band Auger recombination theory, the low-injection carrier lifetime is an inverse quadratic function of doping density. However, for densities below about 3×1018 cm−3, lifetimes measured in past on silicon were significantly smaller than predicted by this theory. Recently, a new theory has been developed [A. Hangleiter and R. Häcker, Phys. Rev. Lett. 65, 215 (1990)] that attributes these deviations to Coulombic interactions between mobile charge carriers. This...

Building on Part I of this paper [Altermatt et al., J. Appl. Phys. 100, 113714 (2006)], the parametrization density states and incomplete ionization (ii) is extended to arsenic- boron-doped crystalline silicon. The amount ii significantly larger in Si:As than Si:P. Boron phosphorus cause a similar although boron energy level has distinctly different behavior as function dopant level. This so because ground state fourfold degenerate, while twofold degenerate. Finally, equations are derived...

Faulty device drivers cause significant damage through down time and data loss. The problem can be mitigated by an improved driver development process that guarantees correctness construction. We achieve this synthesising automatically from formal specifications of interfaces, thus reducing the impact human error on reliability potentially cutting costs.

Device drivers are notorious for being a major source of failure in operating systems. In analysing sample real defects Linux drivers, we found that large proportion (39%) bugs due to two key shortcomings the device-driver architecture enforced by current systems: poorly-defined communication protocols between and OS, which confuse developers lead protocol violations, multithreaded model computation leads numerous race conditions deadlocks.

Modern smartphones are increasingly performant and feature-rich but remain highly power-constrained. Effective energy management demands an informed policy, to that end we present a detailed power analysis of the Samsung Galaxy S III smartphone. We measure consumption by instrumentation at circuit level, breakdown major components including CPU, RAM, display, GPU, wireless radios, camera, GPS environmental sensors.

ARM is the dominant processor architecture for mobile devices and many other high-end embedded systems. Late last year announced architectural support virtualization, which will allow execution of unmodified guest operating system binaries. We have designed implemented what we believe first hypervisor supporting pure virtualization using those hardware extensions evaluated it on simulated hardware. describe our approach report initial experience with architecture.

Storage channels can be provably eliminated in well-designed, high-assurance kernels. Timing remain the last mile for confidentiality and are still beyond reach of formal analysis, so must dealt with empirically. We perform such an collecting a large data set (2,000 hours observations) two representative timing channels, locally-exploitable cache channel remote exploit OpenSSL execution timing, on verified seL4 microkernel. also evaluate effectiveness, bandwidth reduction, number black-box...