——系统软件与软件安全实验室简介 报告人：冯新宇 构造安全、高效的系统软件 ——系统软件与软件安全实验室简介 报告人：冯新宇

研究背景 处理能力越来越强 应用的日益多样化 安全性需求越来越高 多核、众核、GPU … 网络、云计算、大数据、移动计算 … 电子支付、医疗、无人驾驶汽车、航空航天、核电… Heartbleed: SSL buffer overflow bug

研究背景（二） 系统软件：软件系统的核心 操作系统、虚拟机、程序设计语言和编译器、数据 库、网络软件、设备驱动等 几乎所有的应用都离不开系统软件的支持

研究方向 如何算的“快”？ 如何算的“对”？ 如何服务于新兴的计算需求？ 如何充分利用多核（众核）计算资源，解决计算问题？ 新的算法、操作系统、编程语言和模型等 如何算的“对”？ 软件的正确性、可靠性、安全性等 高可信软件：如何开发没有bug的软件？ 如何服务于新兴的计算需求？ 如何从性能和可靠性两个方面为新兴应用提供支持？ 应用：嵌入式和移动系统、网络、云计算、大数据

研究团队 邵中（耶鲁） 冯新宇 华蓓 陈意云 张昱 郭宇 梁红瑾 李兆鹏 付明

面向多核的 新型操作系统和程序语言

多核计算：主要挑战 7x 3.6x 1.8x Time: Moore’s law Speedup User code Traditional Recall the traditional scaling process for software: write it once, trust Intel to make the CPU faster to improve performance. Traditional Uniprocessor Time: Moore’s law

Unfortunately, not so simple… 多核计算：主要挑战 Speedup 1.8x 7x 3.6x User code With multicores, we will have to parallelize the code to make software faster, and we cannot do this automatically (except in a limited way on the level of individual instructions). Multicore Unfortunately, not so simple…

多核计算：主要挑战 2.9x 2x 1.8x Parallelization and Synchronization Speedup 2.9x 2x 1.8x User code Multicore This is because splitting the application up to utilize the cores is not simple, and coordination among the various code parts requires care. Parallelization and Synchronization require great care…

多核计算：主要挑战 并发程序开发及正确性 大量的不确定性 难以编程、易出错、难测试/调试

多核计算：主要课题 确定性并行编程模型和操作系统 确定性操作系统Dlinux 确定性并行 编程模型 确定性共享虚存模型: 不同读写特征的内存区域 只读、单生产者-多消费者模型、DiffMerge 进程/线程的动态管理、I/O的确定性并行 确定性并行 编程模型 张昱

多核计算：主要课题 程序分析与变换技术及工具 针对C/Java/JavaScript/Android等应用程序 发现程序错误，理解程序行为，提高程序性能 集中于内存使用和并发控制方面 Java虚拟机(Apache Harmony)上即时编译器辅助的垃 圾收集 C函数调用图构建工具 代码段分离工具 张昱

多核计算：主要课题 并发算法正确性的验证 栈、队列、集合等并发对象的验证 并发垃圾收集算法的验证 部分算法来自于java.util.concurrency包 并发垃圾收集算法的验证 算法在Java虚拟中使用 发现了外科手术机器人控制程序中并发算法的bug 冯新宇

网络与多核计算

网络与多核计算：主要挑战 传统网络设备 问题 解决方案 基于特定应用和需求，通过思科、 华为等厂商定制各种各样的盒子 周期长，成本高 基于特定应用和需求，通过思科、 华为等厂商定制各种各样的盒子 问题 周期长，成本高 无法适应日益多样化的集群和网络结构、应用需求等 数据中心、云平台等 解决方案 通用服务器 + 编程 来取代 “定制盒子” 高效算法和服务器、软件定义网络、网络功能虚拟化

网络与多核计算：主要课题 基于多核/众核处理器的高速网络算法/系统 基本思路 基于多核服务器的 高速网络流量监视系统 基于GPU的算法加速 利用通用多核服务器构建高速网络系统 研究突破网络系统瓶颈的关键技术 基于多核服务器的 高速网络流量监视系统 可支持10Gbps链路速度和 几百万TCP连接规模 由合作企业完成成果转化 基于GPU的算法加速 异常检测，数据压缩，数据流加密，...... 华蓓

网络与多核计算：主要课题 软件定义网络（SDN）和网络功能虚拟化 （NFV） 网络领域最热门的研究方向 课题：高性能NFV平台 软件实现网络功能，无需“定制盒子” 课题：高性能NFV平台 课题：SDN辅助的流量迁移 课题：SDN的程序语言支持 华蓓 冯新宇

软件安全

软件安全：需求与挑战 电子商务和移动支付 安全攸关/任务攸关系统

软件安全：需求与挑战 电子商务和移动支付 安全攸关/任务攸关系统 如何发现系统中的缺陷和安全漏洞、 如何严格保证系统的可靠性、正确性和安全性？ 新的研究热点

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

软件安全：主要课题 安卓系统隐私泄露漏洞检测 发现隐私泄露漏洞并阻止 代码检查+ 动态监控 实用工具开发 冯新宇

软件安全：主要课题 实时嵌入式操作系统uC/OS-II内核的验证 使用数学工具，证明系统的安全性、正确性等 约6000行代码 满足安全攸关/任务攸关需求 冯新宇 Parrot Drone

软件安全：主要课题 CertiKOS虚拟机（Hypervisor）的验证 将CertiKOS部署在 无人驾驶汽车（LandShark）上 项目进行中 Zhong Shao （耶鲁）

软件安全：主要课题 C程序安全和可靠性分析和验证工具、 可信编译等 C程序的自动分析、验证 编译后自动生成关于二进制程序的证明 陈意云 无需相信编译器的正确性 陈意云

研究团队 邵中（耶鲁） 冯新宇 华蓓 陈意云 张昱 郭宇 梁红瑾 李兆鹏 付明

主要平台 中国科大-耶鲁高可信软件联合研究中心 系统软件与软件安全实验室 基础研究为主 交换学生、 教师互访等 耶鲁方合作者： 卲中 Richard Yang

科大提供技术，国创提供资金（1000万）和市场需求 主要平台 基础研究与产业化相结合 科大提供技术，国创提供资金（1000万）和市场需求 系统软件与软件安全实验室 中国科大-国创高可信软件工程中心

主要平台 中国科大-耶鲁高可信软件联合研究中心 系统软件与软件安全实验室 中国科大-国创高可信软件工程中心

加入我们的5点原因 选择最基础，同时又最热门的研究方向 多核、软件定义网络（SDN）、软件安全、 防崩溃代码等 理论问题和现实需求相结合 良好的就业前景 毕业生去向——企业：微软、Intel、思科、华为、BAT等 毕业生去向——高校、科研院所：留校、深圳先进技术研 究院等

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

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

加入我们的5点原因 选择最基础，同时又最热门的研究方向 站在领域最前沿，从事国际一流的研究 我们的多项研究处于国际领先地位 邵中：近年来Certified Software概念的主要倡导者之一 [CACM 2010] 冯新宇和邵中被列为国际上防崩溃代码的主要研究人员 多篇顶级期刊和会议文章 TOPLAS、POPL、PLDI、PPoPP、SIGCOMM PPoPP’06：国内首篇 POPL’12：国内首篇 ACM TOPLAS：国内第二篇

并发算法验证：里程碑式的工作

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

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

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

欢迎你们的加入！ 跟我们联系： 冯新宇：xyfeng@ustc.edu.cn ， 15895437185 华蓓： bhua@ustc.edu.cn ， 18056028579 张昱： yuzhang@ustc.edu.cn, 13866131689 邵中/陈意云：yiyun@ustc.edu.cn, 13866750058

谢 谢！