Transcript Systems for Safety and Dependability

Systems for
Safety and
Dependability
David Evans
http://www.cs.virginia.edu/~evans/
University of Virginia
Department of Computer Science
What Are You Afraid Of?
• Malicious attacks
– Russian New Year, Melissa, Chernobyl,
Java thread attack, etc.
• Buggy programs
– Can cause harm accidentally
– Can be exploited by attackers
• User mistakes/bad interfaces
– tar –cf *
14 December 1999
Safety and Dependability
2
Menu
Naccio: Policy-Directed Code Safety
How do you prevent bad programs from
doing bad things?
naccio.cs.virginia.edu
LCLint: Annotation-Assisted Static Checking
How do you help good people not write
bad programs?
lclint.cs.virginia.edu
14 December 1999
Safety and Dependability
3
Naccio Motivation
• Weaknesses in existing code safety
systems:
– Limited range of policies
– Policy definition is ad hoc and platform
dependent
• Enforcement is tied to a particular architecture
• Can we solve them without sacrificing
efficiency or convenience?
Yes!
14 December 1999
Safety and Dependability
4
Naccio Overview
Program
• General method for
defining policies
– Abstract resources
– Platform independent
Safety
Policy
• System architecture
for enforcing policies
– Prototypes for
JavaVM classes,
Win32 executables
Safe Program
14 December 1999
Safety and Dependability
5
Problem
User’s View System View
Program
WriteFile (fHandle, …)
Platform Interface
tar cf *
Policy
System Library
OS Kernel
Resources
Files
14 December 1999
Safety and Dependability
Disk
6
Safety Policy Definition
• Resource descriptions: abstract
operational descriptions of resources
(files, network, …)
• Platform interface: mapping between
system events (Java API calls) and
abstract resources
• Resource use policy: constraints on
manipulating those resources
14 December 1999
Safety and Dependability
7
Resource Description
global resource RFileSystem
openRead (file: RFile)
Called before file is opened for reading
openWrite (file: RFile)
Called before existing file is opened for writing
write (file: RFile, nbytes: int)
Called before nbytes are written to file
… // other operations for observing properties of files, deleting, etc.
resource RFile
RFile (pathname: String)
Constructs object corresponding to pathname
14 December 1999
Safety and Dependability
8
Java PFI Excerpt
wrapper java.io.FileOutputStream
requires RFileMap;
state RFile rfile;
wrapper void write (byte b[])
if (rfile != null) RFileSystem.write (rfile, b.length);
%%% // original method call
…
// wrappers needed for constructors, other write
// methods, close and getFD
14 December 1999
Safety and Dependability
9
Resource Use Policy
policy LimitWrite
LimitBytesWritten (1000000), NoOverwrite
property LimitBytesWritten (n: int)
requires TrackBytesWritten;
check RFileSystem.write (file: RFile, nbytes: int)
if (bytes_written > n) violation (“Writing more than …”);
stateblock TrackBytesWritten
addfield RFileSystem.bytes_written: int = 0;
precode RFileSystem.write (file: RFile, nbytes: int)
bytes_written += nbytes;
14 December 1999
Safety and Dependability
10
Enforceable Policies
• Can enforce any policy that can be defined
• What can be defined depends on resource
operations
• Resource operations depend on platform
interface
– Any manipulation done through API calls
– Cannot constrain CPU usage
• Solutions possible: insert calls
• Portable policies use standard resources
14 December 1999
Safety and Dependability
11
Program
Outline
 System architecture
 Defining policies
• Enforcing policies
• Architecture
• Results – JavaVM, Win32
Safety
Policy
Safe Program
14 December 1999
Safety and Dependability
12
Naccio Architecture
Per policy
Per application
Safety policy definition
Policy
compiler
Policy-enforcing
system library
Program
Policy description file
Application
transformer
Version of program that:
• Uses policy-enforcing system library
• Satisfies low-level code safety
Platforms in development:
JavaVM – program is collection of Java classes
Win32 – program is Win32 executable and DLLs
14 December 1999
Safety and Dependability
13
Policy Compiler
Resource use policy
Resource descriptions
Platform
independent
analyses
Platform interface
Describes Java API
System library
Java library classes
Platform dependent
analyses and code
generation
Policy
description file
Policy-enforcing system library
• Implementations of resource operations
– Perform checking described by resource use policy
• Modifies Java byte codes
– Call abstract resource operations as directed by platform
interface
14 December 1999
Safety and Dependability
14
Implementing Resources
policy LimitWrite
NoOverwrite,
LimitBytesWritten (1000000)
RFileSystem
RFile
Resource descriptions
stateblock TrackBytesWritten
addfield RFileSystem.bytes_written: int;
precode RFileSystem.write (file: RFile, nbytes: int)
bytes_written += nbytes;
property LimitBytesWritten (n: int)
check RFileSystem.write (file: RFile, nbytes: int)
if (bytes_written > n) violation (“Attempt …);
Resource use policy
Policy compiler
Resource implementations
package naccio.p253.resource;
class RFileSystem {
static int bytes_written = 0;
static void write (RFile file, int nbytes) {
bytes_written += nbytes;
if (bytes_written > 1000000) Check.violation (“LimitWrite”, “Attempt to write …);
}
…
Rewriting Classes
class FileOutputStream {
…
public void write (byte b[]) {
writeBytes (b, 0, b.length);
}
}
wrapper java.io.FileOutputStream
state RFile rfile;
wrapper void write (byte b[])
if (rfile != null) RFileSystem.write (rfile, b.length);
%%% // original method call
System library classes
Platform interface
Policy compiler
Wrapped library classes
class FileOutputStream {
naccio.p253.resource.RFile rfile;
… // orig_write – same implementation as old write method
void write (byte b[]) {
if (rfile != null) naccio.p253.resource.RFileSystem.write (rfile, b.length);
orig_write (b);
}
14 December 1999
Safety and Dependability
16
Optimizations
• Only implement resource operation if it:
– May produce a violation
– Modifies state used elsewhere
• Only wrap library method if it:
– Calls implemented resource operation
– Modifies state used meaningfully
– Alters behavior
• Simple dataflow dependency analysis
• Not done yet: inline methods and state to
remove resource overhead
14 December 1999
Safety and Dependability
17
Program
Collection of Java classes
Policy description file
Program
Transformer
Version of program that:
1. Uses policy-enforcing library
• Replace class names in constant pool
• Wrappers for dynamic class loading methods
2. Satisfies low-level code safety
• Use Java byte code verifier
• Wrappers on reflection methods
14 December 1999
Safety and Dependability
18
What’s different for Win32?
• Program is Win32 executable and DLLs
• Platform interface describes Win32 API
• Policy compiler
– Generate DLLs instead of Java classes
• Application transformer
– Replace DLL names in import table
– Low-level code safety is platform-specific
• SFI for jumps, PFI wrappers to protect memory
• Scan for kernel traps
• Policies can be reused
14 December 1999
Safety and Dependability
19
Normalized Run Time
Results - JavaVM
• Preparation time
minimal
• Overhead depends on
policy and application
• Substantially faster
than JDK
2.5
2
Naccio
1.5
1
JavaApplet
using JDK
JavaApplet
TarCustom
LimitWrite
tar from www.ice.com
14 December 1999
– Policy decisions made
at transform time
– Can optimize out
unnecessary checking
• Details in [Evans99]
Safety and Dependability
20
Results – Win32
1.1
1.05
1
LimitWrite
ReadOnlyDir
LimitPath
Null
Normalized Run Time
1.15
• Can enforce policies on
Microsoft Word
• Caveats:
– Subset of Win32 API
– Doesn’t deal with lowlevel code safety yet
(need to implement SFI)
• Details in [Twyman99]
pkzip
14 December 1999
Safety and Dependability
21
Related Work
• Software fault isolation [Wahbe et al, 93]
• Similar enforcement mechanisms
– Execution monitoring [Schneider]
– Ariel Project [Pandey, Hashii]
• Alternative: verify properties
– Proof-carrying code [Necula, Lee]
– Typed Assembly Language [Morrisett]
14 December 1999
Safety and Dependability
22
Naccio Summary
• Method for defining large class of policies
– Using abstract resources
• General architecture for code safety
• Encouraging results so far
– Win32: need to implement low-level safety
– JavaVM: needs to be attacked
For more information:
IEEE Security & Privacy 99 (Oakland)
http://naccio.cs.virginia.edu
14 December 1999
Safety and Dependability
23
Annotation-Assisted Static Checking
all
Bugs Detected
Formal Verifiers
Compilers
none
Low
14 December 1999
Effort Required
Safety and Dependability
Unfathomable
24
Approach
• Programmers add annotations (formal
specifications)
– Simple and precise
– Describe programmers intent:
• Types, memory management, data hiding,
aliasing, modification, nullness, etc.
• LCLint detects inconsistencies between
annotations and code
– Simple (fast!) dataflow analyses
14 December 1999
Safety and Dependability
25
Sample Annotation: only
extern only char *gptr;
extern only out null void *malloc (int);
•
•
•
•
Reference (return value) owns storage
No other persistent (non-local) references to it
Implies obligation to transfer ownership
Transfer ownership by:
– Assigning it to an external only reference
– Return it as an only result
– Pass it as an only parameter: e.g.,
extern void free (only void *);
14 December 1999
Safety and Dependability
26
Example
extern only null void *malloc (int); in library
1 int dummy (void) {
2
int *ip= (int *) malloc (sizeof (int));
3
*ip = 3;
4
return *ip;
5 }
LCLint output:
dummy.c:3:4: Dereference of possibly null pointer ip: *ip
dummy.c:2:13: Storage ip may become null
dummy.c:4:14: Fresh storage ip not released before return
dummy.c:2:43: Fresh storage ip allocated
14 December 1999
Safety and Dependability
27
Checking Examples
• Encapsulation – abstract types (rep
exposure), global variables,
documented modifications
• Memory management – leaks, dead
references
• De-referencing null pointers, dangerous
aliasing, undefined behavior
14 December 1999
Safety and Dependability
28
Unsoundness &
Incompleteness are Good!
• Okay to miss errors
– Report as many as possible
• Okay to issue false warnings
– But don’t annoy the user to too many
– Make it easy to configure checking and
override warnings
• Design tradeoff – do more ambitious
checking the best you can
14 December 1999
Safety and Dependability
29
LCLint Status
• Public distribution since 1993
• Effective checking >100K line programs
(checks about 1K lines per second)
– Detects lots of real bugs in real programs
(including itself, of course)
• More information:
lclint.cs.virginia.edu
PLDI ’96, FSE’94
14 December 1999
Safety and Dependability
30
Where do we go from here?
• Motivating Example:
Take an e-commerce site and prove that credit
card information is never stored or transmitted
unencrypted
• Meta-annotations [David LaRochelle]
– Allow users to define new annotations and
associated checking
• Generalize framework
– Support static checking for multiple source
languages in a principled way
– Integrate static and run-time checking to enable
completeness guarantees
14 December 1999
Safety and Dependability
31
Summary
• A little redundancy goes a long way
• Naccio:
– Describe high-level behavioral constraints in an
abstract way
– Check them automatically at run-time
• LCLint:
– Describe programmer intent in a precise way
– Check them statically at compile-time
14 December 1999
Safety and Dependability
32
Credits
• Naccio
Win32 Implementation: Andrew Twyman
• LCLint
LCL: Yang Meng Tan, John Guttag,
Jim Horning
• Funding
DARPA, NSF, ONR
14 December 1999
Safety and Dependability
33