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”.

Removing compiler from TCB

SVA type system:

Encoding security policies as type systems within the typed bytecode language in SVA.

  • derived from SAFECode, enhanced with metapool.

  • allows to check that complex pointer analysis is correct.

  • a soundness gurantee on the principles used in this work. (LLM: which principles?)

Typing rules in the type system check that the annotated types are never violated.

Type checker implements the typing rules to check the encoded proof is correct.

More typing: information flow[^35], security automata[^48]

  1. Secure Virtual Architecture: A Safe Execution Environment for Commodity Operating Systems, SOSP, 2007. ↩
  2. Memory Safety for Low-Level Software/Hardware Interactions, Usenix Security, 2009. ↩
Created Jul 4, 2019 // Last Updated Aug 31, 2020

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

... what would you change?