中科大 - 耶鲁高可信软件联合研究中心招生宣传 冯新宇

Presentation on theme: "中科大 - 耶鲁高可信软件联合研究中心招生宣传 冯新宇"— Presentation transcript:

1 中科大 - 耶鲁高可信软件联合研究中心招生宣传 冯新宇
构造没有Bug的软件 中科大 - 耶鲁高可信软件联合研究中心招生宣传 冯新宇

2 软件无处不在 安全攸关系统 （Safety-critical systems） 核电站 医疗设备 航空航天

3 软件无处不在 安全攸关系统 基础设施 通信网络 交通网络（高铁、地铁） 电力系统 日常生活 移动设备 汽车、家电 …

4 Bug无处不在 升空后40秒钟爆炸 将64位整数转化为16位 整数时发生溢出错误 Arianne 5, June 4, 1996

5 “Better, Faster, Cheaper”
1999, NASA失去对 Mars Polar Lander 和 Climate Orbiter的控制. Orbiter: 模块复用出错. Lander: 违背调用条件.

6 Therac-25 1985至1987年间, 6名病人死于或者伤于过量辐射（超过正常剂量100倍） 并发进程之间的数据竞争所导致

7 美国东北大停电 发生于2003年8月14日，覆盖美国东北部、中西部和加拿大的安大略地区
警报系统中的软件的数据竞争错误，导致预警无法及时发出和处理

8 病毒和木马 2010年Stuxnet病毒对伊朗核电站的攻击 利用了Windows系统的4个不为人知的bug

9 如何保证你开发的软件没有bug？

10 测试的局限性 工程中广泛应用，并且有效 简单、容易自动化 无法保证没有bug 在并发（多核/网络）下面作用有限
Testing shows the presence, not the absence of bugs. Edsger W. Dijkstra

11 Limitation of testing – Northeast blackout, 2003
We test exhaustively, we test with third parties, and we had in excess of three million online operational hours in which nothing had ever exercised that bug. I’m not sure that more testing would have revealed that. Unfortunately, that’s kind of the nature of software… you may never find the problem. I don’t think that’s unique to control systems or any particular vendor software. -- Mike Unum, manager at GE Energy Race conditions in GE Energy's Unix-based XA/21 energy management system caused alarm system failure.

12 我们的思路： 基于程序验证技术，构造没有bug的软件

13 内存安全性、功能正确性、终止性、实时性等
主要研究方向 可信系统软件 以形式化程序验证为手段，确保操作系统内核、编译器等系统软件的可靠性、正确性、安全性 程序（数学模型） 规约（数学描述） 内存安全性、功能正确性、终止性、实时性等 验证 严格保证程序相对于其规约没有bug 证明（可靠性证据）

14 程序验证 将程序及其行为刻画为数学对象 将正确性需求刻画为该数学对象上的数学性质 采用逻辑的办法，严格证明这个数学对象满足我们的正确性需求
常见正确性性质举例： “程序永远不会有内存访问错误： 空指针引用、下标越界、内存泄漏等等” “排序函数正确的完成了对数组的排序” “程序不会进入无限循环”

15 程序验证技术 -- 构造没有Bug的软件系统
计算机科学家的最高理想之一 1960年代开始提出 取得众多突破性进展，但仍然面临巨大挑战 有巨大的经济需求 软件bug每年给美国经济带来596亿美元的损失 2002年美国NIST的研究结果 “Null References: The Billion Dollar Mistake” Tony Hoare

16 用形式化验证技术严格证明底层操作系统不会崩溃
防崩溃代码 (Crash-Proof Code)

17 中心研究人员 邵中 (耶鲁) 冯新宇 陈意云 郭宇 李兆鹏 付明 梁红瑾

18 中心研究人员 邵中 耶鲁大学教授，我校大师讲席教授 主要研究方向： 程序设计语言和编译、可信系统软件 SML/NJ编译器的主要设计和开发人员
Certified Software概念的主要倡导者之一

19 中心研究人员（2） 冯新宇 2007年耶鲁大学博士毕业， 2010年加入中国科大，任教授 获教育部新世纪优秀人才计划支持 国际学术任职：
师从邵中教授 2010年加入中国科大，任教授 获教育部新世纪优秀人才计划支持 国际学术任职： 2015年APLAS程序委员会主席（PC Chair） 顶级会议的程序委员会委员：POPL’15, POPL’13, ICPP’15, ICALP 2015 主要研究方向： 操作系统内核验证、并发和多核程序验证

20 中心研究人员（3） 陈意云 郭宇（可招生） 教授 多年从事编译器及程序自动分析和验证的研究 国内率先从事可信编译器的研究
退休，不单独招研究生，但仍活跃在科研一线 郭宇（可招生） 特任副研究员 操作系统内核验证

21 中心研究人员（4） 梁红瑾（可招生） 李兆鹏 付明 特任副研究员 多核算法验证和并发理论 博士后 程序分析和验证
并发程序验证、操作系统内核验证

22 主要平台 中国科大-耶鲁高可信软件联合研究中心 软件安全课题组多核计算课题组 基础研究为主 交换学生、 教师互访等 耶鲁方合作者：
卲中 Richard Yang Bryan Ford

23 科大提供技术，国创提供资金（1000万）和市场需求
主要平台 基础研究与产业化相结合 科大提供技术，国创提供资金（1000万）和市场需求 软件安全课题组多核计算课题组 中国科大-国创高可信软件工程中心

24 主要平台 中国科大-耶鲁高可信软件联合研究中心 软件安全课题组多核计算课题组 中国科大-国创高可信软件工程中心

25 主要课题（1） 实时嵌入式操作系统uC/OS-II内核的验证 约6000行代码 广泛应用于各类嵌入式系统 项目进行中
Parrot Drone

26 主要课题（2） CertiKOS虚拟机（Hypervisor）的验证 将CertiKOS部署在 无人驾驶汽车（LandShark）上
项目进行中（耶鲁大学）

27 主要课题（3） C程序验证器和可信编译 C程序的自动验证 编译后自动生成关于二进制程序的证明 无需相信编译器的正确性

28 主要课题（4） 无锁并发算法的验证 栈、队列、集合等并发对象的验证 并发垃圾收集算法的验证 发现了外科手术机器人控制 程序中并发算法的bug
部分算法来自于java.util.concurrency包 并发垃圾收集算法的验证 算法在Java虚拟中使用 发现了外科手术机器人控制 程序中并发算法的bug

29 加入研究中心的几点原因 选择最关键，同时又最热门的研究方向 最关键：是计算机领域的一项基础性研究 丰富的应用价值和经济价值
无bug软件是计算机科学家的最高理想之一 此领域出过近20名图灵奖得主 仍然有丰富的理论问题，具有很高的研究价值 丰富的应用价值和经济价值 596亿美元的市场？ 新一轮研究热点：2011十大新兴技术之一

30 用形式化验证技术严格证明底层操作系统不会崩溃
防崩溃代码 (Crash-Proof Code)

31 获得此奖项的其他一些软件： Unix、TCP/IP、World-Wide Web、Java、Make、VMWare、Eclipse、LLVM … 国际学术界对精通Coq的研究人员有很大需求 （希望出国的同学可以考虑）

32 加入研究中心的几点原因 选择最关键，同时又最热门的研究方向 站在领域最前沿，从事国际一流的研究 我们在可信软件领域的研究处于国际领先地位
邵中：近年来Certified Software概念的主要倡导者之一 [CACM 2010]

33 MIT出版的Technology Review对十大新兴技术之一——防崩溃代码的报道
防崩溃代码的主要研究人员 33

34 加入研究中心的几点原因 选择最关键，同时又最热门的研究方向 站在领域最前沿，从事国际一流的研究 我们在可信软件领域的研究处于国际领先地位
邵中：近年来Certified Software概念的主要倡导者之一 [CACM 2010] 冯新宇和邵中被列为国际上防崩溃代码的主要研究人员 梁红瑾:国内第一篇本领域顶级会议POPL文章

35 世界一流高校和科研机构在近五年POPL会议上发表论文统计
年份 POPL接收论文总数 录用率 世界一流高校及科研机构＊ POPL论文统计 数量 比例 2008 35 16% 16 46% 2009 36 22% 21 58% 2010 39 18% 54% 2011 49 23% 20 41% 2012 44 21% 17 39% ＊高校 麻省理工、加州伯克利、卡耐基梅隆、斯坦福、剑桥、哈佛、普林斯顿、宾西法尼亚、康奈尔 ＊科研机构 微软、IBM、法国INRIA

36 加入我们的几点原因 选择最基础，同时又最热门的研究方向 站在领域最前沿，从事国际一流的研究 广泛的国际交流机会 目前已有10名研究生访问耶鲁
也很容易建立跟其他学校的交流 10名博士生：王伟、李勇、付明、庄重、蒋信予、张昊中、梁红瑾、张扬、王俊昌、张凯

37 加入我们的几点原因 选择最基础，同时又最热门的研究方向 站在领域最前沿，从事国际一流的研究 广泛的国际交流机会 广阔的发挥个人兴趣的空间
两个研究/工程中心： 提供基础研究和应用型研究的选择 充分尊重学生自己的想法和思路

38 加入我们的几点原因 选择最基础，同时又最热门的研究方向 站在领域最前沿，从事国际一流的研究 广泛的国际交流机会 广阔的发挥个人兴趣的空间
良好的学习和生活环境 合肥和苏州，可以选择

39 1.5h 2.5h 0.5h

40

41

42 近几年研究生的毕业去向 硕士：微软（苏州）、360、百度、小米 …
博士：微软（北京）、Intel、惠普、MicroStrategy … 高校

43 欢迎有兴趣的同学加入！ 跟我联系： 中心主页 xyfeng@ustc.edu.cn，0512-87161319
中心主页

44 谢谢！

45 近期代表性突破 操作系统内核验证（内核不会崩溃等） 编译器验证（编译过程中不会引入新的bug） seL4内核的验证（澳大利亚NICTA）
Verisoft project （德国） Singularity and Verve （Microsoft Research） 编译器验证（编译过程中不会引入新的bug） 经过验证的C语言编译器CompCert（法国INRIA） Type-preserving compiler （ Microsoft Research ）

46 近期代表性突破（2） 程序验证环境和工具 Spec# for C# (MSR) VCC for C (MSR) JML for Java
Z3定理自动证明器 (MSR) SLAM: model checker for device drivers (MSR) …