欢迎来到麦多课文档分享! | 帮助中心 海量文档,免费浏览,给你所需,享你所想!
麦多课文档分享
全部分类
  • 标准规范>
  • 教学课件>
  • 考试资料>
  • 办公文档>
  • 学术论文>
  • 行业资料>
  • 易语言源码>
  • ImageVerifierCode 换一换
    首页 麦多课文档分享 > 资源分类 > PPT文档下载
    分享到微信 分享到微博 分享到QQ空间

    Systems for Safety and DependabilityDavid Evanshttp---.ppt

    • 资源ID:389574       资源大小:236.50KB        全文页数:33页
    • 资源格式: PPT        下载积分:2000积分
    快捷下载 游客一键下载
    账号登录下载
    微信登录下载
    二维码
    微信扫一扫登录
    下载资源需要2000积分(如需开发票,请勿充值!)
    邮箱/手机:
    温馨提示:
    如需开发票,请勿充值!快捷下载时,用户名和密码都是您填写的邮箱或者手机号,方便查询和重复下载(系统自动生成)。
    如需开发票,请勿充值!如填写123,账号就是123,密码也是123。
    支付方式: 支付宝扫码支付    微信扫码支付   
    验证码:   换一换

    加入VIP,交流精品资源
     
    账号:
    密码:
    验证码:   换一换
      忘记密码?
        
    友情提示
    2、PDF文件下载后,可能会被浏览器默认打开,此种情况可以点击浏览器菜单,保存网页到桌面,就可以正常下载了。
    3、本站不支持迅雷下载,请使用电脑自带的IE浏览器,或者360浏览器、谷歌浏览器下载即可。
    4、本站资源下载后的文档和图纸-无水印,预览文档经过压缩,下载后原文更清晰。
    5、试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓。

    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,


    注意事项

    本文(Systems for Safety and DependabilityDavid Evanshttp---.ppt)为本站会员(registerpick115)主动上传,麦多课文档分享仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对上载内容本身不做任何修改或编辑。 若此文所含内容侵犯了您的版权或隐私,请立即通知麦多课文档分享(点击联系客服),我们立即给予删除!




    关于我们 - 网站声明 - 网站地图 - 资源地图 - 友情链接 - 网站客服 - 联系我们

    copyright@ 2008-2019 麦多课文库(www.mydoc123.com)网站版权所有
    备案/许可证编号:苏ICP备17064731号-1 

    收起
    展开