可信软件

Report
可信软件与多核计算
报告人:冯新宇
研究背景
• 处理能力越来越强
• 多核、众核、GPU …
• 问题规模越来越大
• 网络、云计算、大数据…
• 安全性需求越来越高
• 软件应用越来越广、计算环境日益复杂
Heartbleed: SSL
buffer overflow bug
研究方向
• 如何算的“快”?
• 如何充分利用多核(众核)计算资源,解决计算问题?
• 新的算法、操作系统、编程语言和模型等
• 如何算的“对”?
• 软件的正确性、可靠性、安全性等
• 高可信软件:如何开发没有bug的软件?
• 如何服务于新兴的计算需求?
• 如何从性能和可靠性两个方面为新兴应用提供支持?
• 应用:嵌入式和移动系统、网络、云计算、大数据
研究团队
卲中(耶鲁)
张昱
冯新宇
华蓓
郭宇
李兆鹏
陈意
云
付明
可信软件
构造没有Bug的软件系统
• 计算机科学家的最高理想之一
• 1960年代开始提出
• 取得众多突破性进展,但仍然面临巨大挑战
• 有巨大的经济需求
• 软件bug每年给美国经济带来596亿美元的损失
• 2002年美国NIST的研究结果
• “Null References:
The Billion Dollar Mistake”
- Tony Hoare
用形式化验证技术严格证明底层操作系统
不会崩溃
防崩溃代码
(Crash-Proof Code)
主要研究方向
• 可信防崩溃系统软件构造
• 以形式化程序验证为手段,确保操作系统内核的可靠性、
正确性、安全性
• 形式化程序验证
• 将程序及其行为刻画为数学对象
• 将正确性需求刻画为该数学对象上的数学性质
• 采用数学的办法,严格证明这个数学对象满足我们的正
确性需求 – 比测试有更严格的保证
常见正确性性质举例:
“程序永远不会有内存访问错误:空指针引用、下标越界、内存泄漏等”
“排序函数正确的完成了对数组的排序”
“程序不会进入无限循环”
可信软件:主要课题
• 实时嵌入式操作系统uC/OS-II内核的验证
• 约6000行代码
• 广泛应用于各类嵌入式系统
• 项目进行中
Parrot Drone
冯新宇
可信软件:主要课题
• CertiKOS虚拟机(Hypervisor)的验证
• 将CertiKOS部署在
无人驾驶汽车(LandShark)上
• 项目进行中
Zhong Shao
(耶鲁)
可信软件:主要课题
• C程序验证器和可信编译
• C程序的自动验证
• 编译后自动生成关于二进制程序的证明
• 无需相信编译器的正确性
陈意云
多核计算
多核计算:主要挑战
• 并发程序开发及正确性
• 大量的不确定性
• 难以编程、易出错、难测试/调试
多核计算:主要挑战
• 并发程序开发及正确性
• 大量的不确定性
• 难以编程、易出错、难测试/调试
• 计算资源的充分利用
• 并行化:如何把任务分配到
不同的处理器上?
如何有效协调存在
依赖关系的任务?
• Cache对性能的影响?
CPU 和 GPU 的协同?
多核计算:主要课题
• 确定性并行编程模型和操作系统
• 确定性操作系统Dlinux
• 确定性共享虚存模型: 不同读写特征的内存区域
张昱
• 只读、单生产者-多消费者模型、DiffMerge
• 进程/线程的动态管理、I/O的确定性并行
• 确定性并行编程模型的设计和实现
Reducor(是否可交换)
Dynamic Scheduler
Load Balancer
…
多核计算:主要课题
• 基于多核/众核处理器的高速网络算法/系统
• 基本思路
华蓓
• 利用通用多核服务器构建高速网络系统
• 研究突破网络系统瓶颈的关键技术
• 基于多核服务器的高速网络流量监视系统
• 关键技术突破:用于核间通信的单生产者-单消费者并发无锁队列、
大规模TCP查找算法(已实际应用)
• 由合作企业完成成果转化(万兆级数据中心服务性能监视系统)
• 新型计算架构上的网络系统:CPU+独立GPU,APU
• 基于GPU的算法加速
• 异常检测,数据压缩,数据流加密,......
多核计算:主要课题
• 无锁并发算法的验证
• 栈、队列、集合等并发对象的验证
• 部分算法来自于java.util.concurrency包
冯新宇
• 并发垃圾收集算法的验证
• 算法在Java虚拟中使用
• 发现了外科手术机器人控制程序中并发算法的bug
对新兴应用领域的支持
可信软件
关键应用
多核计算
关键应用
• 大数据分析平台及关键技术
华蓓
冯新宇
• 集海量数据存储、查询、分析功能于一体的数据平台
• 基于对非关系数据库MongoDB的改造
• 高效的大数据索引技术
• 网络流量大数据分析
• 数据分析的隐私保护以及编程语言支持
• 软件定义网络(SDN):最有前途的新型网络架构
• 以视频多播和网络编码应用为切入点,研究SDN的
关键技术,并在CENI平台上验证。
• 新型的编程语言支持
• 网络程序的分析和验证
研究团队
卲中(耶鲁)
张昱
冯新宇
华蓓
郭宇
李兆鹏
陈意
云
付明
基础研究为主
主要平台
交换学生、
教师互访等
中国科大-耶鲁高可信
软件联合研究中心
软件安全课题组
多核计算课题组
耶鲁方合作者:
卲中
Richard
Yang
Bryan
Ford
主要平台
基础研究与产业化相结合
软件安全课题组
多核计算课题组
科大提供技术,国创提供资
金(1000万)和市场需求
中国科大-国创高可信
软件工程中心
主要平台
中国科大-耶鲁高可信
软件联合研究中心
软件安全课题组
多核计算课题组
中国科大-国创高可信
软件工程中心
加入我们的5点原因
• 选择最基础,同时又最热门的研究方向
• 多核、软件定义网络(SDN)、大数据等
• 当前研究热点,有广泛的应用
• 可信软件
• 最基础:是计算机领域的一项基础性研究
• 无bug软件是计算机科学家的最高理想之一
• 此领域出过近20名图灵奖得主
• 仍然有丰富的理论问题,具有很高的研究价值
• 丰富的应用价值和经济价值
• 596亿美元的市场?
• 新一轮研究热点:2011十大新兴技术之一
加入我们的5点原因
• 选择最基础,同时又最热门的研究方向
• 站在领域最前沿,从事国际一流的研究
• 我们的多项研究处于国际领先地位
• 邵中:近年来Certified Software概念的主要倡导者之
一 [CACM 2010]
防崩溃代码的主要
MIT出版的Technology Review对十大新兴
研究人员
技术之一——防崩溃代码的报道
加入我们的5点原因
• 选择最基础,同时又最热门的研究方向
• 站在领域最前沿,从事国际一流的研究
• 我们的多项研究处于国际领先地位
• 邵中:近年来Certified Software概念的主要倡导者之一
[CACM 2010]
• 冯新宇和邵中被列为国际上防崩溃代码的主要研究人员
• 多篇顶级期刊和会议文章
• TOPLAS、POPL、PLDI、PPoPP、SIGCOMM
加入我们的5点原因
• 选择最基础,同时又最热门的研究方向
• 站在领域最前沿,从事国际一流的研究
• 广泛的国际交流机会
• 博士生4年级去耶鲁大学访问1-2年
• 目前已有10名研究生访问耶鲁
• 也很容易建立跟其他学校的交流
加入我们的5点原因
• 选择最基础,同时又最热门的研究方向
• 站在领域最前沿,从事国际一流的研究
• 广泛的国际交流机会
• 广阔的发挥个人兴趣的空间
• 两个研究/工程中心:
提供基础研究和应用型研究的选择
• 充分尊重学生自己的想法和思路
加入我们的5点原因
• 选择最基础,同时又最热门的研究方向
• 站在领域最前沿,从事国际一流的研究
• 广泛的国际交流机会
• 广阔的发挥个人兴趣的空间
• 良好的学习和生活环境
• 合肥和苏州,可以选择
欢迎你们的加入!
• 跟我们联系:
• 冯新宇:[email protected] , 15895437185
• 华蓓: [email protected] , 0551-63607043
• 张昱: [email protected], 0551-63603804
• 中科大-耶鲁高可信软件联合研究中心主页
• http://kyhcs.ustcsz.edu.cn
谢 谢!
主要平台
• 软件安全课题组和多核计算课题组
• 中科大 – 耶鲁高可信软件联合研究中心
• 基础研究为主
• 交换学生和教师互访等
• 与耶鲁大学的多位教授合作开展研究
• Zhong Shao(我校大师讲席教授), Richard Yang, Bryan Ford
卲中
Richard
Yang
Bryan
Ford
主要平台
• 软件安全课题组和多核计算课题组
• 中科大 – 耶鲁高可信软件联合研究中心
• 基础研究为主
• 交换学生和教师互访等
• 与耶鲁大学的多位教授合作开展研究
• Zhong Shao(我校大师讲席教授), Richard Yang, Bryan Ford
• 中科大 – 国创高可信软件工程中心
• 基础研究与产业化相结合
• 科大提供技术,科大国创公司提供资金(1000万)
和市场需求
• 嵌入式操作系统内核的验证、程序验证器的开发等
1.5h
2.5h
0.5h
主要研究方向
• 可信防崩溃系统软件
• 以形式化程序验证为手段,确保操作系统内核的可靠性、
正确性、安全性
程序(数学模型)
严格保证程序相对于其
规约没有bug
规约(数学描述)
验证
内存安全性、功能正确性、
终止性、实时性等
证明(可靠性证据)
主要研究方向
• 可信防崩溃系统软件
• 以形式化验证为手段,确保操作系统内核的可靠性、正
确性、安全性
• 研究各种相关的理论、程序设计语言和工具的支持
• 操作系统中断处理和多任务调度的验证、自动定理证明、可信
编译器的开发 …

similar documents