2025年11月28日—11月30日，2025 CCF 中國軟件大會在湖北省武漢國際會議中心圓滿舉辦。本屆大會以“軟件定義智能互聯(lián)新世界”為主題，全面展示我國軟件創(chuàng)新領域的前沿研究、先進工具鏈與產(chǎn)業(yè)實踐。大會邀請了12位中國科學院與中國工程院院士作特邀報告，并舉辦院士高峰論壇，同時組織了75個分論壇和活動，覆蓋軟件工程、系統(tǒng)軟件、形式化方法、工業(yè)場景落地及人才培養(yǎng)等多個關鍵領域。作為深度參與者，浙江望安科技有限公司在大會期間發(fā)布四場論壇報告，展示了其在“原生安全”和“形式化驗證”領域的最新研究成果和典型應用案例。
在形式化驗證和原生安全方向，望安科技作為國內(nèi)較早布局相關技術的創(chuàng)新企業(yè)，在本屆大會中通過四場論壇報告集中展示其研發(fā)進展、工具鏈體系與實際工程經(jīng)驗，使更多行業(yè)參與者了解形式化驗證如何服務于基礎軟件可信、安全內(nèi)核構(gòu)建以及關鍵系統(tǒng)的開發(fā)。
望安科技創(chuàng)始人、浙江大學博士生導師趙永望教授作《AI賦能的形式化驗證技術探索》報告。趙永望教授指出，AI/LLM 技術為形式化驗證應用帶來了新的機遇，并在報告中系統(tǒng)闡述了 AI 賦能形式化驗證的核心思路，同時分析其關鍵技術瓶頸與未來發(fā)展方向。
在另一場報告中，趙永望教授作《操作系統(tǒng)形式化驗證：現(xiàn)狀與挑戰(zhàn)》報告。操作系統(tǒng)的任何錯誤都可能引發(fā)系統(tǒng)崩潰或被攻擊，影響整體安全與可靠性。傳統(tǒng)“事后補丁式”安全方案往往治標不治本，無法避免缺陷反復出現(xiàn)。基于原生安全理念，操作系統(tǒng)需要從架構(gòu)設計開始就建立可信基礎，而形式化驗證正是實現(xiàn)這一目標的關鍵技術。通過數(shù)學化的規(guī)約描述與嚴格證明，可在開發(fā)早期發(fā)現(xiàn)深層邏輯漏洞，確保系統(tǒng)調(diào)用、調(diào)度機制、權(quán)限管理等模塊符合預設安全與功能要求。報告對國內(nèi)外研究現(xiàn)狀、關鍵技術難點以及工程化挑戰(zhàn)做出了系統(tǒng)分析，為未來發(fā)展提供了方向。
望安科技形式化驗證工程師王布陽作《基于Auto-active與交互式集成的L4線程管理形式化驗證》報告。報告分享了團隊通過圍繞 L4 微內(nèi)核的關鍵機制——線程管理，開展了系統(tǒng)的形式化規(guī)約與驗證研究。在驗證過程中，團隊將交互式驗證與 Auto-active 方法結(jié)合，不僅提高了驗證自動化水平，還有效降低了人工證明工作量。
望安科技技術副總裁張峰作《以形式化方法構(gòu)建基礎軟件原生安全》報告。原生安全不是傳統(tǒng)安全加固的延伸，而是從產(chǎn)品規(guī)劃、需求設計、架構(gòu)建模到開發(fā)驗證的全生命周期安全體系。其核心是以形式化方法為支撐，通過抽象建模、符號分析、自動化證明等手段驗證關鍵模塊的設計正確性，實現(xiàn)安全需求、設計邏輯與系統(tǒng)行為的嚴格一致。張峰詳細展示了望安科技如何通過形式化驗證技術和“穹道”原生安全平臺作用于內(nèi)核、系統(tǒng)調(diào)用、調(diào)度器、內(nèi)存管理和關鍵庫函數(shù)，幫助企業(yè)從根本上消除深層設計缺陷，保障產(chǎn)品長期業(yè)務價值，真正構(gòu)建“先天可信、內(nèi)生安全”的基礎軟件。
2025 CCF 中國軟件大會的成功舉辦為行業(yè)提供了思想交流與技術前瞻的平臺。作為贊助單位和深度參與者，望安科技不僅展示了技術實力，也推動了形式化驗證、原生安全等領域的學術交流與產(chǎn)業(yè)合作。多位與會專家認為，形式化驗證正在從學術工具走向工程體系，而“原生安全”正成為基礎軟件建設的重要趨勢。望安科技在本屆大會上集中展示的實踐案例，為行業(yè)提供了可參考的工程路徑，也推動相關技術在更多場景中的應用討論。
申請創(chuàng)業(yè)報道，分享創(chuàng)業(yè)好點子。點擊此處，共同探討創(chuàng)業(yè)新機遇！
