中科大耶鲁高可信软件联合研究中心-介绍资料.ppt

可信软件与多核计算 报告人：冯新宇 研究背景 处理能力越来越强 多核、众核、GPU … 问题规模越来越大 网络、云计算、大数据… 安全性需求越来越高 软件应用越来越广、计算环境日益复杂 研究方向 如何算的“快”？ 如何充分利用多核（众核）计算资源，解决计算问题？ 新的算法、操作系统、编程语言和模型等 如何算的“对”？ 软件的正确性、可靠性、安全性等 高可信软件：如何开发没有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平台上验证。 新型的编程语言支持 网络程序的分析和验证 华蓓 冯新宇 研究团队 陈意云 张昱 郭宇 付明 李兆鹏 冯新宇 华蓓 卲中（耶鲁） 主要平台 软件安全课题组多核计算课题组 中国科大-耶鲁高可信软件联合研究中心 耶鲁方合作者： 基础研究为主 交换学生、 教师互访等 主要平台 软件安全课题组多核计算课题组 中国科大-国创高可信软件工程中心 基础研究与产业化相结合 科大提供技术，国创提供资金（1