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