系统软件安全技术论坛

NASAC

系统软件是计算机系统运行的基础，包含以操作系统为代表的基础系统软件和以无人车、大飞机、工业控制软件为代表的领域系统软件。系统软件是互联网基础设施的核心组成部分，任何系统软件安全问题会直接危害在其上运行的应用程序安全，因此其安全性对于计算机系统乃至网络空间安全至关重要。为此，本论坛围绕“系统软件安全技术”进行研讨，特邀国内外顶尖的系统软件安全研究团队和来自企业的安全工程团队，进行专题报告，深入探讨系统软件安全的核心话题。

论坛组织委员会：

申文博（浙江大学）

常 瑞（浙江大学）

周亚金（浙江大学）

论坛主持人：

申文博（浙江大学）

常 瑞（浙江大学）

日程安排：

时 间：2020年11月21日（星期六）13:30-17:00

地 点：重庆富力假日酒店 宴会厅3

论坛议程：

报告及嘉宾简介：

1. 陈海波：软硬件协同的系统安全增强技术研究

摘要：Meltdown/Spectre、Rowhammer等新型硬件安全漏洞以及AI在安全攻防领域的广泛应用使得当前计算机系统面临巨大的安全威胁。该报告将回顾当前计算机系统面临的安全挑战，并且分析当前硬件安全扩展与AI带来的安全增强机会，并介绍当前国际学术界以及上海交大IPADS团队在系统安全方面的一些工作，并且展望未来的研究方向。

简介：陈海波，上海交通大学特聘教授，并行与分布式系统研究所所长，领域操作系统教育部工程研究中心主任，国家杰出青年基金获得者、ACM杰出科学家。主要研究领域为操作系统和系统安全。曾获教育部技术发明一等奖（第一完成人）、CCF青年科学家奖、全国优秀博士学位论文奖等。目前担任ACM SIGOPS ChinaSys主席、CCF系统软件专委会副主任、ACM旗舰杂志《Communications of the ACM》中国首位编委与Special Sections领域共同主席、《ACM Transactions on Storage》编委。曾任ACM SOSP 2017年大会共同主席、ACM CCS 2018系统安全领域主席、ACM SIGSAC奖励委员会委员。按照csrankings.org的统计，其在操作系统领域近5年（2015-2019）发表的高水平会议（SOSP/OSDI，EuroSys，Usenix ATC和FAST）论文数居世界第一。

2. 秦承刚：可信基础设施的实践

摘要：蚂蚁集团在2020年双11实施了可信安全容器集群，通过安全容器、数据加密、可信启动等技术初步实践了可信基础设施。同时，在积极探索通过软硬件结合持续提升金融数据中心的隔离性、机密性与完整性。此次论坛以蚂蚁在操作系统、安全沙箱、硬件加速、可信根等系统安全技术上的实践为基础，像大家介绍工业界在系统安全领域的最新进展

简介：秦承刚，蚂蚁集团资深技术专家，任职于可信原生技术部，带领可信硬件与内核团队，专注在可信金融基础设施的技术创新与研发工作，涉及操作系统/安全容器等系统软件及软硬件结合领域。在ASPLOS，SoCC等学术会议上发表过多篇论文。

3. Fu Song：Formal Verification of Masking Countermeasures for Arithmetic Programs

摘要：Cryptographic programs may be vulnerable to practical power side-channel attacks, which may infer private data via statistical analysis. To thwart these attacks, several masking schemes have been proposed, giving rise to effective countermeasures for reducing the statistical correlation between private data and power consumptions. However, designing effective masking programs is a labor intensive and error-prone task. Existing formal verification approaches either are currently limited to Boolean programs or suffer from low accuracy. In this work, we propose an approach for formally verifying masking countermeasures of arithmetic programs. Our approach is essentially a synergistic integration of type inference and model-counting based methods. The type inference system allows a fast deduction of leakage-freeness of most intermediate computations, the model-counting based methods accounts for completeness. A distinguished feature of our type system lies in its support of compositional reasoning when verifying programs with procedure calls, so the need of inlining procedures can be significantly reduced. We have implemented our methods in a verification tool QMVERIF which has been extensively evaluated on cryptographic benchmarks including full AES, DES and MAC-Keccak. The experimental results demonstrate the effectiveness and efficiency of our approach, especially for compositional reasoning. In particular, our tool is able to automatically prove leakage-freeness of arithmetic programs for which only manual proofs exist so far; it is also significantly faster than the state-of-the-art tools: EasyCrypt on common arithmetic programs, QMSINFER, SC Sniffer and maskVerif on Boolean programs.

简介：Fu Song is an Assistant Professor at School of Information Science and Technology in the ShanghaiTech University. Fu received his Ph.D. from University Paris Diderot (Paris 7) in 2013. He was an Associate Research Professor and Lecturer at School of Computer Science and Software Engineering in the East China Normal University during 2013-2016, and a visiting researcher at Computer Security Lab of Nanyang Technological University in 2014. His research spans formal verification, program analysis and cyber-security. Fu has published more than 50 papers in peer-reviewed conferences and journals including CAV、ICSE、ISSTA、IEEE S&P、AAAI、IJCAI、I&C, IEEE TSE and ACM TOSEM. He has been the recipient of the EASST best paper award at ETAPS 2012、Shanghai Pujiang Talent and Shanghai Chenguang Scholar.

4. 赵永望：操作系统安全形式化验证技术与应用

摘要：安全攸关操作系统主要应用于航空、航天、轨道交通、无人系统等领域，它位于计算机系统软件栈的底层，操作系统的错误可能导致系统奔溃、被攻击等问题，涉及功能安全和信息安全等问题。操作系统功能结构复杂，多核多任务的并发度高，开发与调试都十分困难，一些隐藏的错误用常见的软件测试技术难以发现，而形式化验证可帮助软件开发人员发现深层的错误，确保操作系统的高安全可靠性。本报告主要讨论操作系统形式化验证的背景意义、国内外现状和面临的挑战，介绍我们提出的系统方法、理论技术以及工业应用实践。

简介：赵永望，浙江大学 教授、博导，担任ARINC653国际操作系统标准委员会委员、国际信息技术安全评估标准(Common Criteria,CC)操作系统内核技术委员会委员、CCF系统软件专委会和形式化方法专委会委员。主要研究方向包括操作系统安全、形式化验证、编程语言等。提出了操作系统形式验证的系统性理论和方法，突破了覆盖单核到多核、标准到产品、模型到源码的形式化验证关键技术，完成了10多个国内外操作系统的形式验证工作，显著提升国产系统的安全可靠性。相关研究成果得到美国波音、法国空客和国际知名实时操作系统厂商的认可，被纳入国际标准，并在开源实时操作系统社区产生影响力。

论坛组织：

1. 组织者：申文博

简介：申文博，浙江大学百人计划研究员，博士生导师。2015年获得美国北卡罗莱纳州立大学计算机博士学位，研究方向为系统及无线安全，并于同年加入位于美国硅谷的三星美国研究院（Samsung Research America），担任操作系统内核安全的技术负责人。于2019年加入浙江大学网络空间安全研究中心和计算机科学与技术学院。申文博研究员研究成果包含论文及专利30余篇，覆盖全部计算机安全四大国际会议，获得2项杰出论文奖，包含四大顶级会议之一的NDSS的杰出论文奖。申文博研究员常年活跃于移动系统安全攻防的第一线，通过分析实际攻击，设计相应的操作系统保护方案，具有学术界和工业界的双重研究经历和视野；多年来设计、实现并主导部署了多种操作系统内核安全机制，保护超过亿部设备系统内核安全。

2. 组织者：常瑞

简介：常瑞，副教授，博士生导师，浙江大学。从事系统安全方向的科研与教学十余年，于解放军信息工程大学获得计算机科学与技术博士学位，并获ACM中国优秀博士学位论文分会奖。研究兴趣围绕嵌入式系统安全，研究方向包括可信执行环境安全防护、系统安全加固、形式化分析与验证、边缘计算安全等，现任国家信息标准委员会专家、IEEE 可信设备扩展标准项目副主席（P2811.6），近三年发表相关学术论文四十余篇。加入浙江大学前曾就职于中国人民解放军信息工程大学，期间多项研究成果获得省部级以上奖励(省部级教学成果一等奖1项、省部级科技进步二等奖2项等)，教学方面获得全国微课竞赛二等奖、省部级一等奖等，被评为全军优秀教师。

3. 组织者：周亚金

简介：周亚金，浙江大学网络空间安全学院/计算机学院百人计划研究员（博导）。周老师于2015在美国北卡州立大学获得博士学位，随后担任奇虎360高级安全研究员，从事移动安全产品研发工作。2018年加入浙江大学。他发表了40多篇学术论文，包括安全四大会议10篇，四次获得最佳论文奖，包括EURO S&P 2019（国内首次）。他的研究具有较大的影响，总引用数超6500次，h-index 17。两篇文章入选自1981年以来全球引用最多的安全论文前100篇列表。入选AMiner 2009到2019年全球安全和隐私领域最有影响力的100位研究者列表（排名48）。作为指导老师之一，参加美国国立卫生部主办的2019 iDash全球基因安全计算SGX赛道，开发的基于硬件的隐私机器学习系统性能比第二名领先数十倍，以绝对优势获得全球第一名（国内首次）。他受邀担任过个顶级安全学术会议的程序委员会委员，包括CCS, IEEE S&P以及EURO S&P。他的研究工作得到了华尔街日报、中央电视台等媒体报道和谷歌、facebook、三星等企业的致谢。