智能化軟件分析原理課程設計初探

陳振邦，陳立前，王 戟

（國防科技大學計算機學院，湖南長沙 410073）

0 引言

隨著信息技術的發(fā)展，軟件作為現(xiàn)代社會的基礎設施之一，已經滲透到人們生活的方方面面。然而，隨著軟件產業(yè)及其規(guī)模的不斷擴大，軟件的復雜性日益增加，安全問題也日益凸顯。在國家現(xiàn)代化發(fā)展進程中，軟件作為信息化的核心與靈魂發(fā)揮著關鍵作用。但由于軟件作為智力產品具有極高的復雜性，開發(fā)出滿足質量要求的軟件非常困難，屢屢出現(xiàn)的軟件問題已經造成重大經濟損失，給國家安全也產生了極大影響。如何保證軟件質量是國內外工業(yè)界和學術界共同關注的重大前沿問題［1］。

隨著軍隊信息化程度的不斷提高，軍用軟件已經滲透到軍事應用的各個方面，成為武器裝備體系中不可或缺的組成部分［2］。目前，軍用軟件的自主可控需求不斷增強，如何在軟件開發(fā)及運行過程中提高其安全性成為非常重要且急迫的問題。此外，隨著人工智能、大數(shù)據(jù)、物聯(lián)網技術的飛速發(fā)展，當前越來越多的軟件系統(tǒng)中包含人工智能構件，如深度神經網絡等。由于這些構件的天然不可解釋性，給軟件系統(tǒng)質量安全帶來了巨大挑戰(zhàn)，使軟件質量問題呈現(xiàn)出新的時代特點［3］。

國防科技大學軟件工程學科在高可信軟件、智能軟件方面有著非常突出的特點與優(yōu)勢，其中智能化軟件分析為核心研究方向之一，對軟件工程、信息安全、計算機科學與技術等學科起到了輻射支撐作用，也為保證超級計算機、系統(tǒng)軟件等研發(fā)質量發(fā)揮了重要作用。為進一步發(fā)展核心研究方向，為國家和軍隊的關鍵科研任務及人才培養(yǎng)作出更大貢獻，本文針對智能化軟件分析方向的人才培養(yǎng)要求，開展智能化軟件分析原理課程設計研究。

1 智能化軟件分析人才培養(yǎng)的重要性

軟件分析活動在軟件生命周期中廣泛存在。軟件分析是指對軟件進行人工或自動分析，以驗證、確認或發(fā)現(xiàn)軟件的某種性質或規(guī)約［4］。由于軟件是機器智能的重要體現(xiàn)，而自動化軟件分析的本質是設計一個軟件系統(tǒng)分析和理解另外一個軟件系統(tǒng)，因此本文將自動化軟件分析稱為智能化軟件分析。智能化軟件分析技術是提升軟件安全性與可靠性的有效手段，同時也是軟件自主可控的關鍵支撐技術之一。

為適應時代需求，為軍用軟件自主可控研究培養(yǎng)高級人才，同時滿足地方對高級軟件工程人才、高級安全人才的需求，亟需培養(yǎng)智能化軟件分析方面的人才。該類人才需要對智能化軟件分析的基礎理論具有深刻理解，同時具備在不同問題場景下設計開發(fā)相應智能化軟件分析或理解工具的能力。

2 國內外一流大學相關教學情況

智能化軟件分析的基礎理論、技術和工具實現(xiàn)的準入門檻相對較高，主要是歐美一些世界一流高校的計算機相關專業(yè)開設了相關課程。近年來，國內的北京大學和南京大學也開設了相關課程。教學團隊系統(tǒng)調研了國內外多所一流大學，包括美國的卡內基梅隆大學、麻省理工大學、斯坦福大學、加州大學伯克利分校、華盛頓大學、北京大學和南京大學在智能化軟件分析相關課程建設方面的工作，結果見表1。其中教材PPA 是指Flemming 等編寫的Principles of Program Analysis［5］；TAPL 指Benjamin 編寫的Types and Programming Languages［6］；FSPL 指Glynn 編寫的The Formal Semantics of Programming Language：An Introduction［7］；PMC 指Christel 等編寫的Principles of Model Checking［8］；CPTT 指Alfred 等編寫的Compilers：Principles，Techniques，and Tools［9］；LNSA 指Michael 編寫的Lecture Notes on Static Analysis［10］；SPA 指Anders 等編寫 的Static Program Analysis［11］?？梢钥闯?，國內外一流大學相關課程的基礎性、實踐性和前沿性均非常突出，注重學生對分析工具構建能力的培養(yǎng)，因此很多課程都設置了分數(shù)占比較高的實驗。此外，通過調研發(fā)現(xiàn)，上述開設智能化軟件分析相關課程的學校在智能化軟件分析支撐理論和技術方面都有非常扎實的積累以及突出的特點和優(yōu)勢。

3 教學改革情況

國防科技大學在智能化軟件分析方向具備很好的研究和人才培養(yǎng)基礎，在軟件工程專業(yè)研究生培養(yǎng)方面開設了《數(shù)理邏輯》和《形式化方法》等相關基礎核心課程。課程教師在智能化軟件分析的基礎理論、方法和技術研究以及工具開發(fā)方面具備較好的基礎，近年來多項研究成果發(fā)表在軟件工程和程序設計語言的頂級會議上，在學術的前沿性和國際國內學術影響方面具有良好基礎，具備了開設智能化軟件分析課程的條件。

目前，國防科技大學軟件工程方向研究生培養(yǎng)方案中雖然已經存在與智能化軟件分析技術相關的一些課程，包括高級編譯技術、高可信軟件技術、智能軟件工程、人工智能、機器學習等，但尚不能完全涵蓋智能化軟件分析的基礎理論和方法。同時，由于課時原因，核心技術的講授深度也不夠。此外，實踐環(huán)節(jié)對于智能化軟件分析人才培養(yǎng)非常關鍵，在系統(tǒng)講授分析原理的基礎上，配套較為深入和全面的實踐環(huán)節(jié)才能達到深入理解和系統(tǒng)掌握的教學目標。因此，在新一輪研究生培養(yǎng)方案的修訂過程中，對軟件工程方向的研究生課程進行整合，新增智能化軟件分析原理這門專業(yè)基礎課程，用于支撐智能化軟件分析相關方向（軟件工程、信息安全、系統(tǒng)軟件等）的研究生培養(yǎng)。

3.1 課程內容設計

本課程面向計算機相關專業(yè)的研究生，通過對軟件分析的背景、關鍵理論和技術以及主流工具分別進行講授、實踐和研討，對目前存在的一些開放性問題進行探索，使學生理解提高軟件質量的重要性和緊迫性，了解并掌握軟件分析的基礎理論、主要方法、技術和工具，為軟件工程、計算機安全、系統(tǒng)軟件等方向的研究生進一步進行相關領域的學習和研究建立良好基礎。

通過廣泛調研國內外最新的軟件分析系列課程，面向軟件安全和自主可控，結合國防科技大學計算機學院學科特點，梳理了智能化軟件分析的核心概念與內涵，設計了教學內容與實驗體系，以支持研究生系統(tǒng)掌握軟件分析的基礎原理、核心技術及工具的開發(fā)與使用。在研究系統(tǒng)化、結構化課程內容及驗證性實驗環(huán)節(jié)的基礎上，進一步拓展綜合性、設計性和自主性實驗內容。

圖1 給出了課程內容的層次化組織結構。課程內容從基礎理論、關鍵技術、典型應用3 個層面展開。在基礎理論層面介紹命題邏輯、一階邏輯核心以及相應的判定理論和方法（SAT/SMT）、抽象解釋理論、霍爾邏輯3 方面內容；在關鍵技術層面介紹符號執(zhí)行、數(shù)據(jù)流分析、演繹驗證3 方面內容；在典型應用層面介紹相關理論和技術在軟件自動測試、軟件缺陷自動檢測、程序驗證等中的幾個典型應用。同時，以信息安全、軟件測試與驗證為背景，安排了自動測試用例生成、污點分析、自動驗證3 個典型應用實驗，以有效提升學生對課程內容的理解并增強其實踐能力。課程推薦的外文教材包括Decision Procedures：An Algorithmic Point of View［12］、Principles of Program Analysis、Static Program Analysis、The Calculus of Computation：Decision Procedures with Applications to Verification［13］，均為目前國際上相關課程推薦較多的教材，基本覆蓋了課程的教學內容。

Table 1 Construction of intelligent software analysis related courses in first-class universities at home and abroad表1 國內外一流大學智能化軟件分析相關課程建設情況

3.2 改革舉措與初步成效

3.2.1 改革舉措

目前，國防科技大學計算機學院相關專業(yè)研究生課程的理論部分以課堂講授為主，實踐和實驗部分由學生課后完成，存在生源背景差異較大、偏理論課程講授難度大、課程考核方式不合理和針對性不強等問題。為提升教學質量，采取以下幾個方面的改革措施：

（1）針對學校研究生生源背景差異較大的問題，采取基于閉環(huán)的教學全過程管理和監(jiān)控。通過問卷調查等手段掌握學生的知識背景，對智能化軟件分析課程內容的滿意程度以及對課程的期望，將學員意見匯總納入課程內容及實驗體系的設計考慮范疇。

Fig.1 Hierarchical organizational structure of course content圖1 課程內容層次化組織結構

（2）針對理論課程授課難度大的問題，在課程中使用研究工作中經常接觸到的案例開展教學［14］，例如結合人工智能系統(tǒng)的可解釋性和可信保障問題介紹軟件驗證相關技術，結合航空航天軟件的問題案例介紹浮點程序的分析問題，結合安全漏洞介紹數(shù)組和動態(tài)數(shù)據(jù)結構程序的分析問題，結合軟件配置管理介紹SAT 中的MaxSAT 問題等［15-17］，使學生在學習理論知識的同時增強對知識應用場景的理解和認識。此外，由于課程內容門檻相對較高，學生對課程知識的理解、掌握與運用之間存在鴻溝。因此，在關鍵知識點講授過程中采取課堂講授加測試的方式，即在講完后馬上開展隨堂測試，以促進學生課前預習以及課上認真聽講，方便教師及時掌握學生的薄弱知識點。同時通過開展頗具難度的代表性實驗，提升學生對知識的運用能力。

（3）在課程考核方面采取基于實驗的考核方式，實驗得分占最終分數(shù)的60%?；陂_源資源設計組織課程實驗，同時鼓勵學生根據(jù)自己的專業(yè)方向設計開發(fā)創(chuàng)新性實驗項目。目前，課程以LLVM 開源編譯框架為基礎，結合Z3 求解器，為學生提供了3 個應用實驗項目，包括基于數(shù)據(jù)流分析的污點分析實驗（實驗1）、基于符號執(zhí)行技術的程序自動測試實驗（實驗2）以及基于Z3 的程序驗證工具實驗（實驗3），具體實驗過程中還涉及到程序插樁、Horn子句、污點傳播等知識背景。實驗分組要求不超過3 人，實驗總體分數(shù)會根據(jù)平均實驗工作量以及實驗完成度評價，個人分數(shù)則根據(jù)組內工作量評價。

（4）由于課程內容的前沿性較強，以頂會論文報告的形式引導學生了解國際前沿，提升其撰寫閱讀報告以及進行課堂論文報告的能力。具體形式是要求學生在其研究方向的頂級會議中選取最近3 年與課程內容密切相關的論文，撰寫閱讀報告并在課堂上進行匯報。閱讀報告和課堂報告的分數(shù)各占課程總分的20%，具體根據(jù)閱讀報告質量以及課堂匯報的效果進行評價。

3.2.2 初步效果

在開設智能化軟件分析原理課程的第一年（2020 年），共有26 位學生（涉及計算機科學與技術、軟件工程、信息安全等方向）選修，將其分為13 組。圖2 給出了學生的分數(shù)分布情況，可以看出所有學生都通過了課程考核，平均成績?yōu)?1.2 分。圖3 給出了實驗成績統(tǒng)計情況，最終實驗1 有11 組完成，實驗2 有4 組完成，實驗3 有1 組完成，實驗綜合得分最高90分，最低70分。

Fig.2 Course score distribution圖2 課程分數(shù)分布

Fig.3 Experiment score distribution圖3 課程實驗分數(shù)分布

4 結語

針對智能化軟件分析方面的人才培養(yǎng)需求，系統(tǒng)調研了國內外一流大學相關課程的開設情況，并在國防科技大學計算機學院開設課程的基礎上進行了初步改革探索和嘗試，設計了基于基礎理論、核心技術和典型應用三層結構的課程內容，同時開展了工業(yè)級開源環(huán)境下的課程實驗，在智能化軟件分析方向的研究生人才培養(yǎng)方面取得了初步成果。后續(xù)將從以下幾個方面深入課程改革：①探索基于優(yōu)質網絡資源的課程內容設計和教學組織方式，利用優(yōu)質網絡文本、視頻資源開展基于自主學習的課程教學方法；②探索兼顧實際科研需求和國際發(fā)展前沿的課程內容設計，保持課程內容、實驗項目與時俱進，并嘗試開發(fā)自主實驗平臺；③在課程內容上考慮涵蓋動態(tài)分析、指針分析、模型檢驗部分等知識點，同時考慮到該課程的前沿性與創(chuàng)新性，逐步開展中文教材編寫工作。