Transcript CS696 Talk

Research in
Programming
Languages
and Security
David Evans
Office 236A, 982-2218
[email protected]
http://www.cs.virginia.edu/~evans
University of Virginia
Computer Science
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
Naccio Motivation
Problems with existing code safety systems:
1. Don’t let you express many useful policies
e.g., can restrict what network connections are
opened, but not what is done with them after
2. Define policies in ad hoc, platformdependent ways
–
–
Can’t reuse policies on programs for different
platforms
Hard to write, understand and reason about
policies
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
Naccio Architecture
Per policy
Per application
Safety policy definition
Policy
compiler
Policy-enforcing
system library
Program
Policy description file
Program
transformer
Version of program that:
• Uses policy-enforcing system library
• Satisfies low-level code safety
Problem
User’s View
System View
Program
WriteFile (fHandle, …)
tar cf *
System Library
Policy
OS Kernel
Resources
Files
Disk
Safety Policy Definition
• Resource descriptions: abstract
operational descriptions of resources
(files, network, …)
• Platform interface: mapping between
system API and abstract resources
• Resource use policy: constraints on
manipulating those resources
Example Resource Use Policy
stateblock TrackBytesWritten
addfield RFileSystem.bytes_written: int = 0;
precode RFileSystem.write (file: RFile, nbytes: int)
bytes_written += nbytes;
property LimitBytesWritten (n: int)
requires TrackBytesWritten;
check RFileSystem.write (file: RFile, nbytes: int)
if (bytes_written > n) violation (“Writing more than …”);
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
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
Status
• Naccio/JavaVM – policies on Java classes
– Complete implementation, works
– Performance better than JDK
• Naccio/Win32 – Win32 executables
– Done by Andrew Twyman (MIT MEng thesis)
– Works for non-adversarial programs
– Doesn’t implement necessary low-level code
safety
• More information:
– naccio.cs.virginia.edu
IEEE Security & Privacy ‘99 paper, my thesis
Some Naccio-related Projects
• Low-level code safety for Naccio/Win32
– Prevent malicious programs from tampering with
or circumventing checking code and data
• Validate a Platform Interface
– Develop techniques for verifying a platform
interface and API implementation are consistent
according to some model
• Others at www.cs.virginia.edu/~evans/projects.html
and breakout session
LCLint: Annotation-Assisted Static
Checking
all
Bugs Detected
Formal Verifiers
Compilers
none
Low
Unfathomable
Effort Required
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
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
Philosophy (Why it works)
• Don’t try to be perfect:
– 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
• Performance matters – must be fast as
compiler
LCLint Status
Date: Tue, 2 Nov 1999 10:28:29
From: [email protected]
• Public distribution since 1993
…
– Widely distributed (mostly
linux)
One more question – Why did you stop
– About 1000 active users
developing LCLint? I find some
(but lots not writing annotations)
mistakes that is very easy to fix.
• Checks ANSI C programs
Milos (16 year old in Yugoslavia)
• Large, unwieldy code base
• More information:
– lclint.cs.virginia.edu
PLDI ’96, FSE’94
Some LCLint Projects
• Detecting buffer overflows
– Check CERT reports
• Meta-annotations
– Allow users to define new annotations and
associated checking
• Generalize framework
– Support static checking for multiple source
languages in a principled way
Programming Device
Networks
• New project – not well defined yet
• Assume everything you own is networked
• Different programming problem:
– Computation simple, interactions complex
– Must work the first time
– Must behave reasonably despite unpredictable
events
– Performance hardly matters
For more information…
Breakout session:
Thursday, 5:30-7 in 236D
Email me by noon Thursday if you are
coming
Office hours: Mondays 1:30-2:30
[email protected]
http://www.cs.virginia.edu/~evans