Outline

Introduction

Implementation

Analysis

Muen - An x86/64 Separation Kernel forHigh Assurance
Reto Buerki

Adrian-Ken Rueegsegger

Institute for Internet Technologies and Applications
University of Applied Sciences Rapperswil

August 29, 2013

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

Outline1

Introduction
Background
Motivation
Goals

2

Implementation
Overview
Subsystems

3

Analysis
Separation

4

Conclusion
Results
Future Work
Questions
Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

AnalysisConclusion

Virtualization
Virtualization performed by virtual machine monitor (VMM)

VirtualMachine

VirtualMachineVMMVMM

Hosting OS

HardwareHardware(a) Type I, native or baremetal VMM. Runs directlyon the hardware in the mostprivileged processor mode.

(b) Type II or hosted VMM.
The VMM runs on top of aconventional operating
system and uses OS services.

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Outline

Introduction

Implementation

AnalysisConclusion

Intel Virtualization Technologies

VT-x is Intel’s technology for virtualization on the x86
platform
Virtual machine state stored in virtual-machine control
structure (VMCS)
Virtual-machine extensions (VMX) provide CPU instructions
to manage VMCS
VMM runs in VMX root mode
Virtual machines run in VMX non-root mode
Hardware assisted virtualization simplifies implementation ofVMM

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Outline

Introduction

Implementation

Analysis

SPARK
Precisely defined programming language based on Ada
Intended for writing high integrity and security software
Program and proof annotations as Ada comments
Allows proof of absence of runtime errors
Allows partial proof of correctnessIndustrial usage in Avionics, Space, Medical Systems andMilitary
1type Color_Type is ( Red , Green , Blue ) ;23456

procedure Exchange (X , Y : in out Color_Type ) ;--# derives X from Y &--#Y from X ;--# post X = Y∼ and Y = X∼;

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

AnalysisConclusion

Separation Kernel
Concept introduced by John Rushby (1981)
Partition system into multiple subjects which behave as if they
were running on dedicated hardware
Kernel must guarantee component separation
Ideal as basis for a component-based system
No channels for information flow between components otherthan those explicitly provided
Partitioning and isolation of resources(CPU, memory, devices, . . . )Static configuration during integration
Only includes necessary features → small TCB
Well suited for formal verification
Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Outline

Introduction

Implementation

Analysis

Motivation

Currently available (monolithic) systems unsuitable
Implementation suitable for high assurance systems
Increase confidence in systems built with COTS hardware
Public sources and documentation enable third-party review
Many advances in Intel hardware support for virtualization

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

Goals

Open-source separation kernel (GPLv3+)
Implementation in SPARK
Proof of absence of runtime errors
Small code size
Reduction to essential functionality
Leverage latest hardware features of Intel platform(VT-x, EPT, VT-d, . . . )Target platform is 64-bit Intel
Only allow intended data flows
Prevent or limit possible side-/covert channelsReto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

Architecture
Kernel guarantees subject isolation
Spatial isolation by memory management, VT-x
Temporal isolation by scheduling

NativeSubject

VM Subject

Muen Separation Kernel

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

AnalysisConclusion

PolicySpecifies system configuration
Hardware of target platform
Kernel configuration
Subject configuration
Scheduling plansskpolicy tool compiles XML to SPARK sources
123456< subject id = " 2 " name = " crypter " profile = " native " cpu = " 2 "pml4_address = " 270000 " i o _ b i t m a p _ a d d r es s = " 274000 "m s r _ b i t m a p _ a d d r e s s = " 276000 " >& crypterinit ;< memory_layout >& cryptermem ;<! -- crypter request page-- >< memory_region p h y s i c al _ a d d r e s s = " 29 d000 "v ir tu al _ ad dr es s = " 10000 " size = " 4 k " alignment = " 4 k "writable = " false " executable = " false " memory_type= " WB " / >Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Outline

Introduction

Implementation

Analysis

Scheduler I
Fixed cyclic scheduler
Use of VMX preemption timer
VMX root VMX non-root

Scheduling Plan
VM exitKernel Main

Scheduler

Subject

VM enter

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

AnalysisConclusion

Scheduler II
Major frame consisting of minor frames
Minor frames specify subject and time slice in ticks
Scheduling plan specifies minor frames per logical CPUτ 0 subject can switch scheduling plan

Major frame
Minor 1

Minor 2

Minor 3

Subject 1
Subject 2

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Minor 4

Outline

Introduction

Implementation

Analysis

Scheduler III
1
2
3
4
5
6
7
8
91011

< major_frame >< cpu >< minor_frame</ cpu >< cpu >< minor_frame< minor_frame< minor_frame< minor_frame</ cpu ></ major_frame >subject_id = " 0 " ticks = " 200 " / >subject_id = " 1 "subject_id = " 2 "subject_id = " 1 "subject_id = " 2 "Major frame 1

ticks = " 40 " / >ticks = " 80 " / >ticks = " 40 " / >ticks = " 40 " / >Major frame 2

CPU0
CPU1
Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

Traps
Transition to VMX root mode is called a trap
Policy specifies per-subject trap table
Trap causes subject handover according to policy
Trap may inject interrupt in destination subject
Reserved traps are handled differently
VMX preemption timer
External interrupt
Interrupt window
Hypercall

Virtualization using ”Trap and Emulate”
123< trap_table >< entry kind = " * " dst_subject = " sm " dst_vector = " 36 " / ></ trap_table >Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

External Interrupts
Policy assigns devices to subjects
Setup of interrupt routing according to policy
Subject

4 Inject event

2 VM exit

DeviceMuen SK

1 IRQ

3 Handle IRQ

External interrupts cause traps on designated CPU
2 Kernel adds pending event to destination subject
3 Pending events are injected on resumption of subject
4 Subject handles injected event as interrupt
1

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

Event Handling
Event is a hypercall triggered by subject using VMCALL
instruction
Policy specifies per-subject event table
Handover events transfers execution to destination subject
optionally injecting an interrupt
Interrupt events inject interrupt in destination subject withoptional IPI
1234< event_table >< interrupt event = " 1 " dst_subject = " s2 " dst_vector = " 33 "send_ipi = " true " / >< handover event = " 2 " dst_subject = " s3 " / ></ event_table >Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

Multicore
Kernel starts on bootstrap processor (BSP)
BSP starts application processors (APs)
All CPUs synchronize on major frame changes
System Memory
Muen SKCPU storage

Muen SK
INIT-SIPI-SIPI

StackLAPIC
CPU0BSP
Reto Buerki, Adrian-Ken Rueegsegger

CPU storage
StackLAPIC
CPU1AP

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

AnalysisInter-Core Events

Request page
Subject

Subject
Response page

14Muen SK

2IPI

3Muen SK

Handle Hypercall

Handle Hypercall

LAPIC
CPU0

LAPIC
CPU1

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

DemoUntrusted VM subject running MIT’s xv6 OS
Native VT subject provides virtual terminals and keyboard
Native subject monitor (SM) observes xv6 subject
Emulates port I/O
Halts xv6 on invalid operation

Native crypter provides hashing service
Inter-subject communication using shared memory pages
Signalisation using event mechanism

xv6 VM

SubjectMonitor
NativeCrypter
NativeMuen Separation Kernel
Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

VT
NativeConclusion

Outline

Introduction

Implementation

AnalysisVMX Controls - Exiting
Event
External interrupt
VMX preemption timer
Execute INVLPG
Execute MONITOR
Execute MWAIT
Execute RDPMC
Execute RDTSC
Execute WBINVD
MOV to CR3
MOV from CR3
MOV to CR8
MOV from CR8
MOV to/from debug registersI/O port access
MSR accessExceptions
Reto Buerki, Adrian-Ken Rueegsegger

NativeX
X
X
X
X
X
X
X
X
X
X
X
X
X
X
X

Muen Separation Kernel

VM
X
X
X
X
X
X
X
X

X
X
X
X
X

Conclusion

Outline

Introduction

Implementation

Analysis

System Resources
Assigned to subjects according to policy
Assignment is static at integration time
MemorySpecified by memory regions in kernel/subjects spec
Policy compiler creates page tables
Devices
Assignment to subject grants resources(memory, ports, interrupts)
Policy compiler
Maps memory regions into subject’s address space
Enables I/O port access via VMCS I/O bitmap
Creates interrupt routing table entry
Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation KernelConclusion

Outline

Introduction

Implementation

Analysis

Execution Environment
Component
General purpose registers
Segment registers
Instruction pointerFlag register
CR0CR2CR3
CR4
CR8
Descriptor table registers
DR0-3
DR6DR7x87 FPU registers
MMX registers
XMM registers
MSRs
Reto Buerki, Adrian-Ken Rueegsegger

VMCS

StateX

DeniedX
X
X
X
XXXX
XX
XX
X
XX(X)
Muen Separation KernelConclusion

Outline

Introduction

Implementation

AnalysisConclusion

Temporal Isolation

Fixed cyclic scheduler
Static scheduling plan generated from policy
Subject preemption using VMX preemption timer
Sum of minor frame lengths per CPU/major frame are equal
Global barrier sync at beginning of major frame

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Outline

Introduction

Implementation

Analysis

Results
Minimal Zero-Footprint Run-Time (RTS)
KernelTools
Policy compilation tool (skpolicy)
Config generation tool (skconfig)
Packaging tool (skpacker)

Subjects
Initial τ 0 implementationVirtual terminals & keyboard
xv6 OS with minimal adjustments
Subject monitor for xv6
CrypterDumper

Documentation
Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation KernelConclusion

Outline

Introduction

Implementation

Analysis

Results - Kernel

Source code statistics:∼260 lines of Assembly∼2470 lines of SPARK

Proof of absence of runtime errors (All VCs discharged)
Static assignment of resources according to policy
Multicore support
EPT and memory typing (PAT)Event mechanism
Support for native 64-bit subjects
Support for VM subjects

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

Future WorkMid-term
Linux virtualization
Hardware passthrough/PCIe virtualization
Extend τ 0
Covert/Side-Channel analysis
Long-term
MP subjects
Fully virtualized subjects (Windows)
Power Management
Performance optimization
Formal verification
Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion

Outline

Introduction

Implementation

Analysis

Questions?

Thank you for your attention!

Reto Buerki, Adrian-Ken Rueegsegger

Muen Separation Kernel

Conclusion