Secure Virtual Architecture

Todos

  • Where is the pool metadata created/used in SAFECode passes?
  • Where is the runtime check instrumentation in SAFECode passes?

Learn the code from SVA on FreeBSD and propose a solution for the policy to be ported/re-implemented on CheriBSD:

  • sosp 2007

    • booting
    • signal handler dispatch code
    • I/O instructions.
    • kernel allocators.
    • for analysis(ch6.3): int to pointer casts, stack usage, sys_iotctl, initial task structure, stack pointer to structure.

  • sec 2009

    • memory mapped I/O
    • MMU configuration
    • context switching, thread creation

  • sp 2014, KCoFI

    • label based protection for programmed indirect jumps;
    • a thin run-time layer protects key OS data structures like thread stacks and monitors all low-level state manipulations performed by the OS.

  • asplos 2014, Virtual Ghost

    • compiler instrumentation
    • run-time checks

Top Wonderings

  1. How can SAFECode be used to enforce compartmentalization in a single address space? How does the compartmentalization look like?

    • LLM: Like automatic memory partition using pointer analysis as in DSA, can we do automatic program partition using some similar static analysis techniques?

  2. A two-compartment address space: How can we use SAFECode to eliminate the need of transition between user/kernel mode?

  3. LLVA-OS: Kernel operations as language semantics instead of a lib or handwritten assembled OS?

    • abstracting kernel features as special imperative operations with kernel semantics
    • compilers taking control the entire kernel code just as how it is controling an application. But this application(the kernel) is written with a new language with kernel semantics.
    • Instead of restrict C language, how can we extend it to support OS operations as the language’s ‘native’ mechanisms, just as go in Golang for multi-threading?

  4. Compared to CCured with SAFECode?

    • CCured (From 2014-ISCA-CHERI1): elides bounds checks where it can statically prove them unnecessary. Not thread-safe due to non-atomic pointer access (as noted in its documentation).

Contents

  • Automatic Pool Allocation

    • Reading List: [1] Automatic pool allocation: Improving performance by controlling data structure layout in the heap. PLDI, 2005. [2] Linear Regions Are All You Need. European Symposium on Programming, 2006 paper Region-based memory management Tofte-Talpin Data are allocated within lexically-scoped regions and all of the objects in a region are deallocated at the end of the region’s scope. restrictions on when data can be effectively reclaimed memory leaks Cyclone’s dynamic regions and unique pointers Pool Allocation The idea of instrumentation How to determine a pool for which data structures Applicaions SAFECode Performance optimization

  • SAFECode

    • Questions/Todos Runtime check of SAFECode. LLM: Runtime checks in SAFECode Function Pointers in SAFECode? LLM: Function pointers are checked against a static CFG at runtime (some could be checked at compile time). Where does the pool meta-data stored and used? Can we also store meta-data for all pointers in type-unknown regions? What is affine transformations? used in Control-C Overview Memory safety in C language.

  • LLVA OS

    • References: 2006-LLVA-OS 1 2003-LLVA 2 Idea of LLVA and LLVA-OS LLVA (Low Level Virtual Architecture) supports arbitrary languages including C, and enables sophisticated analyses and optimizations. It provides computational, memory access, and control flow operations. However, LLVA “lacks operations a kernel needs to configure hardware behavior and manipulate program state”. Thus comes LLVA-OS. LLVA-OS is a set of extensions to LLVA that provides an interface between the OS kernel and a general purpose processor architecture.

  • SVA-OS

    • References: 2007-SOSP-SVA 1 2009-SEC-SVA 2 Questions/Proposals Compiler assisted program partition to achieve the SVA effect? Memory Safety by kernel C language memory safety in kernel’s code base Memory safety related functionality of the kernel process states in trap/exceptions, including context switching. virtual/physical page mappings I/O memory, DMA memory Idea of SVA-OS LLVA-OS is an interface prvoides “richer OS-information for hardware, greater flexibility in evolving hardware, and sophisticated analysis and optimization capabilities for kernel code”.

  • Memory Safety in Hardware and Software Interactions

    • Secure HW/SW Interface Motivation OS memory safety research Memory safety for OS code: OS designs based on safe languages; Compiler techniques such as SVA-M to enforce memory safety for commodity OSs in unsafe languages; Instrumentation techniques to isolate a kernel from extensions such as device drivers; Singularity, SPIN, JX, JavaOS, SafeDrive, and SVA-M are examples of system that enforce a safe execution environment. Common asumptions of OS memory safety research Unfortunately, all these memory safety techniques (except Verve, which has very limited I/O and no MMU support) make assumptions that are routinely violated by low-level initeractions between an OS kernel and hardware, even if implemented in safe programming language.

  • Virtual Ghost

    • Virtual Ghost1: Compiler instrumentation of operating system code: creating ghost memory, which kernel cannot access; A thin hardware abstraction layer (SVA-based): kernel must use to be restricted; user application use them to protect themselves via ghost memory management, encryption, signing, and key management; Compiler Instrumentation ghost memory protection. LLVM bitcode translation and validation. CFI on kernel code: ensures the compiler instrumentation is not bypassed. Evaluation Implimentation:

  • Intrinsics

    • Reference:

  • Intrumentation

    • Reference:

  1. 2014-ISCA-CHERI, p9. ↩
Created Jul 4, 2019 // Last Updated Aug 31, 2021

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?