期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

安全语言PointerC的设计及形式证明 被引量：8

Design and Proof of a Safe Programming Language PointerC
下载PDF
导出
摘要 程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(side conditions),这些副条件本质上是约束程序语法表达式值的逻辑公式.该文证明了PointerC语言的安全性定理,即满足这些副条件的程序,在执行时不会违反语言的安全策略.为静态推理副条件中涉及指针的命题,作者已经提出了一种指针逻辑(pointer logic),文中证明了指针逻辑对操作语义是可靠的. The safety property of programming languages plays a fundamental role in the design and implementation of safety-critical software systems. And the authors have made investigation towards the design and proof of safe languages suitable for system programming. This paper presents the design of a C-like imperative programming language PointerC. One novelty of PointerC is that typing rules in its type system are accompanied by logic propositions which are called side conditions. And this paper proves PointerC is safe--The executions of programs will not vio- late the safety policy of the language, if these side conditions hold. A pointer logic, as an extension of Hoare logic, has been designed for the purpose of proving pointer-related side conditions statically. This paper presents the soundness proof for the pointer logic.
作者 华保健 陈意云 李兆鹏 王志芳 葛琳 江苏苏州215123
机构地区 中国科学技术大学苏州研究院软件安全实验室
出处 《计算机学报》 EI CSCD 北大核心 2008年第4期556-564,共9页 Chinese Journal of Computers
基金 国家自然科学基金(60673126) Intel中国研究中心资助~~
关键词 软件安全 语言设计 类型系统 HOARE逻辑 指针逻辑 software safety language design type systems Hoare logic pointer logic
分类号 TP301 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献21

  • 1CNCERT/CC. 2006 Annual report. Available at http:// www. cert. org. cn/articles/docs/common/2007042923284. shtml
  • 2Galen Hunt, James Larus. Singularity: Rethinking the software stack. Operating Systems Review, 2007, 41(2): 37-49
  • 3Mandelbaum Y, Walker D, Harper R. An effective theory of type refinements//Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming. Uppsala, Sweden, 2003:213-225
  • 4Xi H. Imperative programming with dependent types//Proceedings of the 15th IEEE Symposium on Logic in Computer Seienee. Washington, DC: IEEE Computer Society, 2000: 375-387
  • 5Xi H, Pfenning F, Dependent types in practical programming//Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. San Antonio, Texas, USA, 1999: 214-227
  • 6Xi H W. Applied type system (extended abstraet)//Post- Workshop Proceedings of the TYPES 2003, Lecture Notes in Computer Science 3085. Berlin: Springer-Verlag, 2004: 394-408
  • 7Smith F, Walker D, Morrisett J G. Alias types//Proceedings of the 9th European Symposium on Programming Languages and Systems. Lecture Notes in Computer Science 1782. London: Springer-Verlag, 2000:366-381
  • 8Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576-580
  • 9Necula G C. Proof-carrying code//Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Paris, France, 1997:106-119
  • 10Chen Y Y, Ge L, Hua B J, Li Z P, Liu C, Wang Z F. A pointer logic and certifying compiler. Frontiers of Computer Science in China, 2007, 1(3): 297-312

二级参考文献29

  • 1Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language//Proceedings of the 25th ACM Symposium on Principles of Programming Languages. San Diego, 1998:85-97
  • 2Mandelbaum Y, Walker D, Harper R. An effective theory of type refinements//Proceedings of the 8th International Conference on Functional Programming. Uppsala, Sweden, 2003: 213-225
  • 3Necula G. Proof-carrying code//Proceedings of the 24th ACM Symposium On Principles of Programming Languages. New York, 1997:106-119
  • 4Appel A W. Foundational proof-carrying code//Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. Baston, Massachusetts, USA, 2001:247-258
  • 5Yu D, Hamid N A, Shao Z. Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming, 2004, 50(1-3):101 127
  • 6Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular Verification of Assembly Code with Stack-Based Control Abstractions//Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation. Ottawa, Canada, 2006:401-414
  • 7Xi H. Applied type system: Extended abstract//Proceedings of TYPES 2003. LNCS 3085. Springer-Verlag, 2004: 394- 408
  • 8Steensgaard B. Points to analysis in almost linear time//Proceedings of the 23th Annual ACM Symposium on Principles of Programming Languages. Florida, USA, 1996:32-41
  • 9Berndl M, Lhotak O, Qian F, Hendren L, Umanee N. Points-to analysis using BDDs//Proceedlngs of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation. San Diego, 2003 :103-114
  • 10Hind M. Pointer analysis: Haven't we solved this problem yet? //Proceedings of the ACM Workshop on Program Analysis for Software. Tools and Engineering. Snowbird, Utab, USA, 2001:54-61

共引文献20

同被引文献49

  • 1Clarke Edmund M, Grumberg Orna, Peled Doron A. Model Checking. Massachusetts: The MIT Press, 1999
  • 2Nipkow T, Paulson L. Isabelle/HOL-A proof assistant for higher-order logic//Lecture Notes in Computer Science 2283. Springer, 2008
  • 3Cruz Jorge. Constraint Reasoning for Differential Models. Amsterdam~ The IOS Press, 2005
  • 4Weiβenbacher Georg. An abstraction/refinement scheme for model checking C programs [M. S. dissertation]. Technischen Universitat Graz, Graz, Austria, 2003
  • 5Henzinger T A, Jhala R, Majumdar R, Necula G C, Sutre G, Weimer W. Temporal-safety proofs for systems code// Proceedings of the 14th International Conference on Computer-Aided Verification (CAV). Copenhagen, Denmark, 2002 : 526- 538
  • 6Clarke M, Kroening D, Sharygina N, Yorav K. SATABS: SAT-based predicate abstraction for ANSI-C//Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005). Edinburgh, U. K. , 2005: 570-574
  • 7Flanagan C, Leino K R M, Lillibridge M, Nelson G, Saxe J B, Stata R. Extended static checking for java//Proceedings of the ACM SIGPLAN2002 Conference on Programming Language Design and Implementation (PLDI' 2002). Berlin, Germany, 2002:234- 245
  • 8Barnett M, Leino K R M, Schulte W, The Spec# programming system: An overview//Proceedings of the CASSIS'04. Marseille, France, 2005:49-69
  • 9Filliatre J C, Marche C. Multi-prover verification of C pro- grams//Proceedings of the ICFEM. Seattle, USA, 2004: 15-29
  • 10Blazy Sandrine, Dargaye Zaynah, Leroy Xavier. Formal veri fication of a C compiler front-end//Proeeedings of the Sympo slum on Formal Methods (FM' 06). Hamilton, Canada 2006: 460-475

引证文献8

二级引证文献9

计算机学报
2008年 第4期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部