智能化軟件分析原理課程設(shè)計(jì)初探

陳振邦，陳立前，王 戟

（國(guó)防科技大學(xué)計(jì)算機(jī)學(xué)院，湖南長(zhǎng)沙 410073）

0 引言

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

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

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

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

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

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

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

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

3 教學(xué)改革情況

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

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

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

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

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

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

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

3.2 改革舉措與初步成效

3.2.1 改革舉措

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

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

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

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

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

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

3.2.2 初步效果

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

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

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

4 結(jié)語(yǔ)

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