望安科技出席2025 CCF中国软件大会，共话形式化验证与原生安全

2025年11月28日—11月30日，2025 CCF 中国软件大会在湖北省武汉国际会议中心圆满举办。本届大会以“软件定义智能互联新世界”为主题，全面展示我国软件创新领域的前沿研究、先进工具链与产业实践。大会邀请了12位中国科学院与中国工程院院士作特邀报告，并举办院士高峰论坛，同时组织了75个分论坛和活动，覆盖软件工程、系统软件、形式化方法、工业场景落地及人才培养等多个关键领域。作为深度参与者，浙江望安科技有限公司在大会期间发布四场论坛报告，展示了其在“原生安全”和“形式化验证”领域的最新研究成果和典型应用案例。

在形式化验证和原生安全方向，望安科技作为国内较早布局相关技术的创新企业，在本届大会中通过四场论坛报告集中展示其研发进展、工具链体系与实际工程经验，使更多行业参与者了解形式化验证如何服务于基础软件可信、安全内核构建以及关键系统的开发。

望安科技创始人、浙江大学博士生导师赵永望教授作《AI赋能的形式化验证技术探索》报告。赵永望教授指出，AI/LLM 技术为形式化验证应用带来了新的机遇，并在报告中系统阐述了 AI 赋能形式化验证的核心思路，同时分析其关键技术瓶颈与未来发展方向。

在另一场报告中，赵永望教授作《操作系统形式化验证：现状与挑战》报告。操作系统的任何错误都可能引发系统崩溃或被攻击，影响整体安全与可靠性。传统“事后补丁式”安全方案往往治标不治本，无法避免缺陷反复出现。基于原生安全理念，操作系统需要从架构设计开始就建立可信基础，而形式化验证正是实现这一目标的关键技术。通过数学化的规约描述与严格证明，可在开发早期发现深层逻辑漏洞，确保系统调用、调度机制、权限管理等模块符合预设安全与功能要求。报告对国内外研究现状、关键技术难点以及工程化挑战做出了系统分析，为未来发展提供了方向。

望安科技形式化验证工程师王布阳作《基于Auto-active与交互式集成的L4线程管理形式化验证》报告。报告分享了团队通过围绕 L4 微内核的关键机制——线程管理，开展了系统的形式化规约与验证研究。在验证过程中，团队将交互式验证与 Auto-active 方法结合，不仅提高了验证自动化水平，还有效降低了人工证明工作量。

望安科技技术副总裁张峰作《以形式化方法构建基础软件原生安全》报告。原生安全不是传统安全加固的延伸，而是从产品规划、需求设计、架构建模到开发验证的全生命周期安全体系。其核心是以形式化方法为支撑，通过抽象建模、符号分析、自动化证明等手段验证关键模块的设计正确性，实现安全需求、设计逻辑与系统行为的严格一致。张峰详细展示了望安科技如何通过形式化验证技术和“穹道”原生安全平台作用于内核、系统调用、调度器、内存管理和关键库函数，帮助企业从根本上消除深层设计缺陷，保障产品长期业务价值，真正构建“先天可信、内生安全”的基础软件。

2025 CCF 中国软件大会的成功举办为行业提供了思想交流与技术前瞻的平台。作为赞助单位和深度参与者，望安科技不仅展示了技术实力，也推动了形式化验证、原生安全等领域的学术交流与产业合作。多位与会专家认为，形式化验证正在从学术工具走向工程体系，而“原生安全”正成为基础软件建设的重要趋势。望安科技在本届大会上集中展示的实践案例，为行业提供了可参考的工程路径，也推动相关技术在更多场景中的应用讨论。