陳振邦，陳立前，王 戟

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

0 引言

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

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

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

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

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

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

2 國內(nèi)外一流大學(xué)相關(guān)教學(xué)情況

智能化軟件分析的基礎(chǔ)理論、技術(shù)和工具實現(xiàn)的準(zhǔn)入門檻相對較高，主要是歐美一些世界一流高校的計算機相關(guān)專業(yè)開設(shè)了相關(guān)課程。近年來，國內(nèi)的北京大學(xué)和南京大學(xué)也開設(shè)了相關(guān)課程。教學(xué)團(tuán)隊系統(tǒng)調(diào)研了國內(nèi)外多所一流大學(xué)，包括美國的卡內(nèi)基梅隆大學(xué)、麻省理工大學(xué)、斯坦福大學(xué)、加州大學(xué)伯克利分校、華盛頓大學(xué)、北京大學(xué)和南京大學(xué)在智能化軟件分析相關(guān)課程建設(shè)方面的工作，結(jié)果見表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］?？梢钥闯?，國內(nèi)外一流大學(xué)相關(guān)課程的基礎(chǔ)性、實踐性和前沿性均非常突出，注重學(xué)生對分析工具構(gòu)建能力的培養(yǎng)，因此很多課程都設(shè)置了分?jǐn)?shù)占比較高的實驗。此外，通過調(diào)研發(fā)現(xiàn)，上述開設(shè)智能化軟件分析相關(guān)課程的學(xué)校在智能化軟件分析支撐理論和技術(shù)方面都有非常扎實的積累以及突出的特點和優(yōu)勢。

3 教學(xué)改革情況

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

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

3.1 課程內(nèi)容設(shè)計

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

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

圖1 給出了課程內(nèi)容的層次化組織結(jié)構(gòu)。課程內(nèi)容從基礎(chǔ)理論、關(guān)鍵技術(shù)、典型應(yīng)用3 個層面展開。在基礎(chǔ)理論層面介紹命題邏輯、一階邏輯核心以及相應(yīng)的判定理論和方法（SAT/SMT）、抽象解釋理論、霍爾邏輯3 方面內(nèi)容；在關(guān)鍵技術(shù)層面介紹符號執(zhí)行、數(shù)據(jù)流分析、演繹驗證3 方面內(nèi)容；在典型應(yīng)用層面介紹相關(guān)理論和技術(shù)在軟件自動測試、軟件缺陷自動檢測、程序驗證等中的幾個典型應(yīng)用。同時，以信息安全、軟件測試與驗證為背景，安排了自動測試用例生成、污點分析、自動驗證3 個典型應(yīng)用實驗，以有效提升學(xué)生對課程內(nèi)容的理解并增強其實踐能力。課程推薦的外文教材包括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］，均為目前國際上相關(guān)課程推薦較多的教材，基本覆蓋了課程的教學(xué)內(nèi)容。

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

3.2 改革舉措與初步成效

3.2.1 改革舉措

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

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

Fig.1 Hierarchical organizational structure of course content圖1 課程內(nèi)容層次化組織結(jié)構(gòu)

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

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

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

3.2.2 初步效果

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

Fig.2 Course score distribution圖2 課程分?jǐn)?shù)分布

Fig.3 Experiment score distribution圖3 課程實驗分?jǐn)?shù)分布

4 結(jié)語

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