安全程序设计语言 | CNCC2021

贺飞

清华大学长聘副教授，博士生导师，CCF形式化专委会常务委员

主要研究程序验证理论、方法、工具及应用。开发了模型检测和软件验证工具，并应用于航空、航天、高铁等国家重大安全领域。在包括POPL, CAV, PLDI, OOPSLA, ICSE, ESEC/FSE, ASE等在内的国际重要会议和期刊上发表论文70余篇。主持和参与国家973项目、自然科学基金重大项目、科技支撑计划项目、重点研发项目等10余项。任《Theory of Computing Systems》编委，CONCUR, FMCAD, SAT, APLAS, ICECCS, SETTA等国际学术会议程序委员会委员。

赵永望

CCF杰出会员、浙江大学教授/博士生导师

担任ARINC653国际操作系统标准委员会委员、中国计算机学会(CCF)高级会员、CCF系统软件专委会和形式化方法专委会委员。曾任国际标准化组织 ISO/IEC JTC1 SOA研究组组长、新加坡南洋理工大学高级研究员。主要研究方向包括操作系统安全、形式逻辑与验证、编程语言原理等。主持和参与国家自然基金重点项目、核高基重大专项、重点研发计划等项目十余项，2011和2017年分别获得中国电子学会和山东省科技进步一等奖。

左志强

南京大学计算机科学与技术系副研究员

报告题目：安全C语言设计与实现

报告摘要：进入信息时代，软件已然成为现代社会的重要基础设施。确保软件安全可信，对维护信息安全以及社会生产具有重要意义。然而随着软件功能日趋复杂，规模日益增大，软件的安全可信面临愈加严峻的挑战，如何确保大规模软件的安全性，已然成为学术界、企业及政府高度关注的课题。本次报告重点介绍我们在安全C语言设计与实现方面的工作。在已有C语言的基础上，通过增加新类型，并结合动态、静态分析及编译技术，最终在编程语言与编译器层面保证软件安全。

个人简介：于新加坡国立大学获博士学位，曾在美国加州大学欧文分校从事博士后研究。科研工作聚焦于系统软件的可信保障与优化，在系统化程序分析、软硬件协同的编译器优化设计等方面取得重要进展，创新性工作以第一和通讯作者发表在包括PLDI、OOPSLA、EuroSys、ACM TOCS等国际重要学术会议和期刊上；独立研发并开源多个系统软件分析及优化系统，并已在华为、阿里等多个企业成功实现转化与应用；担任PLDI2022、FSE2022、IEEE TSE等多个国际重要学术会议程序委员及期刊审稿人。

曹钦翔

上海交通大学约翰霍普克洛夫特计算机科学中心助理教授、博导

报告题目：从程序验证到“开发即安全”

报告摘要：交互式定理证明技术是验证程序复杂性质的重要手段，其主要思想是在现有自动化验证工具无力完成验证工作的情况下，由人提供额外信息从而辅助验证工具“理解”程序并验证其功能以及安全性。经过探索，这一程序验证技术可以嵌入程序开发环境，从而实现“开发即安全”。本报告将介绍 Verified Software Toolchain（VST）工具，该工具以交互式定理证明技术为基础，集成了学术界在程序逻辑等诸多方面的理论研究前沿成果，可用于验证复杂 C 语言程序的功能正确性与安全性，排查空指针引用漏洞、缓冲区溢出错误、并发数据访问竞争等各种问题。

个人简介：曹钦翔，本科毕业于北京大学，博士毕业于美国普林斯顿大学，2018年回国任教，现为上海交通大学约翰霍普克洛夫特计算机科学中心助理教授、博导。其长期从事基于交互式定理证明的程序验证工具开发，并研究有关程序逻辑特别是分离逻辑的理论问题。曹钦翔是Verified Software Toolchain（VST）工具的主要开发者之一，首次实现了从业务逻辑，到源代码开发，再到编译的全链条正确性验证。

汪宇霆

上海交通大学John Hopcroft计算机科学中心副教授

报告题目：指令编码译码的形式化验证方法

报告摘要：机器指令的编码和译码规范是计算机体系结构中不可或缺的组成部分，从中衍生出的编码译码算法被广泛应用于各类处理机器代码的程序，包括编译器、汇编器、二进制程序分析软件等。使用形式化方法保障指令编码译码的正确性，对于从根本上提高这些程序的可靠性有重要意义。已有的该类方法存在一个本质缺陷：它们基于传统的、允许二义性的词法和语法分析，无法保证编码和译码算法互为逆过程，而这个性质对于确保二进制机器码运行的正确性至关重要。该问题导致已有的指令编码译码验证结果无法被应用于大多数实际程序。我们提出了一种新型的机器指令规约语言CSLED，其基于一种不带二义性的指令规约模型，可精确表达复杂体系结构中的指令格式。在此基础上，我们提出了一系列算法，从该语言描述的指令规约中自动提取编码译码过程，以及两者互为逆过程的形式化证明。该方法已被成功应用于验证CompCert可信编译器的X86汇编器后端。

个人简介：上海交通大学John Hopcroft计算机科学中心副教授，此前于美国耶鲁大学计算机系担任博士后研究员，博士毕业于美国明尼苏达大学双城分校。长期从事形式化方法方面研究，内容涵盖形式化验证和程序设计语言的理论基础（包括证明论、类型论、逻辑框架等）以及它们在关键性系统软件（如编译器和操作系统）中的应用，代表性研究成果以发表于形式化验证和程序设计语言的顶级国际会议（如POPL、CAV、OOPSLA、ESOP等）。此外，还致力于开发基于证明理论的定理证明工具，作为主要设计人员之一参与开发了基于高阶抽象语法的新型定理证明工具Abella（http://abella-prover.org），其已被成功应用于程序设计语言学术界的多个研究项目。

宋富

上海科技大学常任副教授

报告题目：密码程序安全威胁与形式验证

报告摘要：本报告介绍密码程序实现所面临的安全威胁，包括时间侧信道、功耗侧信道、缓存侧信道、故障注入等，总结面向安全威胁的形式验证技术与挑战，最后探讨我们的一些想法。

个人简介：宋富，上海科技大学常任副教授、研究员、博导，系统与安全中心主任。宋富博士于2013年4月获得巴黎大学（原巴黎狄德罗大学）计算机科学博士学位，同年8月加入华东师范大学任讲师，2016年1月破格晋升为副研究员，于2015年分别荣获上海市“浦江人才”和上海市“晨光学者”称号。2016年8月全职加入上海科技大学信息科学与技术学院，担任tenure-track助理教授、研究员，2021年7月晋升为常任副教授。研究领域包括模型检验、程序分析与验证、系统和AI安全，已在国际一流期刊和会议发表60多篇论文，如：IEEE TSE, ACM TOSEM, CAV, ICSE, ISSTA, S&P等。

狄鹏

蚂蚁集团程序分析团队负责人

报告题目：面向企业级微服务架构程序分析的IR设计

报告摘要：微服务是面向服务体系结构的最新发展趋势和研究热点，已经在工业实践中形成了广泛的应用。据统计，蚂蚁集团在2019年一年就提交了4亿行的基于微服务的代码。因此，微服务应用的安全性和可靠性时时刻刻影响着每一位互联网用户，正受到日益增长的关注。然而，作为软件安全的重要手段，程序分析往往难以应用到企业级微服务中，这是由系统的复杂性和庞大的代码量导致。Yannis在PLDI‘20就曾指出当前并没有一个很好的程序分析算法或框架，能在企业级微服务应用上得到一个全面令人满意的结果。针对这一问题，我们根据在蚂蚁大规模程序数据的实战经验，构思通过构建面向微服务的轻量弹性中间表达，重构数据驱动的微服务程序分析能力，满足可扩展性、多语言支持、基础分析模块化复用、开放生态等能力，并应用于工业DevSecOps的开发流程中。未来希望能依此为基础，形成新的开发模式生态。我们非常高兴能分享在蚂蚁程序分析的经验，并将挑战问题和同业者探讨。

个人简介：狄鹏，蚂蚁技术研究院可靠计算和软件工程实验室研究员，中国科学院兼职研究员，澳大利亚新南威尔士大学兼职高级讲师。狄鹏博士研究软件领域多年，其研究成果近年连续发布在PLDI、Micro等顶级学术会议。狄鹏和他的团队致力于研究软件分析、安全、可靠性等领域的前沿课题，聚焦打造蚂蚁新一代面向云侧企业级应用的软件分析研发系统，为蚂蚁集团数亿行代码构成的复杂软件系统的安全性保驾护航，并构建新一代的DevSecOps开发生态，提高云应用安全开发的效率。