主題：程序分析與軟件測試前沿

活動時間:2022年6月19日（周日）19:30-21:30

活動地址:會議號713-683-437 （密碼：14210）

主講人:熊英飛、文明、李樾

主辦方:必贏3003no1線路檢測中心必贏3003no1線路檢測中心

報告人1：熊英飛

報告題目：《從參數(shù)化到概率化——北京大學(xué)在程序調(diào)試上的近期工作介紹》

報告簡介：

過去20年，數(shù)據(jù)驅(qū)動的軟件工程技術(shù)獲得很大發(fā)展，多個不同領(lǐng)域的技術(shù)都在大數(shù)據(jù)的幫助下獲得顯著提高。不過，現(xiàn)有大部分數(shù)據(jù)驅(qū)動的工作都是參數(shù)化的，即在大數(shù)據(jù)的幫助下對一些未知參數(shù)進行調(diào)參，而這些參數(shù)本身可能沒有概率論上的解釋。但如果我們從一開始就試圖建立概率模型，那么我們就可以利用概率論的規(guī)則和程序相關(guān)的語法、語義等信息進行推導(dǎo)，既能夠更有效地從數(shù)據(jù)中學(xué)習(xí)，也可以幫我們做出一些概率上最優(yōu)的決策。本次分享將介紹北京大學(xué)團隊沿著這個思路在調(diào)試上的部分工作，包括一個新的差異化調(diào)試算法（發(fā)表于FSE21，被評為ACM SIGSOFT杰出論文）和一個基于程序語義的錯誤定位工作（錄用與ICSE22）。

報告人簡介：

熊英飛于2009年從日本東京大學(xué)獲得博士學(xué)位，2009-2011年在加拿大滑鐵盧大學(xué)工作，2012年加入北京大學(xué)，現(xiàn)任新體制長聘副教授。熊英飛的研究興趣是程序設(shè)計語言和軟件工程，特別是程序合成、修復(fù)和分析。他提出了理論和方法降低程序編寫和缺陷修復(fù)的代價。比如，基于差別的雙向變換框架是最廣泛使用的雙向變換框架之一，概率和邏輯結(jié)合的程序合成框架玲瓏框架將程序修復(fù)的正確率從此前不到40%提升到80%以上。他的工作也被工業(yè)界采用，比如新一代Linux內(nèi)核配置項目、燕云DaaS系統(tǒng)、華為公司等。他獲得CCF-IEEE CS青年科學(xué)家獎、MODELS十年最有影響力論文獎，5次獲得ACM SIGSOFT/IEEE TCSE杰出論文獎。他是SATE18的程序委員會聯(lián)合主席，也在ICSE、FSE、ASE、ISSTA等會議擔(dān)任PC。

報告人2：文明

報告題目：《程序補丁的正確性驗證與存在性測試》

報告簡介：

程序自動修復(fù)技術(shù)在過去的十年時間里吸引了來自工業(yè)界和學(xué)術(shù)界的大量關(guān)注。盡管基于搜索的，基于語義的以及基于學(xué)習(xí)的修復(fù)方法都展現(xiàn)了不錯的效果，并且工業(yè)界也開始逐漸部署相關(guān)的補丁推薦系統(tǒng)，已有技術(shù)都面臨一個共同的挑戰(zhàn)，即補丁的正確性驗證問題。由于缺乏完備的程序規(guī)范，基于已有測試套件來評估補丁正確性的方法往往會造成補丁過擬合問題。針對該問題，我們對已有最新的21種程序自動修復(fù)技術(shù)進行了系統(tǒng)調(diào)研與分析，剖析出了過擬合補丁形成的根源，并對比了已有補丁正確性驗證方法的有效性與局限性?；谠撗芯康陌l(fā)現(xiàn)，我們進一步提出了基于程序結(jié)構(gòu)的上下文感知的代碼變更表示學(xué)習(xí)方法來提升補丁正確性驗證的性能，其驗證準確率達到了92.9%。當正確的補丁被部署到目標系統(tǒng)中之后，由于開源生態(tài)系統(tǒng)的成熟以及第三方庫的廣泛使用，補丁的存在性檢驗變得至關(guān)重要，尤其是對于威脅等級高的缺陷或者漏洞。補丁的存在性檢驗是為了驗證已知缺陷或者漏洞的補丁代碼在目標軟件系統(tǒng)中是否存在。目標軟件可能是源代碼或者二進制，也有可能是被混淆或者優(yōu)化過后的程序。因此，存在性的判定并不是一項容易的任務(wù)。我們針對漏洞補丁的存在性測試開展了研究，抽取了基于程序路徑的細粒度語義特征，提升了已有方法抵抗代碼混淆和優(yōu)化的能力，并且其抵抗能力分別達到了92.9%和87.3%。

報告人簡介：文明，華中科技大學(xué)網(wǎng)絡(luò)空間安全學(xué)院副教授，碩士生/博士生導(dǎo)師。文明博士于2014年從浙江大學(xué)計算機科學(xué)與技術(shù)學(xué)院獲得本科學(xué)位，2019年6月在香港科技大學(xué)計算機科學(xué)與工程學(xué)院取得博士學(xué)位，師從張成志教授。2017年7月至2018年1月，在美國加州大學(xué)戴維斯分校蘇振東教授課題組擔(dān)任訪問學(xué)者。2019年6月至2019年11月，在香港科技大學(xué)全職任職博士后研究員。2019年12月，加入華中科技大學(xué)網(wǎng)絡(luò)空間安全學(xué)院，聘為副教授。文明博士的研究方向主要包括軟件安全，軟件測試與分析，以及軟件生態(tài)系統(tǒng)的安全分析等，在軟件工程領(lǐng)域累計發(fā)表了CCF-A類推薦會議或期刊20篇，其他高水平論文10余篇。常年擔(dān)任TSE，TOSEM，TDSC等國際期刊的審稿人，以及CCF-A/B類會議ASE 2021, ESEC/FSE 2022, SANER 2022, ISSRE 2022的程序委員會委員。文明博士于2021年入選第七屆中國科協(xié)青年人才托舉工程計劃。

報告人3：李樾

報告題目：《指針分析，敢不敢再準一點？》

報告簡介：

指針分析，又名指向分析、別名分析，為編譯優(yōu)化、程序安全分析等應(yīng)用提供關(guān)于程序的基礎(chǔ)控制流與數(shù)據(jù)流信息，它的精度將直接影響其下游應(yīng)用的精度（質(zhì)量）。針對Java程序，目前提升其精度的主流方法是上下文敏感技術(shù)，然而針對大型且復(fù)雜的程序，傳統(tǒng)上下文敏感指針分析很難在可接受的時間內(nèi)分析出結(jié)果。為了解決這一問題，一系列選擇性上下文敏感方法被提出并取得積極成果。在本報告中，針對如何為“難以分析”的Java程序取得高精度的指針分析結(jié)果這一問題，我們提出了Unity-Relay分析框架并實現(xiàn)了它 的一個實例分析工具Baton，通過對比已有最佳方法，Baton對所有評估的程序，在所有的精度指標上都取得最佳精度。在很多情況下，Baton提升精度的效果是非常顯著的，針對已有最好方法報出來的別名對數(shù)量（一種精度指標），Baton最高可以消除71%的誤報。

報告人簡介：

    李樾，南京大學(xué)計算機科學(xué)與技術(shù)系副教授，博士生導(dǎo)師，入選國家級青年人才計劃、南京大學(xué)登峰人才計劃，南京大學(xué)紫金學(xué)者。2016年博士畢業(yè)于澳大利亞新南威爾士大學(xué)， 之后先后在新南威爾士大學(xué)與丹麥奧胡斯大學(xué)從事博士后研究工作。 研究方向為程序設(shè)計語言與程序分析，在程序設(shè)計語言相關(guān)國際重要期刊與會議，TOPLAS、PLDI、OOPSLA、ECOOP等發(fā)表文章。 曾獲ECOOP 2016 杰出論文獎，CGO 2013最佳論文獎和ISSRE 2017最佳論文提名。曾擔(dān)任APLAS 2021、ISSTA 2022等會議程序委員會成員，TOPLAS、PACMPL(POPL) 等期刊審稿專家。