密码实现安全形式化验证发展现状与展望

doi:10.3981/j.issn.2097-0781.2023.01.007

摘要/Abstract

摘要：

密码是保障网络安全和信息安全的核心技术和基础支撑，但密码实现本身面临多种安全威胁，形式化验证是严格证明密码实现安全性的重要技术手段。文章回顾了国内外在密码实现的功能正确性和内存安全性、时间侧信道安全性、功耗侧信道安全性方面的形式化验证技术发展现状和应用情况，分析了当前面向密码实现的形式化验证技术的不足、挑战和发展趋势。鉴于中国密码实现的安全性需求和相应形式化验证技术积累的不足，建议以研制构建高性能、高可信密码库为目标，以国家重大任务为牵引，通过顶层设计，强化自主创新，统一中间表示语言，研制高效率、高精度、自动化的形式化验证平台及安全编译优化工具链，最小化可信计算基，构造高效率、高可信密码实现通用库，促进产学研融合发展，进一步提高国家网络安全和信息安全的发展质量。

关键词: 密码实现, 安全与隐私, 形式化验证, 功能正确, 内存安全, 侧信道安全

Abstract:

Serving as a foundation, cryptography is the key technique for ensuring network and information security. However, cryptographic implementations suffer from various security threats. Formal verification is the most important technique for rigorously proving the security of cryptographic implementations. This article first reviews the development status and application of formal verification techniques for cryptographic implementations both in China and abroad in terms of functional correctness, memory security, and side-channel security including time and power consumption. Then the article summarizes the drawbacks, current challenges, and development trends of these formal verification techniques for cryptographic implementations. According to the security requirements and limited progress in formal verification techniques for cryptographic implementations in China, it is suggested that high-performance and high-assurance cryptographic libraries should be constructed. In addition, the article proposes to follow the top-down design principle, strengthen independent innovation, and unify intermediate representation language under the guidance of national key task, and it plans to develop a high-efficiency, high-precision, and full-automated formal verification platform and a secure compiler optimization toolchain, create high-performance and high-assurance common cryptographic library with minimized trusted computing base, and promote the integrated development of both academic and industrial communities, so as to improve national network and information security.

Key words: cryptographic implementations, security and privacy, formal verification, functional correctness, memory security, side-channel security

宋富. 密码实现安全形式化验证发展现状与展望[J]. 前瞻科技, 2023, 2(1): 90-105.

SONG Fu. Status and Prospects of Formal Verification for Security of Cryptographic Implementations[J]. Science and Technology Foresight, 2023, 2(1): 90-105.

图/表 6

参考文献 69

[1]	Mouha N, Wang Q J, Gu D W, et al. Differential and linear cryptanalysis using mixed-integer linear programming[C]// Yung M, Liu P, Lin D.Proceedings of 4th International Conference on Information Security and Cryptology. Berlin, Heidelberg: Springer, 2012: 57-76.
[2]	Sun S W, Hu L, Wang P, et al. Automatic security evaluation and (related-key) differential characteristic search:Application to SIMON, PRESENT, LBlock, DES(L) and other bit-oriented block ciphers[C]// Proceedings of the International Conference on the Theory and Application of Cryptology and Information Security. Berlin, Heidelberg: Springer, 2014: 158-178.
[3]	Barthe G, Dupressoir F, Grégoire B, et al. EasyCrypt: A tutorial[C]// Aldini A, Lopez J, Martinelli F. Proceedings of the International School on Foundations of Security Analysis and Design Ⅶ, FOSAD 2012/2013. Cham: Springer, 2014: 146-166.
[4]	Bernstein D J, Duif N, Lange T, et al. High-speed high-security signatures[J]. Journal of Cryptographic Engineering, 2012, 2(2): 77-89. DOI URL
[5]	Kocher P C. Timing attacks on implementations of diffie-Hellman, RSA, DSS, and other systems[C]// Koblitz N. Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology—CRYPTO’96. Berlin, Heidelberg: Springer, 1996: 104-113.
[6]	Kocher P, Jaffe J, Jun B. Differential power analysis[C]// Stern J. Proceedings of the International Conference on the Theory and Application of Cryptographic Techniques, Advances in Cryptology—EUKOCRYPT’99. Berlin, Heidelberg: Springer, 1999: 388-397.
[7]	Quisquater J J, Samyde D. ElectroMagnetic analysis (EMA): Measures and counter-measures for smart cards[C]// Attali I, Jensen T. Proceedings of the International Conference on the Smart Card Programming and Security. Berlin, Heidelberg: Springer, 2001: 200-210.
[8]	Mangard S, Pramstaller N, Oswald E. Successfully attacking masked AES hardware implementations[C]// Rao J R, Sunar B. Proceedings of the 7th International Workshop on Cryptographic Hardware and Embedded Systems—CHES 2005. Berlin, Heidelberg: Springer, 2005: 157-171.
[9]	Brumley B B, Tuveri N. Remote timing attacks are still practical[C]// Atluri V, Diaz C. Proceedings of the 16th European Symposium on Research in Computer Security—ESORICS 2011. Berlin, Heidelberg: Springer, 2011: 355-371.
[10]	Aviram N, Schinzel S, Somorovsky J, et al. DROWN: Breaking TLS using SSLv2[C]// Proceedings of the USENIX Security Symposium. Berkeley: USENIX Association, 2016: 689-706.
[11]	Lipp M, Schwarz M, Gruss D, et al. Meltdown: Reading kernel memory from user space[C]// Proceedings of the USENIX Security Symposium. Berkeley: USENIX Association, 2018: 973-990.
[12]	Kocher P, Horn J, Fogh A, et al. Spectre attacks: Exploiting speculative execution[C]// Proceedings of the 2019 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2019: 1-19.
[13]	Almeida J B, Barbosa M, Barthe G, et al. Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations[C]// Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security. New York: ACM Press, 2013: 1217-1230.
[14]	Bernstein D J, Schwabe P. Gfverif: Fast and easy verification of finite-field arithmetic[EB/OL]. [2022-12-14]. http://gfverif.cryptojedi.org.
[15]	Tomb A. Automated verification of real-world cryptographic implementations[J]. IEEE Security & Privacy, 2016, 14(6): 26-33.
[16]	Erbsen A, Philipoom J, Gross J, et al. Simple high-level code for cryptographic arithmetic-with proofs, without compromises[C]// Proceedings of the 2019 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2019: 1202-1219.
[17]	Protzenko J, Parno B, Fromherz A, et al. EverCrypt: A fast, verified, cross-platform cryptographic provider[C]// Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2020: 983-1002.
[18]	Filliâtre J C, Paskevich A. Why3—Where programs meet provers[C]// Felleisen M, Gardner P. Proceedings of the 22nd European Symposium on Programming. Berlin, Heidelberg: Springer, 2013: 125-128.
[19]	Schoolderman M, Moerman J, Smetsers S, et al. Efficient verification of optimized code[C]// Dutle A, Moscato Mm, Titolo L, et al. Proceedings of the 13th International Symposium on NASA Formal Methods. Cham: Springer, 2021: 304-321.
[20]	Appel A W. Verified software toolchain[C]// Goodloe A E, Person S.Proceedings of the 4th International Symposium on NASA Formal Methods. Berlin, Heidelberg: Springer, 2012, doi: 10.1007/978-3-642-28891-3_2.
[21]	Beringer L, Petcher A, Ye K Q, et al. Verified correctness and security of OpenSSL HMAC[C]// Proceedings of the USENIX Security Symposium. Berkeley: USENIX Association, 2015: 207-221.
[22]	Ye K Q, Green M, Sanguansin N, et al. Verified correctness and security of mbedTLS HMAC-DRBG[C]// Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. New York: ACM Press, 2017: 2007-2020.
[23]	Schwabe P, Viguier B, Weerwag T, et al. A Coq proof of the correctness of X25519 in TweetNaCl[C]// Proceedings of the 2021 IEEE 34th Computer Security Foundations Symposium. Piscataway: IEEE Press, 2021, doi: 10.1109/CSF51468.2021.00023.
[24]	Almeida J B, Barbosa M, Barthe G, et al. Jasmin: High-assurance and high-speed cryptography[C]// Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. New York: ACM Press, 2017: 1807-1823.
[25]	Almeida J B, Baritel-Ruet C, Barbosa M, et al. Machine-checked proofs for cryptographic standards: Indifferentiability of sponge and secure high-assurance implementations of SHA-3[C]// Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. New York: ACM Press, 2019: 1607-1622.
[26]	Almeida J B, Barbosa M, Barthe G, et al. The last mile: High-assurance and high-speed cryptographic implementations[C]// Proceedings of the 2020 IEEE Symposium on Security and Privacy. Piscataway: IEEE Press, 2020: 965-982.
[27]	Barthe G, Cauligi S, Grégoire B, et al. High-assurance cryptography in the spectre era[C]// Proceedings of the 2021 IEEE Symposium on Security and Privacy. Piscataway: IEEE Press, 2021: 1884-1901.
[28]	Fu Y F, Liu J X, Shi X M, et al. Signed cryptographic program verification with typed CryptoLine[C]// Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. New York: ACM Press, 2019: 1591-1606.
[29]	Liu J X, Shi X M, Tsai M H, et al. Verifying arithmetic in cryptographic C programs[C]// Proceedings of the 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). Piscataway:IEEE Press, 2020: 552-564.
[30]	Hwang V, Liu J X, Seiler G, et al. Verified NTT multiplications for NISTPQC KEM lattice finalists: Kyber, SABER, and NTRU[J]. IACR Transactions on Cryptographic Hardware and Embedded Systems, 2022(4): 718-750.
[31]	Doychev G, Feld D, Köpf B, et al. CacheAudit: A tool for the static analysis of cache side channels[C]// Proceedings of the 22nd USENIX conference on Security. New York: ACM Press, 2013: 431-446.
[32]	Almeida J B, Barbosa M, Barthe G, et al. Verifying constant-time implementations[C]// Proceedings of the USENIX Security Symposium. Berkeley: USENIX Association, 2016: 53-70.
[33]	Chen J, Feng Y, Dillig I. Precise detection of side-channel vulnerabilities using quantitative Cartesian Hoare logic[C]// Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. New York: ACM Press, 2017: 875-890.
[34]	Antonopoulos T, Gazzillo P, Hicks M, et al. Decomposition instead of self-composition for proving the absence of timing channels[C]// Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press, 2017: 362-375.
[35]	Yang W K, Vizel Y, Subramanyan P, et al. Lazy self-composition for security verification[C]// Chockler H, Weissenbacher G.Proceedings of the 30th International Conference on Computer Aided Verification. Cham: Springer, 2018: 136-156.
[36]	Wu M, Guo S J, Schaumont P, et al. Eliminating timing side-channel leaks using program repair[C]// Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis. New York: ACM Press, 2018: 15-26.
[37]	Cauligi S, Soeller G, Johannesmeyer B, et al. FaCT: A DSL for timing-sensitive computation[C]// Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press, 2019: 174-189.
[38]	Watt C, Renner J, Popescu N, et al. CT-wasm: Type-driven secure cryptography for the web ecosystem[J]. Proceedings of the ACM on Programming Languages, 2019, doi: 10.1145/3290390. DOI
[39]	Wu M, Wang C. Abstract interpretation under speculative execution[C]// Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press, 2019: 802-815.
[40]	Guo S J, Chen Y Q, Li P, et al. SpecuSym: Speculative symbolic execution for cache timing leak detection[C]// Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering. New York: ACM Press, 2020: 1235-1247.
[41]	Wang G H, Chattopadhyay S, Biswas A K, et al. KLEESpectre: Detecting information leakage through speculative cache attacks via symbolic execution[J]. ACM Transactions on Software Engineering and Methodology, 2020, 29(3), doi: 10.1145/3385897. DOI
[42]	Daniel L A, Bardin S, Rezk T. Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level[C]// Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2020: 1021-1038.
[43]	Guarnieri M, Köpf B, Morales J F, et al. Spectector: Principled detection of speculative information flows[DB/OL]. arXiv preprint:1812.08639, 2018.
[44]	Cauligi S, Disselkoen C, Gleissenthall K V, et al. Constant-time foundations for the new spectre era[C]// Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press, 2020: 913-926.
[45]	Wang G H, Chattopadhyay S, Gotovchits I, et al. oo7: Low-overhead defense against spectre attacks via program analysis[J]. IEEE Transactions on Software Engineering, 2021, 47(11): 2504-2519. DOI URL
[46]	Vassena M, Disselkoen C, Von Gleissenthall K, et al. Automatically eliminating speculative leaks from cryptographic code with blade[J]. Proceedings of the ACM on Programming Languages, 2021, doi: 10.1145/3434330. DOI
[47]	Daniel L A, Bardin S, Rezk T. Hunting the haunter—Efficient relational symbolic execution for spectre with haunted RelSE[C]// Proceedings 2021 Network and Distributed System Security Symposium. Reston: Internet Society, 2021, doi: 10.14722/ndss.2021.24286.
[48]	Shivakumar B A, Barthe G, Grégoire B, et al. Enforcing fine-grained constant-time policies[C]// Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security. New York: ACM Press, 2022: 83-96.
[49]	Qin Q, Jiyang J, Song F, et al. DeJITLeak: Eliminating JIT-induced timing side-channel leaks[C]// Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. New York: ACM Press, 2022: 872-884.
[50]	Eldib H, Wang C, Schaumont P. Formal verification of software countermeasures against side-channel attacks[J]. ACM Transactions on Software Engineering and Methodology, 2014, 24(2), doi: 10.1145/2685616. DOI
[51]	Eldib H, Wang C. Synthesis of masking countermeasures against side channel attacks[C]// Biere A, Bloem R.Proceedings of the 26th International Conference on Computer Aided Verification. Cham: Springer, 2014: 114-130.
[52]	Eldib H, Wang C, Taha M, et al. QMS: Evaluating the side-channel resistance of masked software from source code[C]// Proceedings of the 2014 51st ACM/EDAC/IEEE Design Automation Conference (DAC). Piscataway: IEEE Press, 2014, doi: 10.1145/2593069.2593193.
[53]	Barthe G, Belaïd S, Dupressoir F, et al. Verified proofs of higher-order masking[C]// Oswald E, Fischlin M.Proceedings of the 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Advances in Cryptology—EUROCRYPT 2015. Berlin, Heidelberg: Springer, 2015: 457-485.
[54]	Barthe G, Belaïd S, Dupressoir F, et al. Strong non-interference and type-directed higher-order masking[C]// Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. New York: ACM Press, 2016: 116-129.
[55]	Blot A, Yamamoto M, Terauchi T. Compositional synthesis of leakage resilient programs[C]// Maffei M, Ryan M.Proceedings of the 6th International Conference on Principles of Security and Trust. Berlin, Heidelberg: Springer, 2017: 277-297.
[56]	Coron J S. Formal verification of side-channel countermeasures via elementary circuit transformations[C]// Preneel B, Vercauteren F. Proceedings of the 16th International Conference on Applied Cryptography and Network Security. Cham: Springer, 2018: 65-82.
[57]	Bloem R, Gross H, Iusupov R, et al. Formal verification of masked hardware implementations in the presence of glitches[C]// Nielsen J B, Rijmen V. Proceedings of the 37th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Advances in Cryptology—EUROCRYPT 2018. Cham: Springer, 2018: 321-353.
[58]	Zhang J, Gao P F, Song F, et al. SCInfer: Refinement-based verification of software countermeasures against side-channel attacks[C]// Chockler H, Weissenbacher G. Proceedings of the 30th International Conference on Computer Aided Verification. Cham: Springer, 2018: 157-177.
[59]	Gao P F, Zhang J, Song F, et al. Verifying and quantifying side-channel resistance of masked software implementations[J]. ACM Transactions on Software Engineering and Methodology, 2019, 28(3), doi: 10.1145/3330392. DOI
[60]	Wang J B, Sung C, Wang C. Mitigating power side channels during compilation[C]// Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. New York: ACM Press, 2019: 590-601.
[61]	Barthe G, Belaïd S, Cassiers G, et al. MaskVerif: Automated verification of higher-order masking in presence of physical defaults[C]// Sako K, Schneider S, Ryan P Y A. Proceedings of the 24th European Symposium on Research in Computer Security—ESORICS 2019. Cham: Springer, 2019: 300-318.
[62]	Belaïd S, Goudarzi D, Rivain M. Tight private circuits: Achieving probing security with the least refreshing[C]// Peyrin T, Galbraith S D. Proceedings of the 24th International Conference on the Theory and Application of Cryptology and Information Security, Advances in Cryptology—ASIACRYPT 2018. Cham: Springer, 2018: 343-372.
[63]	Belaïd S, Dagand P É, Mercadier D, et al. Tornado: Automatic generation of probing-secure masked bitsliced implementations[C]// Canteaut A, Ishai Y. Proceedings of the 39th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Advances in Cryptology—EUROCRYPT 2020. Cham: Springer, 2020: 311-341.
[64]	Knichel D, Sasdrich P, Moradi A. SILVER—Statistical independence and leakage verification[C]// Moriai S, Wang H. Proceedings of the 26th International Conference on the Theory and Application of Cryptology and Information Security, Advances in Cryptology—ASIACRYPT 2020. Cham: Springer, 2020: 787-816.
[65]	Belaïd S, Coron J S, Prouff E, et al. Random probing security:Verification, composition, expansion and new constructions[C]// Micciancio D, Ristenpart T. Proceedings of the 40th Annual International Cryptology Conference, Advances in Cryptology—CRYPTO 2020. Cham: Springer, 2020: 339-368.
[66]	Gao P F, Xie H Y, Song F, et al. A hybrid approach to formal verification of higher-order masked arithmetic programs[J]. ACM Transactions on Software Engineering and Methodology, 2021, 30(3), doi: 10.1145/3428015. DOI
[67]	Cassiers G, Grégoire B, Levi I, et al. Hardware private circuits: from trivial composition to full verification[J]. IEEE Transactions on Computers, 2021, 70(10): 1677-1690. DOI URL
[68]	Gao P F, Xie H Y, Sun P, et al. Formal verification of masking countermeasures for arithmetic programs[J]. IEEE Transactions on Software Engineering, 2022, 48(3): 973-1000.
[69]	Belaïd S, Mercadier D, Rivain M, et al. IronMask: Versatile verification of masking security[C]// Proceedings of the 2022 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2022: 142-160.

验证工具和文献	年份	内存安全	验证技术	自动化程度	输入语言	目标语言	应用
Frama-C^[13]	2013	●	抽象解释演绎推理	◉	C	C	RSA-OEAP, MEE-CBC
gfverif^[14]	2015	○	代数系统	●	C	C	X25519
Cryptol+SAW^[15]	2016	●	程序等价静态符号执行	◉	C, Java	C, Java	Salsa20, AES, ZUC, FFS, ECDSA, SHA-3
Fiat Crypto^[16]	2019	●	定理证明	○	Gallina	C	Curve25519, P256
EverCrypt^[17]	2020	●	演绎推理定理证明	◉	F^*, Vale	C, ASM, WASM	HACL^*库和ValeCrypt
Why3^[18-19]	2021	◉	演绎推理	◉	WhyML	OCaml, ASM	BGW, X25519
VST^{[20⇓⇓-23]}	2021	●	定理证明	○	Gallina	C	DRBG, SHA-256, SHA-2, X25519
Jasmin^{[24⇓⇓-27]}	2021	●	抽象解释演绎推理定理证明	◉	Jasmin	C, ASM	ChaCha20, Poly1305, SHA-3
CryptoLine^[28⇓-30]	2022	●	演绎推理代数系统	●	CryptoLine	C, ASM	NaCl, OpenSSL等库函数

验证工具和文献	年份	内存安全	验证技术	自动化程度	输入语言	目标语言	应用
Frama-C^[13]	2013	●	抽象解释演绎推理	◉	C	C	RSA-OEAP, MEE-CBC
gfverif^[14]	2015	○	代数系统	●	C	C	X25519
Cryptol+SAW^[15]	2016	●	程序等价静态符号执行	◉	C, Java	C, Java	Salsa20, AES, ZUC, FFS, ECDSA, SHA-3
Fiat Crypto^[16]	2019	●	定理证明	○	Gallina	C	Curve25519, P256
EverCrypt^[17]	2020	●	演绎推理定理证明	◉	F^*, Vale	C, ASM, WASM	HACL^*库和ValeCrypt
Why3^[18-19]	2021	◉	演绎推理	◉	WhyML	OCaml, ASM	BGW, X25519
VST^{[20⇓⇓-23]}	2021	●	定理证明	○	Gallina	C	DRBG, SHA-256, SHA-2, X25519
Jasmin^{[24⇓⇓-27]}	2021	●	抽象解释演绎推理定理证明	◉	Jasmin	C, ASM	ChaCha20, Poly1305, SHA-3
CryptoLine^[28⇓-30]	2022	●	演绎推理代数系统	●	CryptoLine	C, ASM	NaCl, OpenSSL等库函数

验证工具和文献	年份	泄漏模型	验证技术	验证精度	输入语言	目标语言	应用
CacheAudit^[31]	2013	①②	抽象解释	◉	二进制	二进制	AES, eSTREAM
ct-verif^[32]	2016	①②③	交叉积	●	C	Boogie	Nacl, OpenSSL, BoringSSL
Themis^[33]	2017	①	污点分析自组合	○	Java	Java	DARPA STAC测试集
Blazer^[34]	2017	①	污点分析复杂度比较	○	Java	Java	DARPA STAC测试集
IFC-CEGAR/BMC^[35]	2018	①②	污点分析惰性自组合	●	LLVM IR	C	—
SC Eliminator^[36]	2018	①②	类型系统自动修复	◉	LLVM IR	C	AES, DES, LBlock, PRESET等
FaCT^[37]	2019	①②③	类型系统自动修复	◉	FaCT	LLVM IR	Poly1305, XSalsa20, MEE-CBC, Curve25519
CT-Wasm^[38]	2019	①②③	类型系统	◉	WASM	WASM	Salsa20, SHA-256, TweetNaCl
AISE^[39]	2019	②④	抽象解释	◉	LLVM IR	C	hpn-ssh, LibTomCrypt, OpenSSL,Tegra
EverCrypt^[17]	2020	①②③	污点分析类型系统	◉	Low^*, Vale	C, ASM	HACL^*库和ValeCrypt
SpecuSym^[40]	2020	④	动态符号执行	○	LLVM IR	C	hpn-ssh, LibTomCrypt, OpenSSL,Tegra
KleeSpectre^[41]	2020	④	动态符合执行	○	LLVM IR	C	hpn-ssh, LibTomCrypt, OpenSSL,Tegra
BINSEC/REL^[42]	2020	①②	关系符号执行	○	汇编	二进制	HACL^*, OpenSSL, BearSSL
SPECTECTOR^[43]	2020	④	静态符号执行	◉	汇编	汇编	—
Pitchfork^[44]	2020	④⑤	污点分析静态符号执行	◉	汇编	汇编	Poly1305, XSalsa20, MEE-CBC, Curve25519
Oo7^[45]	2020	①②④⑤	污点分析自动修复	○	二进制	二进制	Litmus Tests, SPECint
Blade^[46]	2021	④⑤	类型系统自动修复	◉	WASM	WASM, C	Salsa20, SHA-256, ChaCha20, Poly1305, Curve25519
Binsec/Haunted^[47]	2021	①②④⑤	关系静态静态符号执行	○	汇编	二进制	Libsodium, OpenSSL
Jasmin^{[24⇓⇓-27,48]}	2022	①②④⑤⑥	定理证明	●	Jasmin	C, 汇编	ChaCha20, Poly1305, keccak1600等
DeJITLeak^[49]	2022	①⑥	类型系统自动修复	◉	Java 字节码	Java 字节码	DARPA STAC测试集

验证工具和文献	年份	泄漏模型	验证技术	验证精度	输入语言	目标语言	应用
CacheAudit^[31]	2013	①②	抽象解释	◉	二进制	二进制	AES, eSTREAM
ct-verif^[32]	2016	①②③	交叉积	●	C	Boogie	Nacl, OpenSSL, BoringSSL
Themis^[33]	2017	①	污点分析自组合	○	Java	Java	DARPA STAC测试集
Blazer^[34]	2017	①	污点分析复杂度比较	○	Java	Java	DARPA STAC测试集
IFC-CEGAR/BMC^[35]	2018	①②	污点分析惰性自组合	●	LLVM IR	C	—
SC Eliminator^[36]	2018	①②	类型系统自动修复	◉	LLVM IR	C	AES, DES, LBlock, PRESET等
FaCT^[37]	2019	①②③	类型系统自动修复	◉	FaCT	LLVM IR	Poly1305, XSalsa20, MEE-CBC, Curve25519
CT-Wasm^[38]	2019	①②③	类型系统	◉	WASM	WASM	Salsa20, SHA-256, TweetNaCl
AISE^[39]	2019	②④	抽象解释	◉	LLVM IR	C	hpn-ssh, LibTomCrypt, OpenSSL,Tegra
EverCrypt^[17]	2020	①②③	污点分析类型系统	◉	Low^*, Vale	C, ASM	HACL^*库和ValeCrypt
SpecuSym^[40]	2020	④	动态符号执行	○	LLVM IR	C	hpn-ssh, LibTomCrypt, OpenSSL,Tegra
KleeSpectre^[41]	2020	④	动态符合执行	○	LLVM IR	C	hpn-ssh, LibTomCrypt, OpenSSL,Tegra
BINSEC/REL^[42]	2020	①②	关系符号执行	○	汇编	二进制	HACL^*, OpenSSL, BearSSL
SPECTECTOR^[43]	2020	④	静态符号执行	◉	汇编	汇编	—
Pitchfork^[44]	2020	④⑤	污点分析静态符号执行	◉	汇编	汇编	Poly1305, XSalsa20, MEE-CBC, Curve25519
Oo7^[45]	2020	①②④⑤	污点分析自动修复	○	二进制	二进制	Litmus Tests, SPECint
Blade^[46]	2021	④⑤	类型系统自动修复	◉	WASM	WASM, C	Salsa20, SHA-256, ChaCha20, Poly1305, Curve25519
Binsec/Haunted^[47]	2021	①②④⑤	关系静态静态符号执行	○	汇编	二进制	Libsodium, OpenSSL
Jasmin^{[24⇓⇓-27,48]}	2022	①②④⑤⑥	定理证明	●	Jasmin	C, 汇编	ChaCha20, Poly1305, keccak1600等
DeJITLeak^[49]	2022	①⑥	类型系统自动修复	◉	Java 字节码	Java 字节码	DARPA STAC测试集

验证工具和文献	年份	安全模型	阶数	可组合验证	验证技术	验证精度	输入语言	目标语言	应用
SC Sniffer^[50⇓-52]	2014	①⑦	1,2	N	约束求解自动修复	●	布尔电路	C	Keccak, AES-Sbox
EasyCrypt^[53]	2015	①⑥	≥1	N	证明系统	◉	EasyCrypt	EasyCrypt	Keccak, AES, AES-Sbox
maskComp^[54]	2016	②③	≥1	Y	证明系统自动修复	◉	C	C	AES, Keccak, Simon, Speck
BYT^[55]	2017	①	≥1	Y	约束求解自动修复	●	布尔电路	C	Keccak, AES-Sbox
CheckMasks^[56]	2018	②③	≥1	N	初等变换	◉	Lisp	Lisp	布尔算术互转函数
Rebecca^[57]	2018	①⑤	≥1	N	傅里叶分析约束求解	◉	布尔电路	Verilog	Keccak/AES-Sbox
SC Infer^[58-59]	2019	①⑦	1	N	类型系统约束求解混合验证	●	布尔电路	C	Keccak, AES-Sbox
SC Sniffer2^[60]	2019	①⑥	1	N	类型系统自动修复	◉	布尔电路	C	Keccak, AES-Sbox
maskVerif^[61]	2019	①②③⑤⑥	≥1	N	证明系统	◉	布尔电路	Verilog	Keccak/AES-Sbox
tightPROVE^+[62-63]	2020	①	≥1	Y	线性代数自动修复	◉	布尔电路	Usuba	NIST 2nd Round 轻量级加密算法
SILVER^[64]	2020	①②③④⑤	≥1	N	二元决策图	●	布尔电路	Verilog	AES/PREENT/ PRINCE-Sbox
VRAPS^[65]	2020	⑧	≥1	Y	类型系统	◉	布尔电路	Sage	AES
HOME^[66]	2021	①	≥1	N	类型系统约束求解混合验证	●	算术电路	C	Keccak, AES
fullverif^[67]	2021	④⑤	≥1	Y	依赖分析	●	布尔电路	Verilog	Sbox
QMV_ERIF^[68]	2022	①⑥⑦	1	Y	类型系统约束求解混合验证	●	算术电路	C	Keccak, AES-Sbox
IronMask^[69]	2022	②③④⑤⑥⑧	≥1	N	高斯消元	◉	布尔电路	Sage	乘法器