Some notes taking from reading the paper ‘The Singularity System’.

Safe Programming Language

what is PL safety

  • semantic precision for every statement
  • undefinedness -> security compremised
  • the language ensures a statement is only excuted whtn it makes sense, or signals some error(ex throwing an exception)

memory safety

  • programs can only access mem locarions that they are allowed to access
  • may be compremised by:
    • pointer arithmetic
    • unconstrained casting
    • lack of in-built array bounds checks
    • lack of in-guilt checks for null pointers
    • programmer-controlled de-allocation (free malloc in C), it may cause use-after-free/double-free bugs -> we can use GC to solve these problems
  • programs never read uninitialised memory
  • a memory safery language never result in segment faults

type safety

  • type soundness(strong typing) -> never result in type errors

Singularity System

Singularity is a small experimental OS built by Microsoft Research designed with modern software engineering practices and tools.

Motivation & Key

Safety in OS:

  • mem safety between
    • process -> page table / process
    • kernel -> mode (kernel&user)
  • with a safe language, can achieve safety without hardware support

Design principle:

  • unrealable software shoud not cause system failure
  • system write in safe language
  • system must be self-describing

Structure

  • architecture: microkernel, precess and IPC in kernel, else user space
  • language: Sing#, C#
  • abstraction:
    • SIP(Software Isolated Process)
    • Channel whti contracts
  • Because of memory safety -> SIP can be run in ring0
  • making safe code efficient: Bartok for Sing# -> native instruction (Java -> intermedian -> instruction)

Hardware vs software mem isolation

  • SIP: p1 cannot have a pointer to p2
    • every wuer proggam is writtern in Sing#
    • each SIP has a singularity runtime
    • system call -> function call -> performance up
  • memory isolation

The plug in problem

  • run in seperate address -> overhead
  • run in same address -> safety
  • sandbox -> expressivety
  • SIP for plugin -> Sing#

built-in Singularity design decisions

  • SIPs are inexpensive -> allowing isolation at finer granularity (processes are highly costed in other system -> encourage plug-ins to extend system behavior)
  • SIPs do not share memory -> process state is altered by only one process at a time
  • Communication between SIPs passes through strongly typed channels

protection domains

  • safe programs -> run in ring0
  • unsafe -> ring3

SIP communication

  • channels
    • all message are strongly typed
  • contracts
  • memory isolation -> exchange heap

Specifications everywhere -> Verification

  • channel contracts and program manifests(like ELF headers)
  • decice driver manifests -> hardware registers used by device
    • varify if 2 devs have conflicting reg
    • create typed obj for dev regs

Limitations

  • generational collectors do not agree with the lifetime of many kernel objects that persist as long as the system or process exists
  • data in a process is conventional C# objects, while data passed along channels lives in a distinct type system
  • C# is not convenient for manipulating bit-level formatted data and inlined arrays

Lessons learned

  • manifests could be used to describe dependencied, communication, hardware access
  • replacing in-process plug-ins with components in separate process can improve resilience
  • safe languages, sofeware isolation, increase specification can improve a system