馬藝新, 唐時博, 譚靜, 李雪霏, 胡偉

(西北工業(yè)大學(xué) 網(wǎng)絡(luò)空間安全學(xué)院, 陜西 西安 710072)

密碼技術(shù)是網(wǎng)絡(luò)與信息安全的重要支撐性技術(shù),是用于保障信息機密性和完整性等關(guān)鍵屬性的重要手段。密碼算法在數(shù)學(xué)上的安全性與其實現(xiàn)的安全性是2個截然不同的問題。雖然密碼算法的安全性已經(jīng)從數(shù)學(xué)上得到證明,但是,密碼算法核實現(xiàn)會由于設(shè)計錯誤、旁路信道[1]、調(diào)試接口[2]或后門程序[3]等原因引入安全漏洞。這些安全漏洞一旦被攻擊者挖掘與利用,將能夠在較低時間和空間復(fù)雜度條件下完全恢復(fù)算法保密密鑰。攻擊者可進一步利用密鑰竊取更多有價值的信息,使得密碼算法核以及計算設(shè)備的安全性受到嚴(yán)重威脅。

在密碼核硬件電路設(shè)計過程中,驗證的時間開銷往往達(dá)到總工作量的40%～70%[4]。功能驗證的局限性在于:覆蓋率依賴于測試激勵信號，導(dǎo)致驗證覆蓋率低、驗證不充分;設(shè)計規(guī)模很大或要模擬的情況很多時通常會導(dǎo)致模擬時間會很長,驗證效率低。密碼算法核中的高隱蔽性安全漏洞,單純依靠有限次的功能測試很難保證可以覆蓋。由此可見,功能驗證難以滿足密碼算法核的安全驗證需求。

信息流跟蹤(information flow tracking,IFT)方法通過為存儲對象添加安全標(biāo)簽，并通過計算與跟蹤存儲對象的標(biāo)簽執(zhí)行信息流安全策略去驗證、控制整個硬件系統(tǒng)的信息流動[5]。信息流跟蹤方法具有良好的信息流監(jiān)控能力,可以防止有害的信息流動。Tiwari等[6]提出了門級信息流跟蹤(gate level information flow tracking,GLIFT)方法。GLIFT方法通過為每個二進制位數(shù)據(jù)分配一比特的標(biāo)簽精確地監(jiān)控每個二進制位信息的流動,是一種細(xì)粒度的信息流控制方法,能夠通過捕捉有害的信息流動來檢測和消除設(shè)計中潛在的安全漏洞。Ferraiuolo等[7]設(shè)計了一種帶類型系統(tǒng)的安全Verilog語言SecVerilog,通過在設(shè)計編譯階段靜態(tài)檢查不同安全級別數(shù)據(jù)之間的信息流安全屬性,給出了一種驗證處理器架構(gòu)中安全域和非安全域之間隔離特性的方法。Jin等提出了一種基于攜帶證明代碼的硬件安全驗證框架,硬件知識產(chǎn)權(quán)(intellectual property,IP)核攜帶了安全屬性相關(guān)的定理,可利用Coq進行安全定理證明,從而檢測第三方IP核中潛在的木馬設(shè)計[8-9]。Ardeshiricham等[10]提出了寄存器傳輸級信息流跟蹤(register transfer level information flow tracking,RTLIFT)方法,它能夠直接在寄存器傳輸級(register transfer level,RTL)代碼的基礎(chǔ)上生成精確的IFT邏輯,進行安全驗證。

現(xiàn)有的安全驗證方法需要設(shè)計者用新的語言重新編寫硬件模型,或者需要設(shè)計新的驗證框架,或者由于抽象層次低不能擴展到大的設(shè)計。本文從信息流安全的角度研究密碼算法核安全驗證與漏洞檢測方法,基于信息流分析的安全驗證方法只需要掌握密碼算法核的RTL級源碼或門級網(wǎng)表,在RTL級源碼或者門級網(wǎng)表的基礎(chǔ)上描述信息流和標(biāo)簽的傳播,不需要設(shè)計者學(xué)習(xí)新的硬件安全語言。本文利用可實現(xiàn)形式化驗證功能的綜合工具Yosys,它支持自定義信息流安全屬性,在定義不同信息流關(guān)系時更加靈活,例如,顯式流還是隱式流,并且在較高的抽象層次上工作會提高驗證速度。

本文通過對Aoki Laboratory[11]發(fā)布的密碼算法核中全部邏輯信息流進行精確度量,對機密性、完整性等安全屬性進行形式化驗證,可捕捉到電路中的有害信息流,對密碼算法核中的安全漏洞以及時間側(cè)信道有很好的檢測效果。

1 背景

1.1 硬件信息流分析

信息流是指信息的流動和傳播,在本文中信息流均代表與硬件設(shè)計系統(tǒng)邏輯狀態(tài)密切相關(guān)的邏輯信息流。硬件信息流分析中,數(shù)據(jù)通常被賦予一個標(biāo)簽,該標(biāo)簽表征數(shù)據(jù)的安全屬性,如可信/不可信或保密/非保密。在數(shù)據(jù)運算過程中標(biāo)簽隨之在電路中傳播,硬件信息流分析中標(biāo)簽傳播策略是根據(jù)當(dāng)前操作類型、輸入以及輸入標(biāo)簽來確定輸出的標(biāo)簽,通過靜態(tài)分析或動態(tài)檢查輸出的標(biāo)簽,可以有效防止違反信息流安全策略的運算操作,防止有害信息流的流動,例如:保密信息流向了電路中非保密區(qū)域數(shù)據(jù)寄存器,可信區(qū)域程序計數(shù)器中接收到了來自以太網(wǎng)的不可信數(shù)據(jù)。

如表1所示,以密碼算法核為例詳細(xì)介紹標(biāo)簽傳播規(guī)則。密碼算法核中密鑰與輸入進行與操作,密鑰與輸入均為一比特,密鑰為K,輸入為M,輸出為O=K&M,kt,mt和ot為密鑰、輸入和輸出的標(biāo)簽。K,M∈{0,1},kt,mt,ot∈{LOW,HIGH},其中標(biāo)簽“LOW”代表密碼算法核中低安全級別屬性非保密或者可信,標(biāo)簽“HIGH”代表密碼算法核中高安全級別安全屬性保密或者不可信。

假定L(a)為信號a的信息流跟蹤邏輯,當(dāng)at=1時,L(a)=HIGH,當(dāng)at=0時,L(a)=LOW。在運算操作中對輸出起關(guān)鍵決策作用的輸入的標(biāo)簽決定了輸出的標(biāo)簽,例如輸入A的標(biāo)簽為HIGH,A=0,輸入B的標(biāo)簽為LOW,B=1,A為0決定了輸出為0,所以輸出標(biāo)簽由A安全級別決定,輸出標(biāo)簽為HIGH。由表1可以推導(dǎo)出密碼算法核中二輸入與門的信息流跟蹤邏輯為(1)式。

表1 密碼算法核中與操作的標(biāo)簽傳播規(guī)則

ot=Mkt+Kmt+ktmt

(1)

類似地,可以得到密碼算法核中其他基本邏輯門如非門、或門和異或門等基本邏輯單元的信息流模型,從而可以構(gòu)建信息流模型庫。根據(jù)信息流模型庫可以為密碼算法核的每一個邏輯單元離散式地生成信息流模型,從而為整個密碼算法核設(shè)計生成信息流模型。

1.2 信息流安全驗證

安全驗證是一種在流片前對硬件設(shè)計進行的基于屬性的邏輯驗證,安全驗證能夠證明一些被定義好的安全屬性在硬件設(shè)計中是否一直成立。根據(jù)具體方法的不同,進行安全驗證的硬件設(shè)計可能是RTL級代碼或者邏輯門級網(wǎng)表。

基于硬件信息流分析的安全驗證是檢測密碼算法核安全漏洞的一種手段。假設(shè)密碼算法核中包含安全漏洞,密碼算法核正常運行產(chǎn)生正確的運算結(jié)果,并不會觀察到安全漏洞,只有在罕見的情況下,例如違反電路機密性(如密鑰泄露至輸出)時,安全漏洞才會被觀察到。安全漏洞難以通過有限次的功能驗證被覆蓋,信息流分析方法則可取得更好的檢測效果。

在安全屬性的定義中,機密性屬性主要是保證高安全級別敏感信息不會流向密碼算法核中可公開觀測的區(qū)域。標(biāo)準(zhǔn)硬件描述語言Verilog和VHDL只能描述功能屬性,不能用于描述安全屬性。信息流分析中關(guān)注信息的流動,更好地描述了機密性、完整性等安全屬性,安全屬性可采用斷言語言描述。

圖1描述了信息流安全驗證方法。密碼算法核可以作為安全驗證的檢測對象,該方法分析了密碼算法核中需滿足的通用安全屬性,如機密性、完整性、隔離特性以及一些模式相關(guān)的屬性等。將安全屬性映射至密碼算法核的安全驗證模型上,主要進行屬性相關(guān)信號安全級別的劃分和安全屬性標(biāo)簽的實例化,以及安全屬性中斷言語句向功能性驗證語言的轉(zhuǎn)化。完成安全屬性的映射之后,即可結(jié)合密碼算法核的信息流模型,采用形式化驗證工具實現(xiàn)安全屬性的驗證,若驗證失敗則表明存在安全漏洞,同時會生成一個反例,可用于漏洞復(fù)現(xiàn)。

圖1 密碼算法核安全驗證方法

2 密碼核安全驗證與漏洞檢測方法

2.1 密碼算法核信息流模型的生成

在1.1節(jié)為密碼算法核中基本邏輯門構(gòu)造信息流模型的基礎(chǔ)上,可以構(gòu)造一個功能完備的信息流模型庫,通過為密碼算法核中更復(fù)雜的功能單元生成信息流模型,最終生成整個密碼算法核的信息流模型。

如圖2所示,生成密碼算法核的信息流模型首先需要構(gòu)建一個包含基本邏輯單元如與門、或門、非門等的信息模型庫。給定一個邏輯函數(shù),首先使用邏輯綜合工具將其綜合為由基本邏輯單元描述的門級網(wǎng)表,例如圖2中將二輸入選擇器邏輯函數(shù)轉(zhuǎn)化為由2個與門和1個或門描述的門級網(wǎng)表;然后將門級網(wǎng)表映射至基本邏輯單元信息流模型庫中,為門級網(wǎng)表中的各個邏輯單元實例化信息流模型,生成了邏輯函數(shù)的信息流模型。圖2中生成了二輸入選擇器的信息流模型;當(dāng)使用信息流模型生成算法為邏輯函數(shù)生成信息流模型后,將邏輯函數(shù)的信息流模型集成至基本邏輯單元信息流模型庫中,將基本信息流模型庫擴充至復(fù)雜信息流模型庫;對密碼算法核而言,可使用同樣的方法,經(jīng)過邏輯綜合生成門級網(wǎng)表,將門級網(wǎng)表中各個邏輯單元映射至復(fù)雜硬件信息流模型庫,為密碼算法核中各個邏輯單元實例化地附加信息流模型,由此生成整個密碼算法核的信息流模型。

圖2 密碼算法核信息流模型的生成

2.2 安全屬性

對密碼算法核進行安全驗證的前提是分析電路所需遵循的安全屬性,如機密性、完整性、隔離特性以及時間信道等。首先需要描述所需驗證的安全屬性,通常借鑒SystemVerilog Assertion等斷言描述語言的語義,并拓展安全相關(guān)的特性。安全屬性描述語言常用的關(guān)鍵字,主要包含安全級別的設(shè)置、安全屬性的斷言、斷言條件的設(shè)置以及許可路徑的設(shè)定。關(guān)鍵字set用來設(shè)置信號安全級別,如保密、公開、可信、不可信等,關(guān)鍵字assert用來斷言信號安全級別。

在安全屬性描述語言的基礎(chǔ)上,可以對密碼算法核中通常需要滿足的安全屬性進行描述。完整性屬性保證高安全級別的不可信信號不會流向低安全級別的可信區(qū)域;機密性屬性保證高安全級別的保密信號不會流向可公開觀測的區(qū)域。在機密性驗證中將保密信號設(shè)置為高安全級別HIGH,并斷言其不會流向低安全級別LOW的輸出。例如,斷言密鑰不應(yīng)該流向中間數(shù)據(jù)寄存器,描述如下:

set key=HIGH

assert data-reg==LOW

將安全屬性描述語言轉(zhuǎn)化為形式化驗證工具Yosys可以識別的安全約束,即進行安全標(biāo)簽的設(shè)置,以及屬性相關(guān)信號安全級別的劃分與設(shè)置,具體如下所示:

assign key-t= 1′b1

assert data-reg-t== 1′b0

2.3 安全驗證與漏洞檢測

Yosys是種基于Verilog的開源綜合與驗證工具,該工具在命令行窗口下啟動和運行。它可以將Verilog代碼綜合為邏輯門級網(wǎng)表,內(nèi)置用于檢查安全屬性和功能的布爾可滿足性(boolean satisfiability problem,SAT)求解器。

圖3描述了密碼算法核安全驗證與漏洞檢測方案。首先將密碼算法核通過Yosys綜合生成邏輯門級網(wǎng)表,然后根據(jù)2.1節(jié)的信息流模型生成方法,對門級網(wǎng)表進行分析,對門級網(wǎng)表中的邏輯單元進行處理,包括信號端口定義、基本邏輯門、寄存器、觸發(fā)器以及賦值語句等,為門級網(wǎng)表中的每個邏輯單元實例化信息流模型,最終生成整個密碼算法核的信息流模型。

圖3 密碼算法核安全驗證與漏洞檢測方案

密碼算法核信息流模型是安全驗證的基礎(chǔ)。通過對密碼算法核進行安全需求分析,建立密碼算法核安全屬性庫,將密碼算法核需滿足的安全規(guī)范使用安全屬性描述語言進行描述,然后對密碼算法核中屬性相關(guān)信號進行安全等級的劃分,其次通過信號安全標(biāo)簽的設(shè)置,指定允許或禁止的信息流,通常采用斷言語句進行信息流的禁止或許可。這些安全屬性斷言被寫入密碼算法核信息流模型中,用于驗證信息流安全流動。例如,機密性驗證中需要將保密信號設(shè)置為高安全級別HIGH,并禁止它流向低安全級別LOW的輸出。假設(shè)密鑰不應(yīng)該被泄露,將密鑰安全屬性標(biāo)記為HIGH,其他信號安全屬性標(biāo)記為LOW,因為這是一個關(guān)于機密性的屬性,需要檢查密文有效信號是否始終為LOW,這種安全屬性的驗證描述如下:

set key-t HIGH

set DEAFAULT-LABEL LOW

assert cipher-ready-t LOW

將安全屬性轉(zhuǎn)化為Yosys可識別的安全約束腳本或文件,結(jié)合寫入安全屬性斷言的信息流模型,調(diào)用Yosys驗證工具進行安全驗證,分析密碼算法核安全驗證模型中安全屬性以及敏感信息的流動,觀察待驗證的安全屬性標(biāo)簽信號值。根據(jù)Yosys驗證的結(jié)果判斷是否存在違反信息流安全規(guī)范的信息流動,若驗證成功則不存在安全漏洞,若驗證失敗則通過分析驗證失敗時相關(guān)信號的值,對安全漏洞特征進行分析以及定位,結(jié)合驗證工具給出的反例對信息流模型進行功能測試,可獲得密碼算法核中安全漏洞的泄露途徑以及漏洞行為。

3 實驗與分析

3.1 實驗環(huán)境與方案

硬件環(huán)境為英特爾i7處理器,16 GB內(nèi)存。軟件環(huán)境為64位Ubuntu 20.04.1操作系統(tǒng),編譯器為gcc 9.3.0。實驗如圖4所示,包含3個部分:設(shè)計輸入、安全驗證和驗證輸出分析。實驗驗證的對象是加密算法IP核,來自Aoki Laboratory[11]。

圖4 實驗方案

3.2 AES密碼算法核安全驗證

1) 對下載的密碼算法核使用Yosys綜合工具進行綜合,具體是使用綜合腳本和script命令,例如對于AES密碼算法核,對其進行綜合,產(chǎn)生門級網(wǎng)表。

2) 對綜合后產(chǎn)生的邏輯網(wǎng)表進行處理,對邏輯網(wǎng)表中的每一個邏輯單元進行分析,包括端口定義、基本邏輯門、寄存器、觸發(fā)器以及賦值語句等,實例化每一個邏輯單元的信息流模型,最后生成密碼算法核的信息流模型。

3) 對密碼算法核的信息流模型進行分析,根據(jù)密碼算法核中的信號與安全標(biāo)簽的傳播以及電路安全規(guī)范對需要驗證的安全屬性進行分析,對屬性相關(guān)信號進行安全級別劃分,以及安全標(biāo)簽的設(shè)置,實現(xiàn)信息流規(guī)則描述。例如在AES-Comp IP核中對密鑰信號進行分析,根據(jù)機密性安全屬性中禁止高安全級別的保密信號流向可公開觀測的區(qū)域,使用安全屬性描述語言進行描述,并斷言密鑰信號不會直接流向可公開觀測的密文輸出,具體描述如下:

set key-t HIGH

set DEFAULT-LABEL LOW

assert Dout-t LOW

將安全屬性編譯為Yosys可識別的安全約束,即安全驗證腳本。在安全驗證中,不對明文、密文、密鑰和其他狀態(tài)信號的安全級別進行細(xì)致的劃分,將除密文外所有信號的安全標(biāo)簽置為0,重點關(guān)注密鑰泄露問題。為了在輸出結(jié)果中更直觀地體現(xiàn)出密鑰的流動,得到更直觀的驗證結(jié)果,將部分密鑰位的安全標(biāo)簽設(shè)置為1,部分位的污染標(biāo)簽設(shè)置為0。例如將密鑰污染標(biāo)簽最低位設(shè)置為1,剩余位設(shè)置為0,即Kin-t=128 ′h01。為了捕捉密鑰泄露安全漏洞,需要設(shè)置反例,向信息流模型中加入安全斷言,設(shè)置一條賦值語句,當(dāng)輸出信號安全標(biāo)簽等于密鑰安全標(biāo)簽時,即輸出信號為高安全級別時,將證明信號proof-f的安全標(biāo)簽賦值為1,具體如下:

assign proof-t=(Dout-t==128 ′h01)? 1∶0;

Yosys中集成了SAT求解器,在安全腳本中添加SAT形式化驗證語句,從而形式化地驗證證明信號的值是否始終為0,是則驗證成功,否則驗證失敗?？煞治霭踩┒吹拇嬖?使用SAT形式化驗證進行安全驗證的腳本為sat -prove proof-t 1′b0。得到的驗證結(jié)果如圖5所示,可以看出寄存器AES-Comp-ENC.Drg-t的值等于Kin-t的值。

圖5 AES-Comp密碼算法核形式化驗證結(jié)果

根據(jù)加密算法擴散和混淆的特點,密鑰的任何一位都應(yīng)該對密文的多位存在影響,盡管只有最低位密鑰安全標(biāo)簽為1,加密結(jié)果中至少有一半位的安全標(biāo)簽為1。通過Mentor Graphics ModelSim工具進行仿真,得到加密結(jié)果中僅有最低位安全標(biāo)簽為1,功能仿真中未捕捉到密鑰和加密結(jié)果的值相等的波形。

圖6顯示了AES密碼算法核加密模塊的硬件結(jié)構(gòu),如被標(biāo)記為虛線所示,執(zhí)行第一輪密鑰加時,明文與密鑰異或的結(jié)果直接被賦值給密文輸出端口。如圖7所示,將仿真testbench中明文設(shè)置為全0,則在輸出端口上可直接觀測到密鑰值。因為只有最低位密鑰受到污染,所以密文輸出中也只有最低位受到污染。經(jīng)過信息流安全驗證與功能驗證結(jié)合分析得到,在特定明文輸入條件下即明文為全0時密碼核直接泄露了全部的密鑰,此種安全漏洞屬于由中間加密結(jié)果導(dǎo)致的關(guān)鍵信息泄露。

圖6 AES-Comp密碼算法核加密模塊的硬件結(jié)構(gòu)[11]

圖7 AES密碼算法核密鑰泄露仿真波形

3.3 RSA密碼算法核安全驗證

本實驗采用Aoki Laboratory[11]提供的RSA密碼算法核進行安全驗證和漏洞檢測,在安全驗證過程中,不對明文、模數(shù)、密鑰和其他狀態(tài)信號的安全級別進行細(xì)致的劃分,將密鑰的安全標(biāo)簽全部置為1,其他信號的標(biāo)簽置為0。按照3.2節(jié)中的方法對RSA密碼算法核進行邏輯綜合,并產(chǎn)生信息流模型。

對生成的信息流模型進行安全驗證,使用Mentor Graphics ModelSim工具進行時序仿真,通過分析仿真產(chǎn)生波形的變化來驗證相關(guān)信號安全標(biāo)簽是否會產(chǎn)生變化,檢驗是否存在安全漏洞。設(shè)置密鑰信號32′hFFFFFFFF,經(jīng)過一段時間的仿真后,Dout-t信號變?yōu)?2′hFFFFFFFF,BSY-t信號也變?yōu)?。Dout輸出的標(biāo)簽信號受到污染是毋庸置疑的,因為密鑰必然會影響輸出。BSY信號是操作完成的標(biāo)志,當(dāng)IP核進行加密、解密或者導(dǎo)入數(shù)據(jù)之后,BSY信號變?yōu)?。通過對RSA密碼算法核進行分析,該密碼算法利用密鑰位進行算法流程控制。密鑰位取 1 或者取 0 時會導(dǎo)致條件分支語句執(zhí)行,需要執(zhí)行不同的操作,會導(dǎo)致 RSA模冪運算時間出現(xiàn)差異[12],操作時間上的差異導(dǎo)致RSA密碼算法核中存在時間側(cè)信道。

信息流安全仿真的結(jié)果表明:受污染的密鑰不僅導(dǎo)致密文輸出受到污染,還導(dǎo)致了操作完成信號(BSY)受到了污染,這表明了密鑰也流向了BSY信號。密鑰流向密文信號是毋容置疑的,因為密鑰影響著加密結(jié)果。在本次實驗中,密鑰對BSY信號是沒有直接影響的,當(dāng)加密完成后,BSY信號總會由0變?yōu)?。事實上,由BSY信號的標(biāo)簽BSY-t從0變?yōu)?可以看到密鑰確實影響了BSY信號。這是由于密鑰值的變化導(dǎo)致操作時間存在差異,從而BSY信號由0置1的時間也發(fā)生了變化,這屬于時間信息流。

通過信息流安全驗證的方法與工具,可以捕捉到由密鑰信號到加密完成信號的時間隱通道。

圖8 RSA密碼算法核時間隱通道仿真結(jié)果

3.4 IP核安全驗證總結(jié)

對Aoki Laboratory[11]中的6個密碼算法核進行安全驗證,總結(jié)如表2所示。經(jīng)過信息流安全驗證和信息流仿真,DES、AES、Camellia、MISTY1和CAST-128密碼核經(jīng)過安全驗證以后均發(fā)現(xiàn)有明文或者密鑰通過中間寄存器泄露至輸出的漏洞行為。這是由于上述幾種密碼算法核的設(shè)計實現(xiàn)方式導(dǎo)致的,中間寄存器的存在使得關(guān)鍵信息存在泄露風(fēng)險。RSA密碼核中發(fā)現(xiàn)了由密鑰到操作完成信號的時間側(cè)信道。對密碼算法核進行形式化安全驗證和功能仿真,形式化驗證在Ubuntu平臺下Yosys中完成；功能仿真在Windows系統(tǒng)下Mentor Graphics ModelSim中完成。對驗證時間和資源消耗進行統(tǒng)計,結(jié)果列于表3?？梢钥闯?，DES和MISTY1密碼算法核在功能仿真中沒有捕捉到密鑰或明文泄露。

表2 密碼核安全驗證與漏洞檢測結(jié)果

表3 密碼核驗證性能

4 結(jié) 論

由于傳統(tǒng)功能驗證方法已經(jīng)無法滿足密碼算法核安全驗證的需求,本文提出了利用信息流安全驗證的方法進行密碼算法核驗證。以Aoki Laboratory中的密碼算法核作為測試基準(zhǔn),信息流安全驗證方法通過為每個信號添加安全標(biāo)簽的方式為整個密碼算法核設(shè)計產(chǎn)生安全驗證模型,利用形式化驗證工具Yosys進行輸出信號安全級別的檢測,從而驗證是否存在違反信息流安全屬性的有害信息流流動。輔助使用仿真工具Mentor Graphics ModelSim,進行信息流仿真,對敏感信息的泄露行為有了直觀展現(xiàn),并且通過相關(guān)信號安全標(biāo)簽的變化分析出RSA密碼算法核中時間側(cè)信道的存在。無論是對中間寄存器導(dǎo)致的敏感信息泄露還是時間信息流,信息流安全驗證方法都有較好的檢測效果。需要進一步完善的是如何自動化書寫高質(zhì)量安全屬性。