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