中科大－耶鲁高可信软件联合研究中心简介.doc

中科大－耶鲁高可信软件联合研究中心 简 介 一、概述 在中科大软件安全实验室和耶鲁大学FLINT实验室近五年合作的基础上，双方校长于2008年10月签署备忘录，以中科大软件安全实验室为基础，在中科大建立高可信软件联合研究中心。 该中心是在两校相关实验室多年合作的基础上建立的。五年多来，我校软件安全实验室在耶鲁大学邵中教授的指导（包括和他主持的FLINT实验室的合作）下，研究水平上升较快。在邵中教授的支持下，软件安全实验室多次获得国家基金面上项目的资助，目前正在合作申请“海外及港澳学者合作研究基金”。在国际会议和国内外期刊上，两校研究生共同发表了7篇论文，我校研究生单独发表论文10多篇。近6年在编程语言理论及实现技术、软件安全和软件形式验证等研究方向培养了18名博士，其中在高校当教师的有8人，在Intel、Microsoft和Sun公司研发部门工作的有6人，做博士后的有2人。 二、研究领域 （1）程序设计语言理论和实现技术。 这是一个持续活跃了半个世纪的研究领域，目前国际上最活跃的方向是并行编程语言的设计和实现技术、程序验证技术等。我们目前的研究集中在形式程序验证（formal program verification）和出具证明编译器（certifying compiler）两个方向上。通过近几年的国际合作研究，研究水平上升较快。 （2）第2步拟展开的研究方向是计算机网络方面。 有待耶鲁大学相关教授来访，和华蓓教授（可见htttp://staff.ustc.edu.cn/~bhua）和董群峰 在高可信软件研究领域，联合研究中心以形式程序验证为主要方法，研究提高软件可信程度的理论和技术等，目前正在开展的课题有系统软件的形式验证、出具证明的编译器技术、并发多核软件的开发、自动定理证明系统等 在高可信软件研究领域，联合研究中心近5年的建设目标是：研究如何有效地集成形式程序验证和领域专用语言和逻辑（domain-specific languages and logics）这两种软件技术，形成提高编写高可信软件生产力、提高对它们正确性和安全性信任程度、并且能被工业界接受的软件开发新方法，构建基于此方法并能向工业界推广的开发携带证明大型系统软件的基础结构。这是一项为了把形式程序验证技术推向实用，解决其中理论和技术问题的奠基性研究。这项研究的成果将对提高安全攸关软件的可信度，对建设各种安全的信息系统有着重要作用。 三、研究团队 1、研究人员 目前在高可信软件及相关领域的研究人员如下： ? 教授：邵中、陈意云、华蓓、董群峰、冯新宇 ? 副教授：张昱 ? 博士后：郭宇、李兆鹏、付明 ? 博士：华保健、郭燕 ? 博士生和硕士生：20名左右 四、在高可信软件领域中的合作成果 1、近5年连续承担国家自然科学基金面上项目： ? 基于语言理论和实现技术的移动代码安全（Security of mobile code based on techniques of programming language theory and implementation） ? 类型论在软件安全方面的应用研究（Application Research of Type Theory in Software Security and Safety） ? 软件安全性的验证和编译（Verification and Compilation of Software Safety） ? 面向携带证明软件设计的语言、逻辑和证明（Languages, Logics, and Proofs for Certified Software Design） 2、近5年在编程语言理论及实现技术、软件安全和软件验证方面培养了14名博士，其中在Intel、Microsoft和Sun等公司研发部门工作的有6人，在高校当教师的有6人，做博士后的有2人。 3、近期发表的代表性论文如下： [1] X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Modular verification of assembly code with stack-based control abstractions. In Proc. 2006 ACM Conference on Programming Language Design and Implementation, pages 401-414, June 2006. [2] Chunxian Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, and Yu Guo. Foundational typed assembly language with certifi