Transcript CIF: Criswell Information Flow

John Criswell, Andrew Lenharth, Dinakar Dhurjati, Arushi
Aggarwal, Will Dietz, and Vikram Adve
University of Illinois at Urbana-Champaign
Secure Virtual Architecture
Secure Virtual
Architecture
1
Outline
• Background
• Results to Date
• Ongoing Work
• Secure Application Computation
Secure Virtual Architecture
• Controlling the OS
• Full System Recovery
2
SVA
e.g.,
Enforce
properties
on a
malicious
OS
Data-centric security
Formal methods
TRANSFORMATION
Hardware support for
isolation
Dealing with malicious
hardware
HARDWARE
Secure browser
appliance
e.g.,
Prevent
data
exfiltration
Secure servers
WEB-BASED
ARCHITECTURES
SYSTEM ARCHITECTURES
e.g.,
Enable
complex
distributed
systems,
with
resilience
to hostile
OS’s
Secure Virtual Architecture
Binary translation
and
emulation
Cryptographic
secure computation
3
Applications Need a Hero
• Enforce application-specific security policies
• But Malicious OS can examine/modify any data in memory
• Need an agent to control a potentially malicious OS
• Need something below the OS!
Hardware! Protect
me from this
malicious OS!
Application
Operating System
Hardware
Sorry,
application.
You’re on your
own
Secure Virtual Architecture
• Confidentiality
• Data-centric application/user policies
4
Secure Virtual Architecture
Virtual ISA
Native ISA
• Compiler-based virtual machine
• Uses sophisticated compiler analysis & transformation techniques
• Virtual instruction set
• Typed virtual instruction set enables sophisticated program analysis
• Special instructions for OS kernel support
• Provide safe execution environment for commodity software
• Supports unmodified C/C++ applications
• Supports commodity operating systems (e.g., Linux)
Secure Virtual Architecture
Commodity
Applications + OS
Compiler + VM
Hardware
5
Safe Language
Control flow integrity
Array indexing within bounds
No uses of uninitialized variables
Type safety for all objects
Secure Virtual Architecture
Control flow integrity
Array indexing within bounds
No uses of uninitialized variables
Type safety for subset of objects
No uses of dangling pointers
Sound operational semantics
Dangling pointers are harmless
Sound operational semantics
• Dangling pointers & non-type-safe objects do not
compromise other guarantees
• Strongest memory safety for C sans garbage collection
Secure Virtual Architecture
SVA Safety Guarantees
6
What’s the Secret Sauce?
•
•
•
•
Load/Store Checks
Bounds Checks
Illegal Free Checks
Indirect Call Checks
• Static Analysis and
Transformations
• Type Inference
• Points-to Analysis
• Automatic Pool Allocation
Secure Virtual Architecture
• Run-time Checks
7
Outline
• Background
• Results to Date
• Ongoing Work
• Secure Application Computation
Secure Virtual Architecture
• Controlling the OS
• Full System Recovery
8
SVA-OS
• Like a ukernel, only better
• Sufficiently low-level to support multiple operating systems
• Sufficiently high-level to enable strong analysis
Linux + SVA-OS
SVM
Virtual ISA
Native ISA
Hardware
SVA can control the OS!
Secure Virtual Architecture
• API implemented as a run-time library linked into the kernel
• Implements interface between system code and hardware
• Provides key software/hardware functionality
9
Operation
Problem
Solution
Context
Switching
Kernel can load bad state
on to CPU
Store CPU state in SVA VM
memory
Stack
Kernel stacks are regular,
Management mutable memory objects
SVA creates new type of memory
object for kernel stacks; pointers
to such objects cannot be
dereferenced
Signal
Handler
Dispatch
Kernel must modify
application stack for signal
handler invocation
Provide higher-level instructions
for pushing/popping function call
frames on applications stack
MMU
Configuratio
n
Static analysis assumes
virtual address space is
immutable
Use para-virtualization to prevent
MMU configurations that violate
static analysis safety guarantees
Secure Virtual Architecture
Safe Software/Hardware
Interaction
10
Summary: A Secure Foundation
• Strong memory safety enforcement == full SVA guarantees
• Can rely on static analysis results to hold at run-time
• Enforces safety properties on applications and OS kernel code
Safety enforced despite hostile OS Code!
Secure Virtual Architecture
• Even for low level OS code!
11
Operating System Recovery
• Recovery Domains: An Organizing Principle for Recoverable
Operating Systems
• Basic Idea: treat OS system calls as transactions
• When an error is detected roll back state and re-exec syscall
Secure Virtual Architecture
• ASPLOS ‘09: Andrew Lenharth, Vikram Adve, and Samuel T. King
12
Outline
• Background
• Results to Date
• Ongoing Work
• Secure Application Computation
Secure Virtual Architecture
• Controlling the OS
• Full System Recovery
13
Secure Memory
• Only an application can access its secure memory
• SVA prevents the OS from accessing the secure memory
Secure Virtual Architecture
• Disallow OS from mapping the secure memory
Application
Virtual Pages
OS
Virtual Pages
Physical
Page Frames
Application
Regular Memory
14
Application
Secure Memory
OS
Kernel Memory
Secure Memory is Great, But…
• Unfettered OS can indirectly access secure memory
• Secure Memory is difficult to use
• Pointers to secure memory must also be in secure memory.
• Program itself can leak data unintentionally
Secure Virtual Architecture
• E.g., Signal handler dispatch and context switching
15
Secure Memory Outline
• What we’re working on now: basic secure memory
• Key: maintain CFI for application, protect data
• Use compiler to help with difficult to reason about properties
Secure Virtual Architecture
• What we’ll be working on soon: usable secure memory
16
Preventing Access to Program
Code and Stacks
Application Kernel
• OS cannot modify or remap:
• Works because SVA controls:
Code:
• Loads/stores
• MMU configuration
• Protects application CFI
• OS cannot get application to
bypass run-time checks
Stack:
inserted by SVA
• OS cannot cause application to
execute arbitrary code
Secure Virtual Architecture
• Application Stack
• Application Code
17
Interacting with the OS
• Prevent OS could from modifying saved program state
• CPU state saved on syscall or interrupt
• CPU state saved on context switch
• Context Switch
• Memory access still an open challenge
• Simple solution: allow heap access, promote stack buffers to heap
• More complex: analyze application and OS together
OS is Master
Application
Operating System
OS is Untrusted Partner
Application
Operating System
Secure Virtual Architecture
• Ensure that OS restores correct state
18
Asynchronous Program
Invocation and Signal Handling
• SVA-OS has instruction for modifying application stack
• Add checks to it to ensure function is a signal handler
• SVA can determine which functions are arguments to syscalls
Application
Stack
Application
Stack
sva_push_func
Application
Stack
sva_load_icontext
Original Application Registers
Application Registers After Signal Handler Dispatch
Secure Virtual Architecture
• Ensure OS restores correct application state on sigreturn()
19
Basic Usable Secure Memory
• Move them to secure
memory
Pointer
Insecure
Memory
Object
Secure
Memory
Object
Secure Virtual Architecture
• Pointers to secure
memory objects
must be in secure
memory
• Points-to graph can
find such pointers
20
• Computations using secure memory do not use insecure
memory
• Computations using insecure memory do not use secure
memory
• Import/export instructions moving data to/from secure
memory
• Allows intentional breaking of non-interference
• Ensures OS does not affect computations
Secure Virtual Architecture
Secure Memory and Non-interference
21
Conclusions
• SVA provides a secure foundation
• Control over the OS
• Recovery from detected safety violations
• Automated recovery from run-time safety violations
• Initial design of secure memory
• Ongoing work:
• Implementation of secure memory
• Design of secure memory usability enhancements if time permits
Secure Virtual Architecture
• We have:
22