望安科技赵永望教授参加CNCC技术论坛，并作《安全攸关操作系统形式化验证》主题演讲

10月22日-24日，为期3天的2020CNCC计算机领域的年度盛会在北京举办。

本次领域盛会汇聚了图灵奖获得者、两院院士、国内外顶尖学者、知名企业家等亲临大会，展望前沿趋势，分享创新成果。

望安科技创始人赵永望教授参加“安全攸关系统形式化方法应用实践”论坛并作主题演讲。

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

本论坛中，浙江望安科技有限公司创始人、浙江大学教授、博导赵永望作了《安全攸关操作系统形式化验证：技术与应用实践》的主题演讲。

赵教授根据本领域和方向的趋势，通俗易懂、简练地解释了操作系统形式化验证的背景意义、国内外现状和面临的挑战，介绍团队提出的系统方法、理论技术以及真实应用实践。

赵教授提出，目前，安全攸关操作系统主要应用于航空、航天、轨道交通、无人系统等领域，它位于计算机系统软件栈的底层，操作系统的错误可能导致系统崩溃、被攻击、时间不确定性等问题，涉及功能安全、信息安全等问题。操作系统功能结构复杂，多核多任务的并发度高，开发与调试都十分困难，一些隐藏的错误用常见的软件测试技术难以发现，而形式化验证可帮助软件开发人员发现深层的错误，确保操作系统的高安全可靠性。

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