學術活動
信息工程學院講座-CCF形式化專委走進首都師范大學
2025-04-16
點擊次數：時間：2025年4月16日 下午1:30
地點：首師大校本部電教樓三層國際報告廳
主講人：1. 孫猛，北京大學數學科學學院教授，博導
2. 蔡少偉，中國科學院軟件研究所研究員，博導
3. 時清凱，南京大學計算機學院副教授，博導
主持人：王瑞，首都師范大學信息工程學院教授
主講人簡介：
1. 孫猛，北京大學數學科學學院信息與計算科學系教授，博士生導師， CCF形式化方法專委執行委員，CCF區塊鏈專委執行委員，CSIAM區塊鏈專委常務委員，CSIAM金融科技與算法專委常務委員，CAAI人工智能邏輯專委委員。主要研究領域包括程序理論、軟件形式化方法、信息物理系統、深度學習、區塊鏈與智能合約，主持及作為主要成員參與國家自然科學基金、重點研發計劃等國家及省部級項目十余項，在TSE、TDSC、ICSE、FSE、FM 、NeurIPS、AAAI等期刊及會議發表論文百余篇，獲TASE2015、SBMF2017等國際會議最佳論文獎，曾任ICFEM(2024、2018)、TASE(2023)、FACS(2009、2024)等國際會議程序委員會主席及FM、TACAS等多個國際會議程序委員會委員。
2. 蔡少偉，中國科學院軟件研究所研究員，博導，中國科學院優秀導師，CCF杰出會員和杰出演講者，智源青年科學家，承擔多個國家項目和課題，多次獲得約束求解領域國際比賽冠軍，在領域頂級會議SAT、CP、CAV等獲得最佳論文獎/杰出論文獎。成果應用于華為的EDA和操作系統項目，以及多家EDA企業，香山處理器緩存驗證，微軟云平臺故障檢測，以及多家互聯網頭部企業。帶領團隊研發了首個基于大模型技術的SAT求解器。
3. 時清凱，南京大學計算機學院副教授，博士生導師，國家級高層次青年人才，2020 年于香港科技大學獲得博士學位，曾任源傘科技聯合創始人、螞蟻集團技術專家、美國普渡大學博士后研究員。目前主要從事軟件分析及軟件安全技術研究，其研究成果廣泛發表于程序語言（如PLDI，OOPSLA）、軟件工程（如ICSE，ESEC/FSE）、網絡安全（如SP，CCS）等CCF A 類會議或期刊，曾獲ACM SIGSOFT 杰出論文獎、ACM SIGPLAN 杰出論文獎、Google 論文獎、Hong Kong PhD Fellowship。其研究成果廣泛應用于諸如阿里、華為等高新技術企業，已幫助企業識別數百個高危漏洞。
主講內容簡介：
1. 報告題目：基于統計模型檢查的深度神經網絡魯棒性估計
摘要：以深度神經網絡為代表的深度學習系統已在自動駕駛、醫療診斷等安全攸關領域得到了廣泛應用。與傳統軟件系統不同，其數據驅動的特點使得該類系統擁有與傳統系統完全不同的決策邏輯，并且深度學習系統的高維輸入、龐大參數規模和狀態空間使得其復雜程度遠遠超過傳統的軟件系統，從而使得目前應用于傳統軟件系統的形式化技術難以直接應用于大規模深度學習系統的安全性、魯棒性保障之中。本次報告中將介紹我們近期關于統計模型檢查算法改進和深度神經網絡魯棒性估計的部分工作結果。我們對主流統計模型檢查工具中使用的Okamoto bound估計方法進行了改進，設計了新的統計模型檢查算法，大幅減少了采樣次數，可比現有統計模型檢查算法節省40%-60%的時間。從統計模型檢查的角度，我們給出了深度神經網絡魯棒性的估計算法，僅用少量圖片即可獲得與傳統方法使用大量圖片計算得到的全局魯棒性值強相關的結果。
2. 報告題目：約束求解與EDA形式化驗證
摘要：“約束求解”一般是指一種方法論，強調對問題通過某種數學語言進行形式化表達，然后對其進行求解，是計算機解決問題的一種常見方法論。約束求解器，特別是邏輯公式可滿足性問題的求解器，包括SAT求解器和SMT求解器，是軟硬件驗證與測試的基礎引擎。約束求解器的性能是許多形式化驗證工具性能的關鍵因素。本報告首先介紹SAT問題和SMT問題的基礎內容，然后介紹約束求解的前沿技術，最后介紹相關的EDA形式化驗證技術與應用。
3. 報告題目：網絡協議安全分析中的形式化方法
摘要：網絡協議定義計算機系統如何相互連接，是“人機物”融合時代保障“人機物”互融互通的關鍵組件，因此，網絡協議漏洞可能造成災難性嚴重后果。網絡協議的形式化規約是各種自動化網絡安全分析（如模糊測試、網絡監聽、模型檢測等）的基礎，因此格外重要。該報告將介紹網絡協議形式化規約推導、生成技術以及其中所包含的形式化方法，其主要思路為通過靜態程序分析乃至大語言模型等手段，分析網絡協議的實現或文檔，構建包含精確語法結構和語義的網絡協議規約，并使用構建的精確規約指導下游網絡安全分析。截止目前，該工作已找到50余個網絡協議中的嚴重漏洞，包括緩沖區溢出、整數溢出等，并獲得10余個CVE編號。
