网站备案流程详细/什么是网络整合营销

随着软件应用渗透日常生活的各个领域，软件的高可靠与高安全更加受到关注。本论坛将展现形式化方法与可信计算的最新成果，包括系统软件的可信安全实践、行业领域软件的可信应用等。这些问题既具有普适性，也给传统可信技术提出了迭代更新要求，以适应新的软件范式。本论坛的受众对象包括高校、研究所、工业企业、软件企业等可信计算研究者以及对可信计算有强烈需求的企事业单位。

根据本领域和方向的趋势，选定一个鲜明、通俗易懂、简练的主题。论坛鼓励围绕热点和开放问题展开：

论坛主席：

蒲戈光，华东师范大学教授博导，CCF形式化专委副主任。研究方向为形式化方法、软件工程。承担了科技部重点研发、核高基等10余项目，近五年在软工与形式化方法顶会发表论文20余篇，曾获ACM杰出论文奖。获上海市科技进步特等奖、教育部自然科学一等奖等多项省部级奖项。

共同主席：

贺飞，清华大学副教授，CCF形式化专委常委。研究方向为形式化验证理论、方法及应用。在包括POPL, CAV, PLDI, OOPSLA等在内的国际重要会议和期刊上发表论文60余篇。获ACM SIGSOFT 2018杰出论文奖，入选北京市高等学校“青年英才计划”。

赵永望 浙江大学 教授、博导

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

演讲题目：安全攸关操作系统形式化验证：技术与应用实践

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

吴志林 中国科学院软件研究所 研究员

个人简介：吴志林，中国科学院软件研究所计算机科学国家重点实验室研究员，博士生导师， “CCF-IEEE CS”青年科学家奖获得者。博士毕业于中国科学院软件研究所计算机科学国家重点实验室，先后在中国科学院自动化研究所中法计算机科学、自动化与应用数学联合实验室和法国波尔多第一大学LaBRI实验室从事博士后研究。2014-2015在巴黎第七大学IRIF实验室担任国家留学基金委公派访问学者。长期从事计算逻辑、自动机理论、程序验证相关的研究，在知名国际会议和期刊上发表论文30余篇，包括LICS、POPL、CAV、Information and Computation、IJCAR、CADE、CONCUR等。先后主持多项国家级项目，包括“十三五”全军共用信息系统装备预先研究项目、国家自然科学基金面上基金等；同时参与国家重点研发计划项目和国家自然科学基金面上基金项目多项。中国计算机学会形式化方法专业委员会委员，国际会议ATVA、ICECCS、LATA、GandALF等国际会议的程序委员会委员。

演讲题目：安全协议的状态及建模、验证与代码生成

演讲摘要：本报告将介绍形式化方法在安全协议(security protocol)开发中的应用。我们开发了一个使用状态机对安全协议进行建模、验证和代码生成的集成工具套件ISADT。ISADT允许对安全协议的控制逻辑和交互流程使用状态机进行建模，然后使用开源工具Proverif对安全协议的信息安全性质进行形式验证，最后从安全协议的状态及模型自动生成最终的代码。ISADT通过形式验证保证安全协议设计的安全性，通过代码自动生成提高了开发效率，并且减少了人工编码所导致的实现缺陷。我们使用ISADT针对一些典型的安全协议进行了实例研究，发现了一个终端高安全接入控制协议的设计缺陷，并得到了协议设计者的确认。

苏亭 华东师范大学 教授

个人简介：现为华东师范大学软件工程学院教授。主要的研究方向为软件工程、程序语言和软件安全，并一直致力于解决各类复杂软件系统的可靠性问题，特别是针对移动应用软件、工控嵌入式软件、编译器和程序分析软件的自动化测试和验证。目前已发表20篇国际顶级会议和期刊论文(CCF-A)，包括PLDI、ICSE、ESEC/FSE、ASE、TSE、CSUR。研究成果获得了三项ACM SIGSOFT杰出论文奖(ICSE 2018, ASE 2018, ASE 2019)。针对移动软件的研究获得了Google教授研究奖(2019)、ACM SIGSOFT杰出论文奖(ICSE 2018)、全国软件原型工具竞赛一等奖(NASAC 2017)、ACM学生学术竞赛第一名(ICSE 2016)；帮助腾讯微信、Google Gmail/Google+发现了多个软件错误。针对工控嵌入式软件的研究成果已转化为SmartRocket Unit单元测试工具，服务于十余家国内大型企业的软件生产部门。

演讲题目：移动应用软件的自动化测试：从崩溃错误到功能错误

演讲摘要：移动应用软件是一类以图形界面为交互、事件驱动的软件，其功能多样、运行环境复杂(如不同设备型号、系统版本和资源限制)。该类软件用户基数往往很庞大，市场竞争激烈，保证其可靠性和正确性对商业成功、团队信誉、用户忠实度具有重要意义，然而对其实现自动化测试极具挑战性。以安卓软件为例，截至2020年1月，安卓系统已占据移动市场超过74%的份额，每月全球活跃用户数超过20亿，每个月新增移动软件超过2万多个，自动化测试需求巨大。本报告将介绍我们团队在该领域内多年的研究成果，重点介绍我们提出的两类自动化测试方法、技术和工具，分别用于发现移动应用软件中的崩溃错误和功能错误。这两类测试方法已帮助众多安卓软件发现了大量未知软件错误。

赵鲁 华为安全工具部专家顾问，上海寰垒软件科技开发咨询中心技术负责人

个人简介：2012年在犹他大学获得计算机博士学位。曾先后在硅谷担任HP Fortify高级应用安全工程师，Oracle/NetSuite担任首席应用安全工程师，和创业公司Secregen的CTO。主要工作和研究方向为应用程序的安全分析，包括形式化验证、静态和动态程序分析技术，和它们在程序安全分析中的综合应用。作为核心成员参加业界领先的静态源码分析工具Fortify SCA研发，主持了NetSuite云服务安全代码审核周期和流程，开发了独立企业证书管理和通信系统。曾获得多个在软件安全分析领域的美国和国际专利。引领华为的形式化验证软件安全项目和静态安全分析工具项目。

演讲题目：杜绝关键安全漏洞——形式化验证无缓冲区溢出的应用实践和挑战

演讲摘要：业界常用渗透测试和静态源码分析来检测软件产品中的安全漏洞，可是这些方法都存在无法忽视的漏报和误报。对于软件系统里面有着高安全风险的模块来说，如何保证它们没有某些特定的高危漏洞是一个学术界和业界共同的研究和实践难题。本工作介绍SecVerifier验证平台，它用形式化验证技术来保证华为产品代码里面没有缓冲区溢出这一安全风险极高、后果极严重的漏洞。它完成了十几万行代码的自动验证，发现了60+ 缓冲区溢出和30+ 空指针引用漏洞。它验证成功的代码保证了没有缓冲区溢出问题。尽管如此，我们依然面临着复杂的技术挑战，希望和有关的研究人员共同解决这些难题。