| 基于Coq构造携带证明的安全程序 |
| |
| 引用本文： | 郭丽,陈意云,李隆,李兆鹏.基于Coq构造携带证明的安全程序[J].计算机工程与应用,2006,42(21):64-67,73. |
| |
| 作者姓名： | 郭丽 陈意云 李隆 李兆鹏 |
| |
| 作者单位： | 中国科学技术大学计算机科学技术系,合肥,230027 |
| |
| 基金项目： | 中国科学院资助项目;Intel中国研究中心资助项目 |
| |
| 摘 要： | 对可靠程序的需求随着高可信软件在信息社会中的作用日益重要而增加。基于形式化证明工具构造携带证明的安全程序,给出严格的程序规范及其证明是提高软件可靠性的重要途径。论文介绍使用形式化证明工具Coq构造安全程序的过程和经验。
|
| 关 键 词： | 高可信软件 安全程序 形式化证明方法 证明工具Coq |
| 文章编号： | 1002-8331-（2006）21-0064-04 |
| 收稿时间： | 2006-02-01 |
| 修稿时间： | 2006-02-01 |
Building Proof-Carrying Security Programs Based on Coq |
| |
| Guo Li,Chen Yiyun,Li Long,Li Zhaopeng.Building Proof-Carrying Security Programs Based on Coq[J].Computer Engineering and Applications,2006,42(21):64-67,73. |
| |
| Authors: | Guo Li Chen Yiyun Li Long Li Zhaopeng |
| |
| Affiliation: | Department of Computer Science and Technology,University of Science and Technology of China, Hefei 230027 |
| |
| Abstract: | As the high-trusted software plays more and more important role in today's information society,the requirement of sound programs greatly increases.To improve software soundness and security,it is a feasible approach for developers to strictly specify and prove programs safety properties based on formal proof tool.This paper describes the process and experience of building such security programs using proof assistant Coq. |
| |
| Keywords: | high-trusted software security program formal proof method proof assistant Coq |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
