Transcript class5-secure

Secure Execution of
Untrusted Code
Motivation
 Mobile code scenarios
•
•
•
•
•
•
Java applet / Javascript in web page
Postscript / PDF file
Email attachment
BPF
Active networks
Agent technology
Untrusted
Code
My Secure PC
Challenges
 Untrusted code may
• Read sensitive memory regions
•
•
•
•
•
(password, cryptographic keys, db records)
Write memory areas, violate integrity
(overwrite public verification key)
Jump to arbitrary location (jump past password
verification)
Perform arbitrary system calls (execute arbitrary
local programs, access file system)
Waste resources, DoS (memory, computation,
network bandwidth), thrash OS (while 1 do fork())
Crash program, OS
Solution 1: Separate Process
 Run untrusted code in separate process
 Advantages
• Memory separation through VM system
 Disadvantages
• Inter-Process Communication (IPC) is
expensive
– Context switch has high overhead (TLB, cache)
Untrusted code can do any system calls
•
 To protect file system, use chroot
Solution 2: Signed Code
 Only accept code digitally signed by trusted


entity
Advantages
• Simple security policy
• Can be secure if trusted entity creates “secure code”
Disadvantages
• Security relies on secrecy of private key
• Security relies on authenticity of public key
• Coarse-grained access control
Solution 3: Sandboxing
 Run code in limited environment
 Verify each system call
 Verify each memory


Sandbox
reference
Untrusted
Advantage
Code
• Fine-grained control
Disadvantages
Application
• Efficiency
• Expressing security policy
• Sandbox may have security vulnerabilities
Solution 4: SFI
 Provide memory safety efficiently
• Can only r/w legitimate memory locations
 Software fault isolation (SFI): transform
untrusted code into safe code
• Compiler: generates safe code
– Ship source code, or
– Generate code that verifier can easily check
• Loader (binary patching): rewrite untrusted
code
SFI
 Load each module into its own fault
domain
• Code is in read-only part
• Module can r/w anything within fault domain
• Code can only jump within fault domain
 Two parts
• Efficient Software Encapsulation
• Fast Communication Across Fault Domains
Application
Untrusted
Code
Untrusted
Code
Untrusted
Code
Efficient Software Encapsulation
 Goal
• Only allow writes within data part of fault domain
• Only allow jumps within code segment of fault domain
 Mechanisms
• Split memory space into segments, each segment has a
segment identifier (high-order bits of address), and comprises
all addresses for any low-order bits
• Separate code and data segments
• Dedicated registers are only used by inserted code, cannot be
modified by untrusted code
• Tame unsafe instructions by segment matching or address
sandboxing
– PC-relative jumps often safe, static stores are safe
– Other stores and jumps are unsafe
RISC Instruction Set Simplifies SFI
 Memory accessed with load / store
instruction (no add to memory)
 All instructions have fixed size, and are
aligned
• Simplifies instruction verification
• Simplifies jump target verification
 Usually large number of registers
• Can tolerate giving up 5 dedicated registers
Segment Matching
 Verifies correctness of memory accesses
 Advantage
• Can pinpoint address of offending instruction, useful in
debugging
 Disadvantage
• Slow
dedicated-reg  target address
scratch-reg  (dedicated-reg >> shift reg)
compare scratch-reg and segment-reg
trap if not equal
store instruction uses dedicated-reg
Address Sandboxing
 Set segment identifier for each memory access
/ jump instruction
• Overwrite segment identifier with fault domain’s
segment identifier
 Advantage: efficient
 Disadvantage: cannot pinpoint flaw, only
enforces that accesses are within domain
dedicated-reg  target-reg & and-mask-reg
dedicated-reg  dedicated-reg | segment-reg
store instruction uses dedicated-reg
Puzzles
 What about the following transformation, not using
dedicated register?
target-reg  target-reg & and-mask-reg
target-reg  target-reg | segment-reg
store instruction uses target-reg
 What about jumps into SFI verification instructions?

Could we jump outside of fault domain? Could we
write to code segment? Could we jump to data
segment?
What if we only used 4 dedicated registers
(sandboxing case, i.e., 1 dedicated-reg for code/data)?
4-Register Attack
jump target-reg
dedicated-reg  target-reg & and-mask-reg
dedicated-reg  dedicated-reg | segment-reg-c
jump instruction uses dedicated-reg
target-reg = r2
dedicated-reg  target-reg & and-mask-reg
dedicated-reg  dedicated-reg | segment-reg-d
store instruction uses dedicated-reg
Verification of Instrumented Code
 Problem: given instrumented binary, how
can we verify that all rules are met?
 Verify that all unsafe stores and jumps
use dedicated registers to form address
 Verify that all inserted code has correct
pattern (identify inserted code by use of
dedicated registers)
Fast Communication Across Fault
Domains
 Use Jump Table with legal entry points
outside fault domain
 For each call between fault domains, a
customized stub procedure is created
• Stubs run unprotected outside fault domain
• Trusted stub directly copies arguments to
•
•
destination domain
Switch execution stack
Set up register context and validate
dedicated registers
SFI Discussion
 System calls from fault domain?








• Issues and solutions
Allowing arbitrary memory reads?
Could we improve the granulartiy of memory
protection?
• Missing read protection a problem?
Is granularity of jump protection sufficient?
Flexibility for segment size? Internal fragmentation?
Can SFI prevent buffer overruns?
Is self-modifying code possible?
SFI on CISC processors?
Can we change compiler once verifier is deployed?
Solution 5: PCC
 Proof-carrying code (PCC) developed @ CMU




by George Necula and Peter Lee
Goal: safely run code in unsafe languages
Approach: create efficiently verifiable proof
that untrusted code satisfies safety policy
May not need instrumentation code (no
execution overhead!) if we can prove code
safety
Slides based on George Necula’s OSDI96 talk
Proof-Carrying Code: An Analogy
Legend:
code
proof
oracle bits
Proof-Carrying Code (PCC)
untrusted
application code
certification
code producer
code consumer
native
code
safety
proof
PCC binary
proof
validation
CPU
formal
safety policy
Benefits of PCC
 Wide range of safety policies
memory safety
• resource usage guarantees (CPU, locks, etc.)
• concurrency properties
data abstraction boundaries
 Wide range of languages
assembly languages
• high-level languages
 Simple, fast, easy-to-trust validation
 Tamper-proof
Experimentation
 Goal:
• Test feasibility of PCC concept
• Measure costs (proof size and validation
time)
 Choose simple but practical applications
Network Packet Filters
• IP Checksum
• Extensions to the TIL run-time system for
Standard ML
Experimentation (2)
 Use DEC Alpha assembly language
(hand-optimized for speed)
 Network Packet Filters
• BPF safety policy: “The packet is read-only
and the scratch memory is read-write. No
backward branches. Only aligned memory
accesses.”
PCC Implementation (1)
 Formalize the safety policy:
• Use first-order predicate logic extended with
•
can_rd(addr) and can_wr(addr)
Kernel specifies safety preconditions
–Calling convention
–Guaranteed by the kernel to hold on entry
 Use tagged memory to define access
i.(i  0  i  r1  i mod 8  0)  can_rd(r0  i )
j.( j  0  j  16  j mod 8  0)  can_wr(r2  j )
PCC Implementation (2)
 Compute a safety predicate for the code
• Use Floyd-style verification conditions
•
(VCgen)
One pass through the code, for example:
–For each LD r,n[rb] add can_rd(rb+n)
–For each ST r,n[rb] add can_wr(rb+n)
 Prove the safety predicate
• Use a general purpose theorem prover
PCC Implementation (3)
 Formal proofs are trees:
• the leaves are axiom instances
• the internal nodes are inference rule
•
•
instances
at the root is the proved predicate
Example:
PCC Implementation (4)
 Proof Representation: Edinburgh Logical


Framework (LF)
Proofs encoded as LF expressions
Proof Checking is LF type checking
• simple, fast and easy-to-trust (14 rules)
• 5 pages of C code
• independent of the safety policy or application
• based on well-established results from type-theory
and logic
 Large design space, not yet explored
Packet Filter Experiments
 4 assembly language packet filters
(hand-optimized for speed):
1 Accepts IP packets (8 instr.)
2 Accepts IP packets for 128.2.206 (15 instr.)
3 IP or ARP between 128.2.206 and 128.2.209
4 TCP/IP packets for FTP (28 instr.)
 Compared with:
• Run-Time Checking: Software Fault Isolation
• Safe Language: Modula-3
• Interpretation: Berkeley Packet Filter
Performance Comparison
Latency (us)
2.5
2
PCC
SFI
M3
BPF
1.5
1
0.5
0
1
2
Filter
3
4
 Off-line packet trace on a DEC Alpha 175MHz
 PCC packet filters: fastest possible on the architecture
 The point: Safety without sacrificing performance!
Cost of PCC for Packet Filters
 Proofs are approx. 3 times larger than
the code
 Validation time: 0.3-1.8ms
Packet Filter
1
Instructions
8
Proof Size(bytes)
160
Validation Time(us) 362
2
3
4
15
47
28
225 532 420
872 1769 1354
Validation Cost (Filter 3)
ms 15
12
PCC
SFI
M3
BPF
9
6
3
0
0
10
20
30
40
50
Thousands of packets
 Conclusion: One-time validation cost
amortized quickly
PCC for Memory Safety
 Continuum of choices between static
checking and run-time checking:
Performance Penalty
Static
Checking
Run-Time
Checking
Proof Complexity
SFI
 PCC can be also used where run-time
checking cannot (e.g., concurrency)
What Can We Check With PCC?
 Any property with a sound formalization
• if you can prove it, PCC can check it!
 One proof-checker for many such policies!
• Small commitment for open-ended extensibility
 Example: policies defined by safe interpreters
• E.g, security monitors, memory safety, resource
usage limits, …
 … can be enforced statically with PCC
• Prove that all run-time checks would succeed
• No run-time penalty
PCC Beyond Memory Safety
Example: database with access control
 Safety policy:
access
item
• host invokes the agent with:
– security clearance level
price
agent
• level
• parent
pricing server
PCC is not limited to
memory safety!
• item and price fields
readable only if access 
level
– parent
• communication permitted
only back to parent
• must terminate within MAX
instructions
• wait BNDW * SIZE instructions
before sending SIZE bytes
Practical Difficulties
 Proof generation
• Similar to program verification
• But:
– done off-line
– can use run-time checks to simplify the proofs
• In restricted cases it is feasible (even automatable)
 Proof-size explosion
• It is exponential in the worst case
• Not a problem in our experiments
PCC Discussion
 A very promising framework for ensuring


safety of untrusted code
Limitations?
What about generating proof on the fly?
• Could verify safety property based on specific
arguments
 Related problem: how to secure mobile code
from malicious host?