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