安全攸关软件设计与验证：技术前沿与工业应用 | CNCC2021

随着计算机技术应用的日益普及和不断深入，软件系统的规模和复杂性急剧增大，软件在越来越多的系统中成为主要的使能部件。在航空航天、武器装备、医疗设备、交通、核能、金融等安全攸关的应用领域，软件系统失效将导致灾难性的后果，保障软件系统的质量成为迫切的需求和挑战。建模、分析与验证是保障软件系统质量的重要环节和手段。其次，随着国产化软件的快速发展和替代应用，安全攸关软件的设计与验证技术对于国内工业界的软件安全可靠性也具有重大意义。本论坛采用学术界的技术前沿报告与工业界的创新应用报告相结合的方式，分享安全攸关软件设计与验证的国内外技术前沿，以及在航空、航天、汽车、轨道交通、通信等领域的实际案例与成效。

赵永望

浙江大学 教授/博导

浙江大学计算机科学与技术学院、网络空间安全学院，教授/博士生导师，移动终端安全浙江省工程实验室主任，CCF系统软件专委、形式化方法专委和抗恶劣计算专委委员，国际ARINC653操作系统标准委员会成员。主要研究方向包括形式化方法、操作系统安全、编程语言等。主持和参与国家自然基金重点项目、核高基重大专项、重点研发计划等项目二十余项，2011和2017年分别获得中国电子学会和山东省科技进步一等奖。

牛文生

中航机载系统共性技术有限公司，执行董事、总经理、研究员

牛文生，男，研究员职称，博士，博士生导师，公司执行董事、总经理，享受国务院特殊津贴，部级有突出贡献专家，航空工业核心计算平台技术首席技术专家。主要从事抗恶劣环境高可靠嵌入式高速计算机相关技术研究。主持及参与研究的多项课题及关键技术获得国家科技进步奖，在国内外多家权威专业刊物发表学术著作多篇。曾被授予“部级有突出贡献中青年专家”称号，“国防科技工业有突出贡献中青年专家”称号和航空工业集团“航空报国优秀贡献奖”等。

报告题目：机载产业发展与高校人才培养

报告摘要：从机载系统是航空产业的重要组成部分、机载系统产业特征、国家对航空产业的规划、当前机载产业的规模分析、新技术的不断涌现及面临的数字化转型等方面详细阐述了国内机载产业的发展现状。并从国内高等教育的现状、高等教育与机载产业发展的衔接（包含体系、文化、能力、人员四个方面的衔接）以及当前在关键技术突破、自主可控、人力资源扩充需求及产学研一体化发展的模式等方面存在的问题上，提出了面向机载系统产业发展的产学研用协同生态系统的解决思路，着重从以产业集群为基础的创新技术研究、产学研用一体化的基础核心部件研发、产学研用一体化的工业应用软件研发及高效的培训模式、支持产学研用合作的商务模式五个方面开展建设工作。

蒲戈光

上海工业控制安全创新科技有有限公司总经理，华东师范大学 教授、博导，CCF形式化专委会副主任

蒲戈光，上海工业控制安全创新科科技有限公司总经理。研究聚焦形式化方法与软件工程领域，在软件验证理论与算法，与工业级验证工具研发等方面做出了创新贡献。目前担任科技部重点研发计划专项“人工智能安全可信理论及验证平台“首席科学家。研究成果曾获ACM 杰出论文奖，上海市科技进步特等奖，北京市科技进步一等奖等奖项。主导研发的多种创新验证与测试算法对发现真实软件缺陷非常有效，其中研发的两款工业级软件验证工具服务了30余家企业，有效提升了企业软件开发的质量与效率，并成功支撑嫦娥五号飞行器、北斗二号卫星、上海无人驾驶17号线等重大工程的顺利实施。

报告题目：软件验证工具的工业实践与未来挑战

报告摘要：形式化技术在工业界的应用有一定的技术壁垒，重要的原因是对专业人员的素质有较高的要求。通过研制软件验证工具帮助研发人员降低形式化技术的使用壁垒，对提升研发的质量具有重要意义。我们讨论了软件验证工具的几种形态，包括在芯片领域、轨道交通领域、航空航天领域的实际应用案例。同时，对形式化技术在工业界遇到的困难以及未来的挑战提出了分析与展望。

程胜

中国载人航天工程软件工程和数字化技术发展与管理中心 主任、研究员

国务院特贴专家，中国航天科技集团学术带头人，兼任中国载人航天工程软件专家组副组长、数字化专家组副组长，长期从事航天共性软件和软件工程技术研究，主持了国家核高基重大专项“航天装备强容错实时操作系统及开发环境”等项目研制，研制成功我国航天领域首个自主的通用化强容错实时操作系统及软件开发环境，已经在我国载人航天工程等重大航天工程以及新一代卫星、导弹武器、运载火箭等装备中广泛应用。发表论文30多篇，出版专著3本。作为主要完成人获得过多项省部级科技奖励。荣获“中国载人航天工程突出贡献集体”、“航天十大杰出青年”、“航天创新奖”等荣誉。

报告题目：载人航天工程软件设计和验证技术发展

报告摘要：二十多年来，中国载人航天工程取得了举世瞩目的成就，软件工程化以及软件设计验证技术为保障历次飞行任务成功发挥了重要作用。报告介绍载人航天工程软件工程化以及软件设计和验证技术的发展历程、未来软件任务形势以及后续软件设计和验证技术发展趋势。

姜宇

清华大学软件学院 副教授、博导

清华大学软件学院副教授，博士生导师。研究方向为软件系统的动态安全测评分析，在广泛使用的系统软件中挖掘140个漏洞被收录入中美国家信息安全漏洞库，核心成果被并入AFL++, Google ClusterFuzz, Microsoft OneFuzz等模糊测试平台, 以第一作者或通讯作者在ACM SOSP, USENIX Security及IEEE S&P 等会议上发表论文70余篇, 获ACM EMSOFT，ICSE-SEIP等会议最佳论或提名奖6次，作为项目负责人主持华为、微众银行、阿里巴巴、三菱重工等研究课题10余项。

报告题目：车控软件栈安全测试

报告摘要：随着车联网及自动驾驶等技术的高速发展，车辆控制软件的规模也日益庞大，测试分析的难度及对安全的要求也越来越大。上层应用，协议到底层的内核等，微小的漏洞，都可能被触发利用引发严重的后果。所以，针对车控软件的安全保障至关重要。本报告针对DDS库，RTPS协议，RTOS内核等典型车控软件的模糊测试展开，提出基于智能动态调度的应用库模糊测试、跨状态覆盖搜索的协议模糊测试和任务感知学习的内核模糊测试，提升车控软件栈的整体安全测试效果。

殷永峰

北京航空航天大学软件学院 副院长

北京航空航天大学软件学院副院长，副教授/博士生导师，航空工业软件测评中心主任（2013.4-2021.3）。国家公派赴美访问学者。担任某预警机副总师、军兵种软件专家组成员、航空工业集团软件质量专家组成员等。研究方向：软件工程、软件可靠性安全性、嵌入式软件验证。截止目前，发表学术论文60余篇，获省部级一等奖、二等奖各2项、航空工业个人三等功1项，出版专著3部，技术发明专利22项。服务国家战略，主持完成40多个重点型号、累计合同额近3亿元的软件试验鉴定工作，为提高装备质量和可靠性做出重大贡献，获得军方和工业部门的高度评价。

报告题目：机载软件自动化测试技术及其应用

报告摘要：软件测试作为保证系统质量与可靠性的重要手段，已得到充分推广与应用。然而，随着航空机载系统软件重要度与复杂度的提升，机载软件测试技术领域的问题也逐渐凸显。如何有效地开展机载软件自动化测试工作，确保测试的充分性和效率，已成为制约机载软件质量保证工作的关键因素之一。报告针对先进航空装备领域软件自动化验证需求，提出并突破航空机载系统软件建模技术、基于测试模型的用例自动生成及优化技术、机载软件测试用例描述及自动执行等关键技术，开发了系统化的自动化测试环境，形成了一套适用于新一代装备软件自动化测试的完整解决方案，并获得成功工程应用验证，效果显著。

张维

中兴通讯股份有限公司 无线安全实验室 形式化验证工程师

目前在无线安全实验室，主要从事产品关键特性方案的形式化验证相关工作，主要掌握web、主机、数据库渗透测试及TLA+形式化验证技术，持有CISP-PTE证书。

报告题目：基于TLA+的形式化验证方法在ZTE的实践与应用

报告摘要：主要介绍中兴通讯应用形式化验证方法TLA+的实践经验，包括研究成果总览、部分案例分享、推广落地工作、经验与方法总结等内容，旨在通过分享中兴通讯在使用TLA+对复杂程序设计、形式化模型检测理论方面的研究与工程实践探索，进一步深化对形式化验证方法的应用，更加全面系统的开展实践。