安全性路徑驗證主要是針對系統上, 資料傳輸的路徑進行驗證, 以確保系統的資料流不會在不經意的情況下遭到外部惡意的讀取或是寫入, 傳統的檢查方法通常是以演算法搭配相關的模擬(Simulation) 來進行安全性路徑的檢查。
汙點(Taint) 或是路徑敏感性測試(Path Sensitization) 是一種常見的在軟硬體中針對資料傳輸來進行標記的方法, 主要目的是藉由汙點的傳遞來瞭解資料流的去向, 當資料接觸到危險區的時候進行回報, 並且警告使用者, 軟硬體設計師透過這種方法進行模擬(Simulation) 並且調整設計的安全性問題。
模型驗證是使用狀態空間搜索自動驗證的工具之一, 模型驗證相對於傳統的模擬(Simulation) 驗證方式, 更能將整個驗證流程自動化, 而不需要與模擬(Simulation) 一樣需要準備許多測試資料, 在驗證時間與驗證人力的縮減上面可得到更大的提升。
本文提供了一種新式的演算法主要針對於將安全性路徑驗證的問題搭配汙點(Taint) 的理論將問題自動化的轉入至模型驗證器中可讀取的形式再由開源的模型驗證器(Nu-SMV) 來進行模型驗證(Model Checking), 透過模型驗證的特性, 使得使用者在驗證時可以得到完整性的驗證結果, 而非像傳統的模擬結果一樣, 當發生問題時才進行修改。

Security path verification is mainly for verifying the path of data transmission on the system to ensure that the data flow of the system will not be read or written by external malicious inadvertently. The traditional inspection method is usually based on calculation.
The method is combined with the relevant simulation to check the safety path. Taint or Path Sensitization is a common method of marking data transmission in hardware and software.
The main purpose is to understand the whereabouts of data flow through the transmission of stains. Reward in the danger zone and warn the user that the hardware and software designer performs the simulation and adjusts the design safety issues. Model verification is one of the tools for automatic verification using state space search. Model verification can automate the entire verification process compared to the traditional simulation verification method, without the need to prepare many test materials as well as simulation. A greater improvement can be achieved in the verification time and the reduction in verification manpower.
This paper provides a new type of algorithm mainly for the problem of security path verification with Taint theory. The problem is automatically transferred to the readable form of the model validator and then by the open source model validator (Nu -SMV) to perform Model Checking, through the characteristics of the model verification, so that the user can obtain the integrity verification result when verifying, instead of modifying it when a problem occurs, just like the traditional simulation result.

[1] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008.
[2] Cadence. (jaspergold,spv). https://www.cadence.com/.
[3] Ricardo Corin and Felipe Andrés Manzano. Taint analysis of security code in the klee symbolic execution engine. In International Conference on Information and Communications Security, pages 264–275. Springer, 2012.
[4] Jacobus Willem De Bakker and Erik De Vink. Control flow semantics. Citeseer, 1996.
[5] E Allen Emerson and Joseph Y Halpern.“sometimes”and“not never”revisited: on branching versus linear time temporal logic. Journal of the ACM (JACM), 33(1):151–178, 1986.
[6] William Fu, Raymond Lin, and Daniel Inge. Taintassembly: Taint-based information flow control tracking for webassembly. arXiv preprint arXiv:1802.01050, 2018.
[7] Patrice Godefroid, Michael Y Levin, David A Molnar, et al. Automated whitebox fuzz testing. In NDSS, volume 8, pages 151–166. Citeseer, 2008.
[8] ITREAD01.COM. (design for test). https://www.itread01.com/content/1550318945.html.
[9] Chao Ma, Anping He, Tingting Jiab, Lian Lic, and Zhihua Feng. Security path checking of a circuit with behavior. 2017.
[10] Nicolas Markey and Philippe Schnoebelen. Symbolic model checking for simplytimed systems. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pages 102–117. Springer, 2004.
[11] Jiang Ming, Dinghao Wu, Gaoyao Xiao, Jun Wang, and Peng Liu. Taintpipe: pipelined symbolic taint analysis. In 24th {USENIX} Security Symposium ({USENIX} Security 15), pages 65–80, 2015.
[12] James Newsome and Dawn Xiaodong Song. Dynamic taint analysis for automatic detection, analysis, and signaturegeneration of exploits on commodity software. In NDSS, volume 5, pages 3–4. Citeseer, 2005.
[13] Perl. (perldoc.perl.org). https://perldoc.perl.org/perlsec.html.
[14] Roberta Piscitelli, Shivam Bhasin, and Francesco Regazzoni. Fault attacks, injection techniques and tools for simulation. In Hardware Security and Trust, pages 27–47. Springer, 2017.
[15] Technews. (formal analysis of security data paths in rtl design). https://www.research.ibm.com.
[16] Technews. (hardware trojans in the chip: What are the security risks of the x86 cpu?). https://kknews.cc/tech/85eaee.html.
[17] Ilja Tšahhirov and Peeter Laud. Application of dependency graphs to security protocol analysis. In International Symposium on Trustworthy Global Computing, pages 294–311. Springer, 2007.
[18] Zhemin Yang and Min Yang. Leakminer: Detect information leakage on android with static taint analysis. In 2012 Third World Congress on Software Engineering, pages 101–104. IEEE, 2012.