軟件學報最新期刊目錄

面向自動駕駛系統(tǒng)的場景建模及邊緣關鍵場景生成————作者：杜德慧;葉振;鄭成行;朱珍珍;李家蘊;

摘要：自動駕駛中極端的場景、無法預測的人類行為等長尾問題逐漸成為制約自動駕駛系統(tǒng)(autonomous driving system, ADS)發(fā)展的關鍵要素,因此有效地生成安全關鍵場景對于提高自動駕駛系統(tǒng)的安全性至關重要.現有的自動駕駛場景生成主要依賴于大量的路采數據,采用數據驅動式場景生成方法,并結合場景泛化技術生成相應的駕駛場景.該方法耗時耗力,成本高,而且難以有效生成邊緣場景.而模型驅動式場景建...

因果時空語義驅動的深度強化學習抽象建模方法————作者：田麗麗;杜德慧;聶基輝;陳逸康;李滎達;

摘要：隨著智能信息物理融合系統(tǒng)(intelligent cyber-physical system, ICPS)的快速發(fā)展,智能技術在感知、決策、規(guī)控等方面的應用日益廣泛.其中,深度強化學習因其在處理復雜的動態(tài)環(huán)境方面的高效性,已被廣泛用于ICPS的控制組件中.然而,由于運行環(huán)境的開放性和ICPS系統(tǒng)的復雜性,深度強化學習在學習過程中需要對復雜多變的狀態(tài)空間進行探索,這極易導致決策生成時效率低下和泛化性...

面向智能體路徑規(guī)劃算法的動態(tài)隨機測試方法————作者：張逍怡;李幸;劉洋;鄭征;孫昌愛;

摘要：智能體路徑規(guī)劃算法旨在規(guī)劃某個智能體的行為軌跡,使其在不碰到障礙物的情況下安全且高效地從起始點到達目標點.目前智能體路徑規(guī)劃算法已經被廣泛應用到各種重要的物理信息系統(tǒng)中,因此在實際投入使用前對算法進行測試,以評估其性能是否滿足需求就非常重要.然而,作為路徑規(guī)劃算法的輸入,任務空間中威脅障礙物的分布形式復雜且多樣.此外,路徑規(guī)劃算法在為每個測試用例規(guī)劃路徑時,通常需要較高的運行代價.為了提升路徑規(guī)劃...

基于下推自動機的同步數據流語言可信編譯————作者：于濤;王珊珊;徐芊卉;董曉晗;胡代金;羅杰;楊溢龍;呂江花;馬殿富;

摘要：同步數據流語言Lustre是安全關鍵系統(tǒng)開發(fā)中常用的開發(fā)語言,其現存的官方代碼生成器和SCADE的KCG代碼生成器既沒有經過形式化驗證,對用戶也處于黑盒狀態(tài).近年來,通過證明源代碼和目標代碼的等價性間接證明編譯器的正確性的翻譯確認方法被證明是成功的.基于下推自動機的編譯方法和基于語義一致性的驗證方法,提出Lustre語言可信編譯方法,能夠將Lustre語言轉換為C語言并進行形式化驗證以保證編譯的正...

基于函數間結構特征關聯(lián)的軟件漏洞檢測方法————作者：邱少健;程嘉濠;黃夢陽;黃瓊;

摘要：漏洞檢測是軟件系統(tǒng)安全領域的關鍵技術.近年來,深度學習憑借其代碼特征提取的卓越能力,在漏洞檢測領域取得了顯著進展.然而,當前基于深度學習的方法僅關注于代碼實例自身的獨立結構特征,而忽視了不同漏洞代碼間存在的結構特征相似關聯(lián),限制了漏洞檢測技術的性能.針對這一問題,提出了一種基于函數間結構特征關聯(lián)的軟件漏洞檢測方法 (vulnerability detection method based on c...

單球驅動平衡機器人運動學和動力學形式化驗證————作者：張善強;張景芝;施智平;王國輝;關永;

摘要：單球驅動平衡機器人是一種具有全向運動性的機器人,其靈活性能在狹小或復雜環(huán)境中得到充分體現,因此受到廣泛關注.在該型機器人運動學和動力學設計過程中,保證其模型的正確性至關重要.基于測試和仿真的傳統(tǒng)方法難以窮盡系統(tǒng)所有狀態(tài),因此可能無法捕捉到某些設計缺陷或潛在的安全風險.為確保單球驅動平衡機器人滿足安全攸關機器人的正確性、安全性驗證要求,在定理證明器HOL Light中,基于實分析庫、矩陣分析庫、機器...

面向函數內聯(lián)場景的二進制到源代碼函數相似性檢測方法————作者：賈昂;范銘;徐茜;晉武俠;王海軍;劉烴;

摘要：二進制到源代碼函數相似性檢測是軟件組成成分分析的基礎性工作之一.現有方法主要采用一對一的匹配策略,即使用單一的二進制函數和單一的源代碼函數進行比對.然而,由于函數內聯(lián)的存在,函數之間的映射關系實際上表現為一對多——單一的二進制函數能夠關聯(lián)至多個源代碼函數.這一差異導致現有方法在函數內聯(lián)場景下遭受了30%的性能損失.針對函數內聯(lián)場景下的二進制到源代碼函數匹配需求,提出了一種面向一對多匹配的二進制到源...

結合特征生成與重放的可擴展安全虹膜識別————作者：趙冬冬;宋寶剛;廖虎成;閆江;向劍文;

摘要：隨著信息技術的快速發(fā)展,安全認證技術成為個人隱私和數據安全的重要保障.其中,虹膜識別技術憑借其出色的準確性和穩(wěn)定性,被廣泛應用于系統(tǒng)訪問控制、醫(yī)療保健以及司法實踐等領域.然而用戶的虹膜特征數據泄露,就是永久性丟失,無法進行更改或者撤銷.因此,虹膜特征數據的隱私保護尤為重要.隨著神經網絡技術在圖像處理上體現的突出性能,基于神經網絡的安全虹膜識別方案被提出,在保護隱私數據的同時保持了識別系統(tǒng)的高性能....

分布式系統(tǒng)動態(tài)測試技術研究綜述————作者：陳元亮;馬福辰;周遠航;顏臻;姜宇;孫家廣;

摘要：分布式系統(tǒng)是當今計算生態(tài)系統(tǒng)的支柱,它使得現代計算更加強大、可靠和靈活,覆蓋了從云計算、大數據處理到物聯(lián)網等多個關鍵領域.然而,由于系統(tǒng)的復雜性,分布式系統(tǒng)在代碼實現過程中總是不可避免地引入一些代碼缺陷,從而對系統(tǒng)的可用性、魯棒性以及安全性造成巨大威脅.因此,分布式系統(tǒng)的測試以及缺陷挖掘工作十分重要.動態(tài)測試技術在系統(tǒng)運行中進行實時分析,以挖掘其缺陷,評估其行為和功能,被廣泛用于各種系統(tǒng)應用的缺陷...

面向Rust語言的形式化驗證方法研究綜述————作者：張卓若;常瑞;楊申毅;陳芳;

摘要：Rust作為一種新興的安全系統(tǒng)級編程語言,以其創(chuàng)新的所有權模型和借用檢查機制提供了內存安全和并發(fā)安全保證.盡管Rust的設計宗旨在于安全性,但現有研究揭示了其仍面臨諸多安全挑戰(zhàn).形式化驗證作為一種基于嚴格數學基礎的方法,為Rust安全性提升提供了強有力保障.通過構建精準清晰的語義模型,可以證明遵循Rust檢查規(guī)則的程序滿足安全性要求;借助Rust自動化驗證工具能夠幫助用戶確保其Rust程序的安全性...

基于混成自動機路徑過濾與動態(tài)選擇的CPS系統(tǒng)反例生成————作者：王佳宛;劉熹橦;卜磊;李宣東;

摘要：信息物理融合系統(tǒng)(cyber-physical system, CPS)在安全攸關領域具有廣泛的應用,保障其安全性至關重要.形式化驗證是證明系統(tǒng)安全性的有效手段,但在現實世界中的復雜CPS系統(tǒng)上應用仍面臨挑戰(zhàn).因此,反例生成的方法被提出,旨在通過尋找系統(tǒng)中違背安全規(guī)約的反例行為來證明系統(tǒng)的不安全.現有的基于路徑的CPS系統(tǒng)反例生成方法采用分治策略,針對系統(tǒng)模型中各條路徑上的行為空間分別進行探索,能...

深度學習編譯器缺陷實證研究:現狀與演化分析————作者：沈慶超;田家碩;陳俊潔;陳翔;陳慶燕;王贊;

摘要：深度學習編譯器已被廣泛應用于深度學習模型的性能優(yōu)化和部署.與傳統(tǒng)編譯器類似,深度學習編譯器也存在缺陷.存在缺陷的深度學習編譯器會導致編譯失敗或者產生錯誤的編譯結果,甚至有時會帶來災難性的后果.為了深入理解深度學習編譯器缺陷的特性,已有工作針對深度學習編譯器早期的603個缺陷進行研究分析.近年來,深度學習編譯器在快速迭代更新,伴隨著大量新特性的引入和舊特性的棄用.與此同時,一些針對深度學習編譯器缺陷...

操作系統(tǒng)內核權能訪問控制的形式驗證————作者：徐家樂;王淑靈;李黎明;詹博華;呂毅;代藝博;崔舍承;吳鵬;譚宇;張學軍;詹乃軍;

摘要：操作系統(tǒng)內核是構建安全攸關系統(tǒng)軟件的基礎.任何計算機系統(tǒng)的正確運行都依賴于底層操作系統(tǒng)實現的正確性,因此,對操作系統(tǒng)內核進行形式驗證是很迫切的需求.然而,操作系統(tǒng)中存在的多任務并發(fā)、數據共享和競爭等行為,給操作系統(tǒng)內核的驗證帶來很大的挑戰(zhàn).近年來,基于定理證明的方法廣泛用于操作系統(tǒng)各功能模塊的形式驗證,并取得多個成功應用.微內核操作系統(tǒng)權能訪問控制模塊提供基于權能的細粒度訪問控制,旨在防止未經授權...

動態(tài)順序統(tǒng)計樹類結構的函數式建模及其自動化驗證————作者：左正康;劉增鑫;柯雨含;游珍;王昌晶;

摘要：動態(tài)順序統(tǒng)計樹結構是一類融合了動態(tài)集合、順序統(tǒng)計量以及搜索樹結構特性的數據結構,支持高效的數據檢索操作,廣泛應用于數據庫系統(tǒng)、內存管理和文件管理等領域.然而,當前工作側重討論結構不變性,如平衡性,而忽略了功能正確性的討論.且現有研究方法主要針對具體的算法程序進行手工推導或交互式機械化驗證,缺乏成熟且可靠的通用驗證模式,自動化水平較低.為此,設計動態(tài)順序統(tǒng)計搜索樹類結構的Isabelle函數式建模框...

GhostFunc:一種針對Rust操作系統(tǒng)內核的驗證方法————作者：何韜;董威;文艷軍;

摘要：操作系統(tǒng)是軟件的基礎平臺,操作系統(tǒng)內核的安全性往往影響重大. Rust是逐漸興起的內存安全語言,具有生命周期、所有權、借用檢查、RAⅡ等安全機制,使用Rust語言構建內核逐漸成為當前熱門的研究方向.但目前使用Rust構建的系統(tǒng)多包含部分unsafe代碼段,無法從根本上保證語言層面的安全性,因而針對unsafe代碼段的驗證對于保證Rust構建的內核正確可靠尤為重要.以某使用Rust構建的微內核為對象...

干擾惰性序列的連續(xù)決策模型模糊測試————作者：吳泊逾;王凱銳;王亞文;王俊杰;

摘要：人工智能技術的應用已經從分類、翻譯、問答等相對靜態(tài)的任務延伸到自動駕駛、機器人控制、博弈等需要和環(huán)境進行一系列“交互-行動”才能完成的相對動態(tài)的任務.執(zhí)行這類任務的模型核心是連續(xù)決策算法,由于面臨更高的環(huán)境和交互的不確定性,而且這些任務往往是安全攸關的系統(tǒng),其測試技術面臨極大的挑戰(zhàn).現有的智能算法模型測試技術主要集中在單一模型的可靠性、復雜任務多樣性測試場景生成、仿真測試等方向,對連續(xù)決策模型的“...

基于代碼控制流圖的龐氏騙局合約檢測————作者：黃靜;王夢曉;韓紅桂;

摘要：區(qū)塊鏈在加密貨幣投資領域展現出強勁的生命力,吸引了大量投資者的參與.然而,由于區(qū)塊鏈的匿名性,導致了許多欺詐行為,其中龐氏騙局智能合約就是一種典型的欺詐性投資活動,給投資者帶來了巨大的經濟損失.因此,對以太坊上的龐氏騙局合約進行檢測變得尤為重要.但是,現有研究大都忽略了龐氏騙局合約源代碼中的控制流信息.為提取龐氏騙局合約更豐富的語義信息和結構信息,提出一種基于代碼控制流圖的龐氏騙局合約檢測模型.首...

移動應用GUI測試自動生成技術綜述————作者：王博;陳沖;鄧明;董震;林友芳;郝丹;

摘要：移動應用是近10年來興起的新型計算模式,深刻地影響人民的生活方式.移動應用主要以圖形用戶界面(graphical user interface, GUI)方式交互,而對其進行人工測試需要消耗大量人力和物力.為此,研究者提出針對移動應用GUI的測試自動生成技術以提升測試效率并檢測潛在缺陷.收集了145篇相關論文,系統(tǒng)地梳理、分析和總結現有工作.提出了“測試生成器-測試環(huán)境”研究框架,將該領域的研究按...

LLM賦能的Datalog代碼翻譯技術及增量程序分析框架————作者：王熙灶;沈天琪;賓向榮;卜磊;

摘要：Datalog是一種聲明式邏輯編程語言,在不同領域得到了廣泛應用.近年來,學術界和工業(yè)界對Datalog的興趣高漲,設計并開發(fā)了多種Datalog引擎和相應方言.然而,多方言帶來的一個問題是以一種Datalog方言實現的代碼,一般而言不能在另一種方言的引擎上執(zhí)行.因此,當采用新Datalog引擎時,需要將現有Datalog代碼翻譯到新方言上.目前的Datalog代碼翻譯技術可分為人工重寫代碼和人工...

軟件供應鏈SBOM關鍵技術研究————作者：孫澤雨;吳敬征;凌祥;魏怡琳;羅天悅;武延軍;

摘要：供應鏈級別的開源軟件及組件復用是當前軟件開發(fā)的主流模式.該模式避免了重復開發(fā),降低了研發(fā)成本,提高了開發(fā)效率,但是也不可避免地存在組件的來源未知,成分不清,漏洞不明,許可證違規(guī)等問題.為解決上述問題,研究人員提出了軟件物料清單(software bill of material, SBOM). SBOM詳細列出了構成軟件的組件及組件之間的關系,揭示了潛在的和已知的威脅,使軟件透明化.自提出以來,國...

提交