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

Slides:



Advertisements
Similar presentations
第二章 中国的自然环境 地理组 王铁塔. §2.1 地形和地势 学习目标: 1 、 知道我国主要的地形、山脉的名称及山脉 走向的概念。 2 、通过阅读统计图表,总结我国山区面积广大的地 形特征。 3 、了解山区开发、利用的有利条件和不利条件 。 考试要求: 1 、了解我国地形复杂多样,山区面积广大的特征。
Advertisements

数据结构的引入. 通讯录管理 社团机构管理 校园导航管理 通讯录管理 社团机构管理 校园导航管理.
——系统软件与软件安全实验室简介 报告人:冯新宇
博士人员科研答辩   答辩人: 答辩日期:.
优美的双曲线 04级八年制 学号: 学生: 林颖.
——Windows98与Office2000(第二版) 林卓然编著 中山大学出版社
C++面试笔试精要 张立伦 讲师的CSDN博客地址
本科毕业论文:某企业供应链库存成本优化分析
可信软件的前沿理论和技术 计算机科学与技术学院 中科大-耶鲁高可信软件联合研究中心 邵中、陈意云、张昱、郭宇、李兆鹏等
克劳斯-雷克曼 教授 德国 凯勒数控教学仿真软件有限公司
基于解释性语言的手机跨平台架构 Sloan Yi. Qt MTK.
中国药物GCP检查 国家食品药品监督管理局药品认证管理中心         李见明         北京 国家食品药品监督管理局药品认证管理中心.
计算机基础知识 丁家营镇九年制学校 徐中先.
国家高技术研究发展计划 香港大学网格节点 Presented by Cho-Li Wang
程序的形式验证 - 简介 中国科学院软件研究所 张文辉 1.
授课对象:微电子、电子、计算机专业本科生、研究生 先修课:数字逻辑电路、Verilog
嵌入式系统课程简介 宋健建 南京大学软件学院 2004/02/10.
第二讲 搭建Java Web开发环境 主讲人:孙娜
R in Enterprise Environment 企业环境中的R
中国科学技术大学 肖 明 军 《网络信息安全》 中国科学技术大学 肖 明 军
李杰 首都经济贸易大学 安全与环境工程学院 个人主页:
走进编程 程序的顺序结构(二).
第11章:一些著名开源软件介绍 第12章:服务安装和配置 本章教学目标: 了解当前一些应用最广泛的开源软件项目 搭建一个网站服务器
Visual Studio Team System 简介
数 控 技 术 华中科技大学机械科学与工程学院.
Windows网络操作系统管理 ——Windows Server 2008 R2.
作業系統 (Operating System)
沈翔 美国Qwest国际通信公司高级工程师
走进中国科技网 中国科技网 李辉.
湖南大学-信息科学与工程学院-计算机与科学系
美国数学学会 MathSciNet 电子资源的检索和使用
WSDM见闻 程龚.
京师数学大讲坛 第六讲 北京师范大学 数学科学学院
三:基于Eclipse的集成开发环境搭建与使用
Unit 11.Operating System 11.1 What’s OS 11.2 Related Courses
程序设计工具实习 Software Program Tool
第4章 非线性规划 4.5 约束最优化方法 2019/4/6 山东大学 软件学院.
苏晨汀博士 (Dr. Chenting Su) 苏晨汀博士, 1999年毕业于Virginia Tech, 获市场营销学哲学博士学位。曾任教于加拿大University of Victoria 商学院 ( ),现任香港城市大学市场营销系主任,博导。目前致力于研究中国营销渠道冲突及管制机制和消费者选择及决策模型,他的研究成果发表在Journal.
新一代安全网上银行 小组成员:杨志明 王晶 任毅 刘建中 关昊 刘超.
内容摘要 ■ 课程概述 ■ 教学安排 ■ 什么是操作系统? ■ 为什么学习操作系统? ■ 如何学习操作系统? ■ 操作系统实例
Highly Efficient Energy Transfer in Light-Harvesting Complex
C语言程序设计 主讲教师:陆幼利.
微机系统的组成.
Environmental Policy Evaluation – Experiences in Germany and Europe
Seminar 【Speaker】 Ming-Jen Lin Associate professor Dept of Economics
Platform Builder使用介绍 WINCE系统应用开发流程说明 ACTION RDC 杨 涛 2005.Dec.3th
第二章 Java基本语法 讲师:复凡.
程序的形式验证 张文辉
河北大学申请博士生导师 人员基本情况 彩色照片 小二寸 免冠 一、近五年科研项目情况 姓名:张 芳 出生日期: 职称:
计算机网络与网页制作 Chapter 07:Dreamweaver CS5入门
Seminar 【Speaker】 LEI ZHANG, Assistant Professor of
Seminar 【Speaker】 Chung-Ming Kuan, Visiting Professor,
JSP实用教程 清华大学出版社 第2章 JSP运行环境和开发环境 教学目标 教学重点 教学过程 2019年5月7日.
如何成为一名成功的研究生? 系列研讨会 张坤龙
王树水 主任医师 广东省心血管病研究所心儿科副主任 广东省介入性心脏病学会结构性心脏病分会侯任主任委员 招生专业与类型 科研工作 教育经历
Seminar 【Speaker】 Lisa Cameron , Associate professor,University of Melbourne 【Topic】 Propensities to Engage in and Punish Corrupt Behavior: Experimental.
魏新宇 MATLAB/Simulink 与控制系统仿真 魏新宇
甘肃农业大学伏羲学者年度考核 伏羲杰出人才 潘晓婷,女,体育教学部教授,硕士生导师.
计算机绘图 AutoCAD2016.
GIS基本功能 数据存储 与管理 数据采集 数据处理 与编辑 空间查询 空间查询 GIS能做什么? 与分析 叠加分析 缓冲区分析 网络分析
第二节 C语言的特点.
Seminar 【Speaker】 Feng Shuaizhang, assistant professor of the
C++语言程序设计 C++语言程序设计 第一章 C++语言概述 第十一组 C++语言程序设计.
我们关注的是…… © 2009 Citicsf. All rights reserved.. 我们关注的是…… © 2009 Citicsf. All rights reserved.
本节内容 进程 视频提供:昆山爱达人信息技术有限公司 官网地址: 联系QQ: QQ交流群 : 联系电话:
FVX1100介绍 法视特(上海)图像科技有限公司 施 俊.
学习数据结构的意义 (C语言版) 《数据结构》在线开放课程 主讲人:李刚
Seminar 【Speaker】 Soohyung Lee, Department of
实验六、COM类型病毒分析实验 实验开发教师: 刘乃琦 谌黔燕.
光电材料与技术国家重点实验室学术交流会 时间:2016年11月17日(星期四)上午9:00-10:00
Presentation transcript:

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

世界一流高校和科研机构在近五年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

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

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

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

1.5h 2.5h 0.5h

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

欢迎有兴趣的同学加入! 跟我联系: 中心主页 xyfeng@ustc.edu.cn,0512-87161319 http://staff.ustc.edu.cn/~xyfeng 中心主页 http://kyhcs.ustcsz.edu.cn

谢谢!

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

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