返回首页
您的位置:首页 > 新闻 > CCF新闻 > CNCC

CNCC|形式化验证技术如何保障计算机软硬件系统安全?

阅读量:938 2022-09-30 收藏本文

图片


CNCC2022将于12月8日至10日在贵州省贵阳市国际生态会议中心举办,今年CNCC技术论坛数量达到122个,内容涵盖了“计算+行业、人工智能、云计算、教育、安全”等30个方向。本文特别介绍12月9日举办的【计算机软硬件系统安全性形式化验证】技术论坛。


报名及了解更多技术论坛信息请识别下图二维码进入CNCC2022官网。目前早鸟票限时优惠报名正在进行,抓住机会立享大幅优惠!

图片



计算机软硬件系统(比如自动驾驶系统与区块链)一方面与人们日常生活深度融合,关系到人民群众生命财产安全;一方面支撑航空航天、高铁等关键领域,直接影响国家安全。因此计算机软硬件系统的安全性愈发重要,要求越来越高。


形式化验证技术具有严格数学基础,包括定理证明、模型检验、约束求解、抽象解释等多种方法;经过多年发展,其已经成为保障计算机软硬件系统安全性的重要途径,并成功应用于航空航天控制软件、操作系统内核、编译器、硬件设计、网络协议等领域,从而受到学术界和工业界的广泛关注。


本论坛将邀请来自学术界和工业界的顶尖专家,共同探讨计算机软硬件系统安全性形式化验证的前沿理论、技术、与应用,并展望发展趋势。


论坛安排


顺序

主题

主讲嘉宾

单位

1

系统安全形式化验证:从交互式到自动化

赵永望

浙江大学

2

后摩尔时代通过验证提升性能的工业实践

付明

华为德国德累斯顿研究所

3

面向应用的硬件模型检测技术

张弘策

香港科技大学(广州)

4

SATSMT

蔡少伟

中国科学院软件研究所

5

基于抽象内存模型的C程序编译验证

汪宇霆

上海交通大学

6

程序隐私安全性的形式验证

宋富

上海科技大学


Panel环节

胡振江

詹乃军

 

及其他主讲嘉宾

北京大学

中国科学院软件研究所


论坛主席


图片

吴志林

中国科学院软件研究所 研究员


“CCF-IEEE CS”青年科学家奖。博士毕业于中科院软件研究所,后任中科院自动化研究所和法国波尔多第一大学博士后。2014-2015在巴黎第七大学任访问学者。长期从事计算逻辑、自动机理论、程序验证相关研究,在知名国际会议和期刊上发表论文30余篇,如LICS、POPL、CAV、Information and Computation、IJCAR、CADE、CONCUR等。主持多项国家级项目。任ATVA‘22程序委员会共同主席, ATVA、ICECCS、LATA、GandALF等程序委员会委员。


论坛共同主席


图片

张昕

北京大学 研究员/助理教授


国家级青年项目入选者。上海交通大学学士,美国佐治亚理工学院博士,2017-2020年于美国麻省理工学院任博士后,2020年加入北京大学。研究领域为程序设计语言和软件工程,重点为编程系统和机器学习的交叉方向。一方面,利用机器学习技术来提高程序分析等编程系统的可用性,另一方面,开发了新的程序分析和语言以提高机器学习系统的质量。工作发表在 PLDI、POPL、FSE、NeurIPS 等顶级会议上,获 PLDI'14 和 FSE'15 杰出论文奖。曾任 PLDI等国际会议程序委员会委员。


报告及讲者介绍


图片

赵永望

浙江大学 教授


CCF杰出会员,CCF系统软件专委、形式化方法专委和抗恶劣计算专委执行委员。移动终端安全浙江省工程研究中心主任,工信部重大专项首席科学家,主要研究方向为系统安全、形式化验证、编程语言等,相关成果发表在ACM TOPLAS、IEEE TDSC等期刊和CAV、FM、TACAS等会议上。


报告题目:系统安全形式化验证:从交互式到自动化


本报告主要介绍软硬件系统安全的概念、要求和面临的挑战,分析对比各类系统安全验证方法。然后,介绍形式化验证的技术框架,以及国内外最新的发展趋势和应用情况。最后,分析当前系统安全形式化验证面临的问题,着重讨论当前交互式验证与自动化验证的现状,得出形式化验证在自动化方面的挑战与价值。

图片

付明

华为欧洲研究院德国德累斯顿研究所 所长


中国科学技术大学博士,操作系统和形式化方法技术专家。2017年加入华为OS内核实验室,带领形式化验证团队从事内核设计、开发和验证工作,2019年外派德国创建德累斯顿研究所,主要研究方向是操作系统、并发理论和并发程序形式化验证,致力于将形式化方法应用于工业系统软件的开发中,在形式化方法、程序语言理论和操作系统等领域的顶会POPL、CAV、CONCUR、SOSP、ASPLOS、USENIX ATC上发表多篇论文,并获得ASPLOS’21杰出论文奖。


报告题目:后摩尔时代通过验证提升性能的工业实践


后摩尔定律时代,硬件趋向于多核异构,高可靠和高性能的多核并发控制是高效发挥多核算力的关键,而多核体系结构下的弱内存序和NUMA等特性给多核并发控制带来了新的挑战。本报告将介绍华为最近在应用形式化方法构建多核并发基础库方面的一些工业实践,通过形式化验证和优化工具的有效支持,使得程序员有信心做更为激进的多核并发控制算法的设计和优化,有效提升多核并发基础库的性能,同时提供正确性保证。

图片

张弘策

香港科技大学(广州) 助理教授


功能枢纽微电子学域助理教授。2015年本科毕业于上海交通大学,2021年于普林斯顿大学电子与计算机系取得博士学位,主要研究硬件领域的形式化方法应用。曾获得2020 ACM TODAES最佳文章奖,曾担任DAC, ChinaSoft等会议审稿人。


报告题目:面向应用的硬件模型检测技术


现代大规模集成电路的设计与验证离不开软件工具的辅助。形式化方法在数字集成电路逻辑验证工具中的应用主要包括等价性检查与模型检测。相比于等价性检查,模型检测受电路规模制约的问题更加明显,因此提升模型检测工具的性能是一个核心问题。一种可能的解决方案是面向应用问题分析优化算法。本次报告会介绍硬件形式化方法的一类应用场景——指令功能的形式化检查,以及对应的专用模型检测方法的研究。

图片

蔡少伟

中国科学院软件研究所 研究员,中国科学院大学 岗位教授,中科院青促会信息与管理分会 会长


中科院优秀导师,获国家优青项目,入选智源青年科学家,长白山领军人才。北京大学博士,主要研究约束求解、组合优化。发表60多篇顶级期刊和会议论文,获AIJ近五年最受欢迎论文,SAT 2021最佳论文奖。在国际SAT比赛获8次冠军10余次亚军,获SMT比赛多个冠军,EDA Challenge亚军,3个联合逻辑奥林匹克金牌。研究成果应用于国内龙头企业的芯片验证,操作系统验证,微软云平台的故障检测和虚拟机预配置,腾讯地图调度和优化,MIT材料研究等重要项目。


报告题目:从SAT到SMT


命题逻辑可满足性问题(SAT)是计算机科学的核心问题之一,也是密码分析的主要方法之一。SMT是特定背景下一阶逻辑公式可满足性问题,是对SAT的重要扩展,可以视为命题逻辑框架和背景理论如线性算术理论的结合,可以更方便的表达涉及数学理论和数据结构的约束问题。SAT和SMT是EDA和软件验证的核心引擎。本报告介绍SAT和SMT的主要方法。

图片

汪宇霆

上海交通大学 副教授


美国明尼苏达大学博士,曾任美国耶鲁大学计算机系博士后。长期从事形式化方法研究,包括形式化验证和程序设计语言的理论基础(证明论、类型论、逻辑框架等)以及它们在关键系统软件(如编译器和操作系统)中的应用,代表性成果发表于POPL、CAV、OOPSLA、ESOP等国际顶会。并致力于开发基于证明论的定理证明工具,作为主要设计人员之一参与开发了基于高阶抽象语法的新型定理证明工具Abella,其已被成功应用于程序设计语言学术界的多个研究项目。


报告题目:基于抽象内存模型的C程序编译验证


C程序的编译验证是形式化验证领域的一个重要问题,已有工作依赖基于全局约束的内存模型,难以描述局部内存结构、以及支持局部内存转换算法的模块化验证。这些问题极大阻碍了C程序编译验证方法的进一步发展。我们提出了一种通过名义技术(Nominal Techniques)对内存结构进行抽象表示的方法,并使用该方法移除全局内存约束,使得复杂局部内存性质的表述成为可能。通过整合该抽象内存模型和CompCert,我们实现了C程序到机器码完整编译过程的正确性验证。

图片

宋富

上海科技大学 系统与安全中心主任/常任副教授/研究员


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


报告题目:程序隐私安全性的形式验证


软件程序的运行常涉及隐私相关数据,比如密码、用户个人信息等。因此,如何通过技术手段保障攻击者无法通过程序运行时的可观察信息来获取相关隐私信息已经成为国内外的研究热点。本报告将探讨运行时编译优化和多方安全计算场景中的程序隐私安全性的形式验证。


Panel嘉宾


图片

胡振江

北京大学计算机学院 院长/讲席教授

图片

詹乃军

CCF形式化方法专委 副主任

中科院软件所 研究员,中国科学院大学 岗位教授,计算机科学国家重点实验室 副主任


图片








图片

CNCC是级别高、规模大的高端学术会议,探讨计算及信息科学技术领域最新进展和宏观发展趋势,展示计算领域学术界、企业界最重要的学术、技术成果,搭建交流平台,促进科技成果转换,是学术界、产业界、教育界的年度盛会。今年邀请嘉宾包括ACM图灵奖获得者、田纳西大学教授Jack Dongarra以及高文、管晓宏、江小涓、钱德沛、徐宗本、张平等多位院士,还有七百余位国内外名校学者、名企领军人物、各领域极具影响力的业内专家,CNCC在计算领域的水准及影响力逐年递增。本届CNCC的主题是:算力、数据、生态。


CNCC2022将汇聚国内外顶级专业力量、专家资源,为逾万名参会者呈上一场精彩宏大的专业盛宴。大会期间还将举办“会员之夜”大型主题狂欢活动,让参会者畅快交流,燃爆全场。如此盛会,岂能缺席!等你来,马上行动,欢迎参会报名!



图片

图片


图片

图片