goal of an OS is to support running applications ‣ Stability: most applications are not yet written when the system is deployed ‣ Scalability: do not rewrite everything for every new hardware device Firmware Hypervisor Kernel Language Runtime Shared Libraries Configuration files Application
goal of an OS is to support running applications ‣ Stability: most applications are not yet written when the system is deployed ‣ Scalability: do not rewrite everything for every new hardware device • OS does this by ‣ Providing abstraction over hardware — drivers! ‣ Resource management: fi les, users, CPU, memory, network Firmware Hypervisor Kernel Language Runtime Shared Libraries Configuration files Application
goal of an OS is to support running applications ‣ Stability: most applications are not yet written when the system is deployed ‣ Scalability: do not rewrite everything for every new hardware device • OS does this by ‣ Providing abstraction over hardware — drivers! ‣ Resource management: fi les, users, CPU, memory, network • Application code is a small % of the runtime environment Firmware Hypervisor Kernel Language Runtime Shared Libraries Configuration files Application
I agree that microkernels are nicer... As has been noted (not only by me), the Linux kernel is a minuscule part of a complete system: Full sources for Linux currently run to about 200kB compressed. And all of that source is portable, except for this tiny kernel that you can (provably: I did it) re-write totally from scratch in less than a year without having /any/ prior knowledge." – Linus Torvalds, 1992 Firmware Hypervisor Kernel Language Runtime Shared Libraries Configuration files Application
its monolith into many individual libraries. ‣ There is no ambient kernel; just function calls are left. • Device drivers, schedulers, networking, and storage stacks are directly linked to the application ‣ Eliminate the need for an intermediary kernel layer. ‣ Applications select libraries they need with a small boot layer and jump straight into the code.
its monolith into many individual libraries. ‣ There is no ambient kernel; just function calls are left. • Device drivers, schedulers, networking, and storage stacks are directly linked to the application ‣ Eliminate the need for an intermediary kernel layer. ‣ Applications select libraries they need with a small boot layer and jump straight into the code. • Hardware is driven directly from the application, usually in a single address space.
Cambridge/Glasgow • Exokernel: MIT Neither succeeded outside of academia due to the device drivers needing to be updated regularly to stay relevant. Became popular in niche areas (network appliances or high-frequency trading).
hardware, small attack surface, high-performance. Cons: There is no kernel protection internally, and device drivers all need to be rewritten from a normal kernel.
allow the creation of virtual versions of physical resources, such as servers, networks, and storage devices. • It enables multiple virtual machines (VMs), with their own operating systems, to run in isolation, side-by-side, on the same physical hardware. • Hypervisor (aka VMM) — creates and runs virtual machines
• QEMU emulates CPUs and missing hardware • VirtIO — virtualisation of networks and disk device drivers ‣ Can take advantage of Linux Kernel’s vast driver support! Cons: There is no kernel protection internally, and device drivers all need to be rewritten from a normal kernel. Library operating systems
C++, Assembly, Objective-C • Safe languages ‣ With the help of a garbage collector (GC) — JavaScript, Python, Java, Go, OCaml, … ‣ Without a GC — Rust • Unsafe parts of safe languages ‣ Unsafe Rust, unsafe package in Go, Obj in OCaml
C++, Assembly, Objective-C • Safe languages ‣ With the help of a garbage collector (GC) — JavaScript, Python, Java, Go, OCaml, … ‣ Without a GC — Rust • Unsafe parts of safe languages ‣ Unsafe Rust, unsafe package in Go, Obj in OCaml Cons: There is no kernel protection internally, and device drivers all need to be rewritten from a normal kernel. Library operating systems
Powerful module system Functional core with imperative and object- oriented features Native (x86, Arm, Power, RISC-V), JavaScript, WebAssembly Industry Projects
your application can tolerate 1 ms latency, then OCaml is a good fi t ‣ 95% of code that we write fi t this model • GC is a tradeo ff between space and time
your application can tolerate 1 ms latency, then OCaml is a good fi t ‣ 95% of code that we write fi t this model • GC is a tradeo ff between space and time • OCaml is typically 1.5x to 2x slower than C for algorithmic workloads ‣ Python will be 10x to 100x slower than C
your application can tolerate 1 ms latency, then OCaml is a good fi t ‣ 95% of code that we write fi t this model • GC is a tradeo ff between space and time • OCaml is typically 1.5x to 2x slower than C for algorithmic workloads ‣ Python will be 10x to 100x slower than C • Fast FFI to C for speed
compiler that can build specialised images containing only the runtime environment needed by the application ‣ Cut the complexity by designing the layers as independent type-safe libraries.
compiler that can build specialised images containing only the runtime environment needed by the application ‣ Cut the complexity by designing the layers as independent type-safe libraries. • The MirageOS compiler transforms an application manifest into a specialised image. ‣ Rely on the OCaml compiler for modular static analysis, dead-code elimination, etc.
compiler that can build specialised images containing only the runtime environment needed by the application ‣ Cut the complexity by designing the layers as independent type-safe libraries. • The MirageOS compiler transforms an application manifest into a specialised image. ‣ Rely on the OCaml compiler for modular static analysis, dead-code elimination, etc. • Rely on the OCaml runtime as the sole trusted runtime environment (and selected C bindings)
binary • Executed as a virtual machine ‣ Solo5 is the host system process (“tender”) - Provides the platform-speci fi c details for MirageOS applications to interact with the underlying hardware or virtualisation frameworks ‣ Supports — KVM, Xen, virtio, muen, Linux Seccomp • Can also be executed as a Unix process ‣ Useful for debugging and development
traditionally opaque layer ‣ Resulting images usually have a size of a few MiB. ‣ Our HTTPS web server which runs mirage.io is only 10 MiB! • Con fi guration can be partially evaluated at compile-time ‣ Extreme specialisation enables a boot time of a few ms.
traditionally opaque layer ‣ Resulting images usually have a size of a few MiB. ‣ Our HTTPS web server which runs mirage.io is only 10 MiB! • Con fi guration can be partially evaluated at compile-time ‣ Extreme specialisation enables a boot time of a few ms. • If something (e.g. networking) is not used, it will not be available at runtime ‣ Minimal runtime environments use a few MiB of RAM.
traditionally opaque layer ‣ Resulting images usually have a size of a few MiB. ‣ Our HTTPS web server which runs mirage.io is only 10 MiB! • Con fi guration can be partially evaluated at compile-time ‣ Extreme specialisation enables a boot time of a few ms. • If something (e.g. networking) is not used, it will not be available at runtime ‣ Minimal runtime environments use a few MiB of RAM. • The kernel and user space share the same address space ‣ Many runtime checks are removed, so static analysis is critical.
from 2015 to 2018 • Hold the key to 10 bitcoins (peak worth $165k) ‣ Now worth ~$1M • A successful authenticated TLS session reveals the private Bitcoin key • 500,000 accesses to the Piñata website, more than 150,000 attempts at connecting to the Piñata bounty • The bitcoins were safe!
solution to manage cryptographic keys securely. • The software implementation should be easy to customise and o ff er superior security ‣ It should also be easily auditable by anyone to eliminate backdoors. • The NetHSM should meet high-performance requirements, allowing its use in low-power hardware security devices and highly e ff i cient cloud-based solutions. • They chose to use MirageOS running on the Muen micro-kernel https://www.nitrokey.com/products/nethsm
other Linux features • On macOS • Docker daemon runs in a light Linux VM (using hypervisor.framework) • Docker client is a Mac application • MirageOS libraries are used to translate semantics di ff erences between platforms: • volumes: FUSE format + fsevent/inotify • network: Linux ethernet packets to MacOS network syscalls MirageOS libraries used by millions of users
inter-unikernel isolation ‣ No separate kernel vs user space ‣ No separation between di ff erent bits of the user space (no process abstraction) • Linking external C libraries ‣ Legacy C code is unavoidable — crypto, drivers, sqlite, … ‣ may have memory vulnerabilities, may harm Unikernel safety OCaml (safe) + C (unsafe) code
inter-unikernel isolation ‣ No separate kernel vs user space ‣ No separation between di ff erent bits of the user space (no process abstraction) • Linking external C libraries ‣ Legacy C code is unavoidable — crypto, drivers, sqlite, … ‣ may have memory vulnerabilities, may harm Unikernel safety OCaml (safe) + C (unsafe) code
intra-process isolation ‣ Functions mapped to compartments ‣ Restrict control fl ow and data access across security boundaries • Control fl ow restricted by ‣ Whitelisted PC ranges ‣ Shadow stack to prevent ROP attacks
intra-process isolation ‣ Functions mapped to compartments ‣ Restrict control fl ow and data access across security boundaries • Control fl ow restricted by ‣ Whitelisted PC ranges ‣ Shadow stack to prevent ROP attacks • Data access restricted by ‣ VMM tricks (or) fat pointers (or) capabilities (à la CHERI)
MirageOS unikernels ‣ https://gitlab.com/shaktiproject • Intra-process compartments - Vulnerabilities in C do not a ff ect OCaml • Compartment access matrix de fi ned at link time - Run unmodi fi ed OCaml and C code Access Matrix
MirageOS unikernels ‣ https://gitlab.com/shaktiproject • Intra-process compartments - Vulnerabilities in C do not a ff ect OCaml • Compartment access matrix de fi ned at link time - Run unmodi fi ed OCaml and C code • Small extension to hardware and software ‣ Two new instructions added to RISC-V ISA: Val and Checkcap ‣ Modi fi cation to LLVM and OCaml compiler to emit these instructions Access Matrix
and use of Obj.magic trusted • All code is compiled with FIDES C and OCaml compiler ‣ Compiler instrumentation added by FIDES is correct ‣ OCaml runtime is trusted • Binary executable cannot be tampered with • Hardware attacks rowhammer, fault attacks, side-channels are out of scope
fl ow in every execution of the program respects the compartment access matrix • Memory safety ‣ No memory errors; all references point to valid memory ‣ Pointers cannot be forged
memory safety ‣ Hardware-accelerated fat pointers only for C code - Fine-grained data compartments - No fat pointers for OCaml code ‣ Pay attention to FFI boundaries
memory safety ‣ Hardware-accelerated fat pointers only for C code - Fine-grained data compartments - No fat pointers for OCaml code ‣ Pay attention to FFI boundaries • FIDES code compartment must now handle FP features! ‣ Higher-order functions, tail calls, exceptions
amongst migrant voters ‣ 300 million people don’t vote • Enable migrant voters to be able to vote from a di ff erent constituency • Voting machine is more complex! ‣ “Discussion on improving voter participation of domestic migrants using remote voting”, Election Commission of India, 2022 Display Public Ballot Display
sequence • OCaml has several non-call-return control- fl ow operations ‣ Tail calls, exceptions, e ff ect handlers! ‣ Need to manage the shadow stack carefully
compartments ‣ Need to unwind shadow stack appropriately ‣ Challenge: Detect when intra-compartment exceptions are raised • Solution: Security monitor (SM) updates last exn_pc to a special routine exn_pc prev_exn_ptr sp exn_ptr raise sp exn_ptr
= 64 bits Cookie … base bound Memory region Fat pointer Fresh cookie at malloc and free • Fat pointers into the stack have frame scope ‣ Each frame has a cookie freshened at call and return
= 64 bits Cookie … base bound Memory region Fat pointer Fresh cookie at malloc and free • Fat pointers into the stack have frame scope ‣ Each frame has a cookie freshened at call and return • val instruction validates fat pointer before access
= 64 bits Cookie … base bound Memory region Fat pointer Fresh cookie at malloc and free • Fat pointers into the stack have frame scope ‣ Each frame has a cookie freshened at call and return • val instruction validates fat pointer before access • OCaml does not use fat pointers ‣ At FFI, use OCaml object header info to create fat pointer ‣ Use a special cookie that skips temporal validation
lines for LLVM • Protyped on Xilinx Artix-7 AC701 FPGA ‣ 38.2K LUTs (+6.1% over base) ‣ 17.4K registers (+6.0% over base) • Performance on voting application ‣ 4% increase in code size ‣ 23% increase in instruction cycle count OCaml Stdlib (C5) Crypto (C3) Vote Handler (C2) UI (C4) Result table Main (C1) Highly secure Has C code Has C code
runtime is trusted ‣ WIP: Veri fi ed garbage collector for OCaml • Data compartments are too weak ‣ Objects shared across compartments remain accessible forever ‣ Revocation through ownership and borrowing à la Rust - modal types in OCaml
runtime is trusted ‣ WIP: Veri fi ed garbage collector for OCaml • Data compartments are too weak ‣ Objects shared across compartments remain accessible forever ‣ Revocation through ownership and borrowing à la Rust - modal types in OCaml • Hardware is exotic ‣ Arm MTE for fat pointers in C?
kayceesrk
lauravandoore
3n
orderedlist
shlominoach
afnizarnur
aarron
eileencodes
palkan
destraynor
cromwellryan
smashingmag
vanstee
