Microarchitectural timing channels enable unwanted information flow across security boundaries, violating fundamental security assumptions. They leverage timing variations of several state-holding ...microarchitectural components and have been demonstrated across instruction set architectures and hardware implementations. Analogously to memory protection, (Ge et al. 2019) have proposed time protection for preventing information leakage via timing channels. They also showed that time protection calls for hardware support. This work leverages the open and extensible RISC-V instruction set architecture (ISA) to introduce the temporal fence instruction fence.t , which provides the required mechanisms by clearing vulnerable microarchitectural state and guaranteeing a history-independent context-switch latency. We propose and discuss three different implementations of fence.t and implement them on an experimental version of the seL4 microkernel (Klein et al. 2014) and CVA6, an open-source, in-order, application class, 64-bit RISC-V core (Zaruba and Benini 2019). We find that a complete, systematic, ISA-supported erasure of all non-architectural core components is the most effective implementation while featuring a low implementation effort, a minimal performance overhead of less than 1%, and negligible hardware costs.
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 side channel attacks on the last-level cache (LLC), which is shared by all the cores in the processor package, enabling attacks even when VMs are scheduled on different cores. This paper shows how such LLC side channel attacks can be defeated using a performance optimization feature recently introduced in commodity processors. Since most cloud servers use Intel processors, we show how the Intel Cache Allocation Technology (CAT) can be used to provide a system-level protection mechanism to defend from side channel attacks on the shared LLC. CAT is a way-based hardware cache-partitioning mechanism for enforcing quality-of-service with respect to LLC occupancy. However, it cannot be directly used to defeat cache side channel attacks due to the very limited number of partitions it provides. We present CATalyst, a pseudo-locking mechanism which uses CAT to partition the LLC into a hybrid hardware-software managed cache. We implement a proof-of-concept system using Xen and Linux running on a server with Intel processors, and show that LLC side channel attacks can be defeated. Furthermore, CATalyst only causes very small performance overhead when used for security, and has negligible impact on legacy applications.
User-Level Device Drivers: Achieved Performance Leslie, Ben; Chubb, Peter; Fitzroy-Dale, Nicholas ...
Journal of computer science and technology,
09/2005, Letnik:
20, Številka:
5
Journal Article
Recenzirano
Running device drivers as unprivileged user-level code, encapsulated into their own process, has often been proposed as a technique for increasing system robustness. However, in the past, systems ...based on user-level drivers have generally exhibited poor I/O performance. Consequently, user-level device drivers have never caught on to any significant degree. In this paper we demonstrate that it is possible to build systems which employ user-level device drivers, without significant performance degradation, even for high-bandwidth devices such as Gigabit Ethernet.
Worst-case execution time (WCET) analysis of real-time code needs to be performed on the executable binary code for soundness. Obtaining tight WCET bounds requires determination of loop bounds and ...elimination of infeasible paths. The binary code, however, lacks information necessary to determine these bounds. This information is usually provided through manual intervention, or preserved in the binary by a specially modified compiler. We propose an alternative approach, using an existing translation-validation framework, to enable high-assurance, automatic determination of loop bounds and infeasible paths. We show that this approach automatically determines all loop bounds and many (possibly all) infeasible paths in the seL4 microkernel, as well as in standard WCET benchmarks which are in the language subset of our C parser. We also design and validate an improvement to the seL4 implementation, which permits a key part of the kernel’s API to be available to users in a mixed-criticality setting.
Platform virtualization, which supports the co-existence of multiple operating-system environments on a single physical platform, is now commonplace in server computing, as it can provide similar ...isolation as separate physical servers, but with improved resource utilisation.
In the embedded space, virtualization is a new development, which is likely to become more widespread in the next few years. Unlike the server world, where virtualized systems typically run multiple copies of the same (or similar) operating systems, most uses of virtualization in the embedded space are heterogenous, combining different classes of operating systems: an RTOS for traditional embedded real-time programming, and a fully-featured ("rich") operating system to support complex applications such as user interfaces.
We provide a number of examples of present or likely use cases of virtualization in embedded systems, and explain the motivation and benefits, as well as some of the differences to server-style virtualization.
Current approaches to cyberresiliency rely on patching systems after a vulnerability is discovered. What is needed is a clean-slate, mathematically based approach for building secure software. We ...developed new tools based on formal methods for building software for unmanned air vehicles that is provably secure against cyberattacks.
The Last Mile Cock, David; Ge, Qian; Murray, Toby ...
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security,
11/2014
Conference Proceeding
Storage channels can be provably eliminated in well-designed, high-assurance kernels. Timing channels remain the last mile for confidentiality and are still beyond the reach of formal analysis, so ...must be dealt with empirically. We perform such an analysis, collecting a large data set (2,000 hours of observations) for two representative timing channels, the locally-exploitable cache channel and a remote exploit of OpenSSL execution timing, on the verified seL4 microkernel. We also evaluate the effectiveness, in bandwidth reduction, of a number of black-box mitigation techniques (cache colouring, instruction-based scheduling and deterministic delivery of server responses) across a number of hardware platforms. Our (somewhat unexpected) results show that while these defences were highly effective a few processor generations ago, the trend towards imprecise events in modern microarchitectures weakens the defences and introduces new channels. This demonstrates the necessity of careful empirical analysis of timing channels.
High availability and integrity are paramount in systems deployed in life-and mission-critical scenarios. Such fault-tolerance can be achieved through redundant co-execution (RCoE) on replicated ...hardware, now cheaply available with multicore processors. RCoE replicates almost all software, including OS kernel, drivers, and applications, achieving a sphere of replication that covers everything except the minimal interfaces to non-replicated peripherals. We complement our original, loosely-coupled RCoE with a closely-coupled version that improves transparency of replication to application code, and investigate the functionality, performance and vulnerability trade-offs.
