Transcript Secure Virtual Architecture

John Criswell, Arushi Aggarwal, Andrew Lenharth, Dinakar
Dhurjati, and Vikram Adve
University of Illinois at Urbana-Champaign
Secure Virtual Architecture
Secure Virtual
Architecture
1
Outline
Secure Virtual Architecture
• Background
• Current Work
• Future Work
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
Wouldn’t It Be Great?
• Enforce information flow policy
• Confidentiality
• Data-centric policy created by application/user
• Need to control OS memory operations
• Keep system running when a safety violation is detected
Process
1
Process
2
Operating System
Memory
Secure Virtual Architecture
• Malicious OS can examine/modify any data in memory
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
• Type Inference
• Points-to Analysis
Secure Virtual Architecture
• Run-time Checks
7
Outline
Secure Virtual Architecture
• Background
• Current Work
• Future Work
8
Safe Software/Hardware
Interaction
Problem
Solution
Context Switching
Kernel can load bad state Store CPU state in SVA
on to CPU
VM memory
Stack Management
Kernel stacks are regular, SVA creates new type of
mutable memory objects memory object for
kernel stacks; pointers to
such objects cannot be
dereferenced
MMU Configuration
Static analysis assumes
virtual address space is
immutable
Use para-virtualization to
prevent MMU
configurations that
violate static analysis
safety guarantees
Secure Virtual Architecture
Operation
9
A Secure Foundation
• Strong memory safety enforcement
• 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!
10
Current Work
Secure Virtual Architecture
• Information Flow for C
• Improved Type Inference
• Recovery from Safety Violations
11
•
•
•
•
Experimental information flow infrastructure for C/C++
Explicit information flow on memory object granularity
Properly joins (meets) labels for computation results
Based on SVA
• Memory safety errors cannot violate safety guarantees
• Can reuse SVA infrastructure for optimization
Process
Data
Memory
Object
Meet
Data
Secure Virtual Architecture
CIF: C Information Flow
Compiler
12
SVA Controls Information Flow
Process
2
Operating System
SVA Virtual Machine
Memory
• SVA controls
• Memory access
• MMU configuration
• Information Flow
• Uniform monitoring
• SVA enforces policies
• Not the OS
Secure Virtual Architecture
Process
1
13
Improving Type Safety in SVA
• Benefits
• More static type safety yields more precise run-time safety
guarantees
• Better performance
• Type-safe objects do not need load/store checks
Secure Virtual Architecture
• Better pointer disambiguation due to improved field sensitivity
• Better safety
14
Type Safety Enhancements
• Tracking types at byte-offsets
• Identifying C library functions and allocator wrappers
• Static code transformations to improve inference results
• Cloning of address-taken functions for use in direct calls
• Clone functions that take embedded structures from
incompatible types
Secure Virtual Architecture
• Permit a subset of a memory object to be type safe
• Supports C++ class hierarchy sub-typing
15
Secure Virtual Architecture
Static Type Safety SPEC 2000
16
Secure Virtual Architecture
Static Type Safety SPEC 2006
17
Outline
Secure Virtual Architecture
• Background
• Current Work
• Future Work
18
Dynamic Type Tracking in SVA
• Track types stored to memory at run-time
• Used for memory operations that cannot be proven safe statically
• Byte granularity tracking
• Check type of data when loading from memory
Secure Virtual Architecture
• Fine grained tracking of fields in structures
19
Conclusions
• Infrastructure for secure information flow
• Improved type inference
• Automated recovery from run-time safety violations
• In the pipeline:
• Secure information flow to enforce safety sans OS support
• Dynamic type tracking
Secure Virtual Architecture
• SVA provides a secure foundation
• We have:
20