一種基于冗余編碼的變量簽名唯一性安全保證方法

曹 杰 汪明新 孫軍峰

鐵路信號行業直接涉及列車的安全運行和人民群眾的生命財產安全，其安全產品必須滿足RAMS（可靠性、可用性、可維護性、安全性）的要求。尤其對于車載ATP系統，必須達到SIL4級的系統安全完善度等級。系統要求基于安全冗余編碼技術，獨立于軟件和硬件環境，可以防護硬件或內存錯誤等引起的操作數、操作符及運算錯誤，能夠保證系統在復雜的軟件和硬件環境下達到SIL4級要求的錯誤不可檢出率，有效提升系統的安全度等級。目前，多數ATP系統中都使用冗余代碼來保證系統的安全性，雖然形式各異但基本原理相同，并已應用在許多地鐵項目中。

要使系統達到SIL4標準要求的錯誤不可檢出率，需要保證冗余代碼中所有變量在同一時刻的簽名都是唯一的。為此，提出了一種基于冗余編碼的變量簽名唯一性安全保證方法，可以確保系統中所有的變量簽名都是唯一的，這樣系統的所有單點故障都可以檢測出來。而對于多點故障 （發生多次尋址錯誤或硬件失效等故障，這類故障發生概率非常小，一般情況下可忽略不計），系統的錯誤不可檢出率也明顯降低，該方法大大降低了系統的錯誤不可檢出率。

1 編碼理論

微處理器及其電路中所有影響和干擾處理器運算的錯誤，從處理數據層次上或者從數據的角度，可以歸為以下3種類型：①運算錯誤，即處理器在運算過程中發生了錯誤；②操作數錯誤，即處理器在運算時，提取了錯誤的運算數；③操作符錯誤，即處理器使用了正確的運算數，卻混淆了運算符。

冗余編碼算法采用了AN碼、分離碼相結合的編碼方式。對簡單變量x，設計其編碼后的形式為：

其中，A為編碼時選擇的大素數；Bx為編碼時為變量x分配的數據簽名，取值范圍為 ［1，A－1］；DT為時間戳，取值范圍為 ［1，A－1］。在實際編碼中，將2k位的數據分成了高k位和低k位，高k位為數值域，存放數據原始值，XH＝x；低k位為校驗域，校驗處理器錯誤

令rkx＝ （2kx）modA，2kx－（2kx）modA ，能夠被A整除，符合AN碼的格式。按照這種編碼方法，通過AN碼可以檢測算術運算操作是否錯誤；對每個操作數分配一個固定的簽名Bx，可以檢測操作數尋址簽名錯誤和操作符錯誤；時間戳DT可以檢測循環中變量的值沒有被更新的錯誤，或者因為失效使用上個周期變量值的錯誤。

2 設計與實現

在現有的安全冗余編碼系統中，對源碼中所有的變量都會生成高位和低位，其中高位存儲源碼的變量值，低位存儲變量的校驗信息，通過高位和低位信息可以計算出變量的簽名。所以，在系統每個周期運行結束后，通過檢查變量的簽名是否正確，來判斷系統在運行過程中是否出現尋址錯誤、硬件失效等故障 （非系統本身的邏輯錯誤）。如果變量的簽名不唯一，就會導致系統的故障可能檢測不出來，也不便于系統安全的定量分析。

2．1 軟件功能結構

一種基于冗余編碼的變量簽名唯一性安全保證方法，包括經簽名產生模塊后依次進入簽名分配模塊或簽名計算模塊、簽名檢查模塊，最后在簽名存儲模塊存儲簽名，其功能結構如圖1所示。

1．簽名產生模塊：按照簽名生成算法產生足夠的簽名。

2．簽名分配與計算模塊：對待編碼的文件進行冗余編碼，判斷待編碼的語句的類型，為每個變量分配或計算簽名。

3．簽名檢查模塊：對簽名分配與計算模塊得到的簽名做簽名唯一性檢查，如果該簽名與已經分配的簽名相同，則從簽名表中重新取一個簽名分配給該變量。

4．簽名存儲模塊：存儲經過簽名檢查模塊檢查的簽名。

圖1 軟件功能結構示意圖

2．2 工作流程

圖2為該方法的工作流程圖，圖3為簽名產生模塊流程，圖4為簽名計算模塊基本運算簽名處理流程。結合圖2～圖4對各步驟進行詳細描述。

步驟1：按照簽名生成算法產生簽名，圖3是簽名產生模塊的具體步驟，如果產生的簽名個數足夠，就轉向步驟2，否則繼續執行步驟1。例如可以設定產生20000個簽名。

步驟2：輸入待編碼的文件，判斷待編碼的語句的類型，為每個變量分配或計算簽名。

1．該語句為變量定義或聲明，則從步驟1生成的簽名表中分配一個簽名給該變量。

2．該語句屬于基本運算，則判斷該基本運算屬于哪種運算，圖4描述了該過程的具體步驟。如果是加、減、乘、除運算，或者是邏輯與、或、非運算，或者是左移、右移運算，都按照相應運算的簽名計算方式計算簽名。

圖3 簽名產生模塊流程圖

3．該語句為數組運算。如果是數組賦值、數組取值運算，按照相應運算的簽名計算方式計算簽名。

4．該語句為分支、循環結構，也按分支、循環結構的簽名計算方式計算簽名。

5．該語句為函數調用。如果為模塊函數調用或計算函數調用，按相應簽名計算方式計算簽名。

為變量分配或計算好簽名后，則轉向步驟3。

步驟3：對步驟2（或步驟4）得到的簽名做簽名唯一性檢查，如果該簽名與已經分配的簽名相同，則轉向步驟4，否則轉向步驟5。

步驟4：從簽名表中重新取一個簽名分配給該變量，再轉向步驟3。

步驟5：存儲經過簽名唯一性檢查的簽名，并判斷編碼是否結束，如果沒有到達待編碼文件的結尾，則轉向步驟2，否則轉向步驟6。

步驟6：結束。

3 分析

按照隨機編碼思想，在一個消息空間中有N個消息；其中有M個消息是合法消息，那么N個消息中某個消息發生了錯誤，變成合法消息 （M中的一個）的概率P為：

P＝M／N

前提：編碼碼字M在消息空間N中分布足夠隨機。

采用基于冗余編碼的變量簽名唯一性安全保證方法處理后，系統的有效內存空間中所有變量簽名都是唯一的，即對于每個變量該內存空間中只存在一個合法的消息，因此，如果一個合法變量發生錯誤，該變量只可能變成該內存空間中的一個非法變量，從而利用冗余編碼算法簽名錯誤檢查機制檢測出該錯誤。

與現有技術相比，該方法保證了所有變量的簽名都是唯一的，所有的變量都被唯一標識，系統的所有單點故障都能檢測出來；而系統的多點故障，只要基于內存空間中的所有消息 （對應系統中的簽名）的分布足夠隨機 （從某種程度上來說是一種偽隨機），就可以通過對系統的安全進行定量分析，也證明該方法明顯降低了系統的錯誤不可檢出率。

圖4 簽名計算模塊基本運算簽名處理流程圖

［1］ 姜堅華．loo2D模型分析及其在地鐵列車自動防護系統中的應用［J］．城市軌道交通研究，2011，6：25－28．

［2］ IEC 61508 2010Functional Safety of electrical／electronic／programmable electronic safety－related system［S］．

［3］ Forin P．Vital Coded Microprocessor Principle and Application for Various Transit Systems［C］．1989 IFAC CCCT Symposium：79－84．