Systems for Safety and DependabilityDavid Evanshttp---.ppt

1、Systems for Safety and DependabilityDavid Evans http:/www.cs.virginia.edu/evans/,University of Virginia Department of Computer Science,2,14 December 1999,Safety and Dependability,What Are You Afraid Of?,Malicious attacks Russian New Year, Melissa, Chernobyl, Java thread attack, etc. Buggy programs C

2、an cause harm accidentally Can be exploited by attackers User mistakes/bad interfaces tar cf *,3,14 December 1999,Safety and Dependability,Menu,Naccio: Policy-Directed Code SafetyHow do you prevent bad programs from doing bad things?naccio.cs.virginia.eduLCLint: Annotation-Assisted Static CheckingHo

3、w do you help good people not write bad programs?lclint.cs.virginia.edu,4,14 December 1999,Safety and Dependability,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 architect

4、ure Can we solve them without sacrificing efficiency or convenience?,Yes!,5,14 December 1999,Safety and Dependability,General method for defining policies Abstract resources Platform independent System architecture for enforcing policies Prototypes for JavaVM classes, Win32 executables,Program,Safe

5、Program,Naccio,Safety Policy,Naccio Overview,6,14 December 1999,Safety and Dependability,Problem,Users View,Files,Resources,Policy,System View,WriteFile (fHandle, ),Disk,Program,System Library,OS Kernel,tar cf *,Platform Interface,7,14 December 1999,Safety and Dependability,Safety Policy Definition,

6、Resource descriptions: abstract operational descriptions of resources (files, network, ) Platform interface: mapping between system events (Java API calls) and abstract resourcesResource use policy: constraints on manipulating those resources,8,14 December 1999,Safety and Dependability,global resour

7、ce RFileSystemopenRead (file: RFile) Called before file is opened for readingopenWrite (file: RFile) Called before existing file is opened for writingwrite (file: RFile, nbytes: int)Called before nbytes are written to file / other operations for observing properties of files, deleting, etc.resource

8、RFile RFile (pathname: String) Constructs object corresponding to pathname,Resource Description,9,14 December 1999,Safety and Dependability,Java PFI Excerpt,wrapper java.io.FileOutputStreamrequires RFileMap;state RFile rfile;wrapper void write (byte b)if (rfile != null) RFileSystem.write (rfile, b.l

9、ength);% / original method call / wrappers needed for constructors, other write/ methods, close and getFD,10,14 December 1999,Safety and Dependability,Resource Use Policy,policy LimitWriteLimitBytesWritten (1000000), NoOverwriteproperty LimitBytesWritten (n: int)requires TrackBytesWritten;check RFil

10、eSystem.write (file: RFile, nbytes: int)if (bytes_written n) violation (“Writing more than ”); stateblock TrackBytesWrittenaddfield RFileSystem.bytes_written: int = 0;precode RFileSystem.write (file: RFile, nbytes: int) bytes_written += nbytes;,11,14 December 1999,Safety and Dependability,Enforceabl

11、e 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,12,14

12、 December 1999,Safety and Dependability,System architecture Defining policiesEnforcing policiesArchitectureResults JavaVM, Win32,Outline,Program,Safe Program,Naccio,Safety Policy,13,14 December 1999,Safety and Dependability,Policy description file,Applicationtransformer,Program,Version of program th

13、at:Uses policy-enforcing system librarySatisfies low-level code safety,Naccio Architecture,Platforms in development: JavaVM program is collection of Java classes Win32 program is Win32 executable and DLLs,Per application,Policy compiler,Safety policy definition,Policy-enforcing system library,Per po

14、licy,14,14 December 1999,Safety and Dependability,Policy description file,Resource descriptions,System library Java library classes,Platform interface Describes Java API,Platform independent analyses,Platform dependent analyses and code generation,Resource use policy,Policy Compiler,Policy-enforcing

15、 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,package naccio.p253.resource; class RFileSystem static int bytes_written = 0;static void write (RFile

16、file, int nbytes) bytes_written += nbytes; if (bytes_written 1000000) Check.violation (“LimitWrite”, “Attempt to write );,Policy compiler,Resource implementations,Resource use policy,stateblock TrackBytesWrittenaddfield RFileSystem.bytes_written: int;precode RFileSystem.write (file: RFile, nbytes: i

17、nt) bytes_written += nbytes; property LimitBytesWritten (n: int)check RFileSystem.write (file: RFile, nbytes: int)if (bytes_written n) violation (“Attempt );,Implementing Resources,RFileSystem RFile,Resource descriptions,policy LimitWriteNoOverwrite,LimitBytesWritten (1000000),16,14 December 1999,Sa

18、fety and Dependability,class FileOutputStream public void write (byte b) writeBytes (b, 0, b.length); ,class FileOutputStream naccio.p253.resource.RFile rfile; / orig_write same implementation as old write methodvoid write (byte b) if (rfile != null) naccio.p253.resource.RFileSystem.write (rfile, b.

19、length);orig_write (b); ,Policy compiler,Wrapped library classes,System library classes,Platform interface,wrapper java.io.FileOutputStream state RFile rfile;wrapper void write (byte b)if (rfile != null) RFileSystem.write (rfile, b.length);% / original method call,Rewriting Classes,17,14 December 19

20、99,Safety and Dependability,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

21、yet: inline methods and state to remove resource overhead,18,14 December 1999,Safety and Dependability,Program Transformer,Policy description file,Program Collection of Java classes,Version of program that: Uses policy-enforcing library Replace class names in constant pool Wrappers for dynamic class

22、 loading methods Satisfies low-level code safety Use Java byte code verifier Wrappers on reflection methods,19,14 December 1999,Safety and Dependability,Whats different for Win32?,Program is Win32 executable and DLLs Platform interface describes Win32 API Policy compiler Generate DLLs instead of Jav

23、a 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,20,14 December 1999,Safety and Dependability,Results - JavaVM,Preparation time minimal Overhead de

24、pends on policy and application Substantially faster than JDK Policy decisions made at transform time Can optimize out unnecessary checking Details in Evans99,Naccio,tar from ,21,14 December 1999,Safety and Dependability,Results Win32,Can enforce policies on Microsoft Word Caveats: Subset of Win32 A

25、PI Doesnt deal with low-level code safety yet (need to implement SFI) Details in Twyman99,pkzip,22,14 December 1999,Safety and Dependability,Related Work,Software fault isolation Wahbe et al, 93 Similar enforcement mechanisms Execution monitoring Schneider Ariel Project Pandey, HashiiAlternative: ve

26、rify properties Proof-carrying code Necula, Lee Typed Assembly Language Morrisett,23,14 December 1999,Safety and Dependability,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

27、low-level safety JavaVM: needs to be attacked For more information:IEEE Security & Privacy 99 (Oakland)http:/naccio.cs.virginia.edu,24,14 December 1999,Safety and Dependability,Annotation-Assisted Static Checking,Effort Required,Low,Unfathomable,Formal Verifiers,Bugs Detected,none,all,Compilers,LCLi

28、nt,25,14 December 1999,Safety and Dependability,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 Simpl

29、e (fast!) dataflow analyses,26,14 December 1999,Safety and Dependability,Sample Annotation: only,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

30、 as an only result Pass it as an only parameter: e.g., extern void free (only void *);,extern only char *gptr; extern only out null void *malloc (int);,27,14 December 1999,Safety and Dependability,Example,1 int dummy (void) 2 int *ip= (int *) malloc (sizeof (int); 3 *ip = 3; 4 return *ip; 5 ,extern

31、only null void *malloc (int); in library,LCLint output: dummy.c:3:4: Dereference of possibly null pointer ip: *ipdummy.c:2:13: Storage ip may become null dummy.c:4:14: Fresh storage ip not released before returndummy.c:2:43: Fresh storage ip allocated,28,14 December 1999,Safety and Dependability,Che

32、cking Examples,Encapsulation abstract types (rep exposure), global variables, documented modifications Memory management leaks, dead references De-referencing null pointers, dangerous aliasing, undefined behavior,29,14 December 1999,Safety and Dependability,Unsoundness & Incompleteness are Good!,Oka

33、y to miss errors Report as many as possible Okay to issue false warnings But dont 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,30,14 December 1999,Safety and Dependability,LCLint Status,Public distribu

34、tion 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.eduPLDI 96, FSE94,31,14 December 1999,Safety and Dependability,Where do we go from here?,Motivating Ex

35、ample: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 w

36、ay Integrate static and run-time checking to enable completeness guarantees,32,14 December 1999,Safety and Dependability,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,33,14 December 1999,Safety and Dependability,Credits,NaccioWin32 Implementation: Andrew Twyman LCLintLCL: Yang Meng Tan, John Guttag, Jim Horning FundingDARPA, NSF, ONR,