Article(id=1241719284355878952, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, articleNumber=null, orderNo=8, doi=10.3981/j.issn.2097-0781.2023.01.007, pmid=null, cstr=null, oa=null, hot=null, price=null, onlineType=0, articleFormat=0, articleType=null, articleTypeStr=research-article, receivedDate=1671984000000, receivedDateStr=2022-12-26, revisedDate=1675267200000, revisedDateStr=2023-02-02, acceptedDate=null, acceptedDateStr=null, onlineDate=1679846400000, onlineDateStr=2023-03-27, pubDate=1679241600000, pubDateStr=2023-03-20, doiRegisterDate=null, doiRegisterDateStr=null, onlineIssueDate=1679846400000, onlineIssueDateStr=2023-03-27, onlineJustAcceptDate=null, onlineJustAcceptDateStr=null, onlineFirstDate=null, onlineFirstDateStr=null, sourceXml=null, magXml=null, createTime=1773978547415, creator=sys-migrate, updateTime=1773978547415, updator=sys-migrate, issue=Issue{id=1241719216169079576, tenantId=1146029695717560320, journalId=1146032081894723586, year='2023', volume='2', issue='1', pageStart='5', pageEnd='143', issueExtLink='null', onlineDate='null', pubDate='null', beforeIssueId=null, nextIssueId=null, price=null, status=1, issueComplete=1, articleOrder=1, issueType=-1, specialIssue=1, createTime=1773978531159, creator=sys-migrate, updateTime=1774001248771, updator=13041195026, preIssue=null, nextIssue=null, ext={EN=IssueExt(id=1241814500781916967, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, language=EN, specialIssueTitle=Science and Technology Foresight, coverIllustrator=null, specialIssueEditor=null, specialIssueAbout=null), CN=IssueExt(id=1241814500781916968, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, language=CN, specialIssueTitle=形式化方法与复杂计算系统可信保障, coverIllustrator=null, specialIssueEditor=null, specialIssueAbout=null)}, issueFiles=null}, startPage=90, endPage=105, ext={EN=ArticleExt(id=1241719288571154485, articleId=1241719284355878952, tenantId=1146029695717560320, journalId=1146032081894723586, language=EN, title=Status and Prospects of Formal Verification for Security of Cryptographic Implementations, columnId=1149656489310208610, journalTitle=Science and Technology Foresight, columnName=Review and Commentary, runingTitle=null, highlight=null, articleAbstract=
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.
, correspAuthors=null, authorNote=null, correspAuthorsNote=null, copyrightStatement=null, copyrightOwner=null, extLink=null, articleAbsUrl=null, sourceXml=null, magXml=null, pdfUrl=null, pdf=null, pdfFileSize=null, pdfExtLink=null, richHtmlUrl=null, mobilePdfUrl=null, reviewReport=null, pdfFirstPage=null, abstractGraph=null, abstractGraphContent=null, abstractVideo=null, citation=null, cebUrl=null, magXmlContent=null, mapNumber=null, authorCompany=null, fund=null, authors=null, authorsList=Fu SONG), CN=ArticleExt(id=1241719288436936756, articleId=1241719284355878952, tenantId=1146029695717560320, journalId=1146032081894723586, language=CN, title=密码实现安全形式化验证发展现状与展望, columnId=1148708266483446458, journalTitle=前瞻科技, columnName=综述与述评, runingTitle=null, highlight=null, articleAbstract=
密码是保障网络安全和信息安全的核心技术和基础支撑，但密码实现本身面临多种安全威胁，形式化验证是严格证明密码实现安全性的重要技术手段。文章回顾了国内外在密码实现的功能正确性和内存安全性、时间侧信道安全性、功耗侧信道安全性方面的形式化验证技术发展现状和应用情况，分析了当前面向密码实现的形式化验证技术的不足、挑战和发展趋势。鉴于中国密码实现的安全性需求和相应形式化验证技术积累的不足，建议以研制构建高性能、高可信密码库为目标，以国家重大任务为牵引，通过顶层设计，强化自主创新，统一中间表示语言，研制高效率、高精度、自动化的形式化验证平台及安全编译优化工具链，最小化可信计算基，构造高效率、高可信密码实现通用库，促进产学研融合发展，进一步提高国家网络安全和信息安全的发展质量。
, correspAuthors=null, authorNote=null, correspAuthorsNote=null, copyrightStatement=null, copyrightOwner=null, extLink=null, articleAbsUrl=null, sourceXml=vTv+5J9BP5X3tYDt07DBLw==, magXml=CNbOQr4+9RmpWx2uQ00dug==, pdfUrl=null, pdf=erXCBY0/VizFikJqA7etGg==, pdfFileSize=2446887, pdfExtLink=null, richHtmlUrl=null, mobilePdfUrl=null, reviewReport=null, pdfFirstPage=null, abstractGraph=KlmYvAiQMSkE9ucgDcb59A==, abstractGraphContent=null, abstractVideo=null, citation=null, cebUrl=null, magXmlContent=CkyWnzGu0f43rTZ2TgvlKQ==, mapNumber=null, authorCompany=null, fund=null, authors=
 |
宋富，上海科技大学信息科学与技术学院长聘副教授，研究员。上海科技大学系统与安全中心主任。研究方向为形式化验证、系统安全和人工智能安全。主持和参与多项国家自然科学基金青年、面上、重点和中德国际合作项目。发表论文70余篇。获欧洲软件科学与技术协会最佳论文奖、亚马逊研究奖和上海市“浦江人才”、上海市“晨光学者”荣誉称号。电子信箱：songfu@shanghaitech.edu.cn。 |
, authorsList=宋富)}, authors=[Author(id=1241719307609109494, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, orderNo=0, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=songfu@shanghaitech.edu.cn, emailSecond=null, emailThird=null, correspondingAuthor=0, authorType=1, ext={EN=AuthorExt(id=1241719307676218359, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, authorId=1241719307609109494, language=EN, stringName=Fu SONG, firstName=Fu, middleName=null, lastName=SONG, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=null, address=null, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719307802047480, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, authorId=1241719307609109494, language=CN, stringName=宋富, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=null, address=null, bio={"img":"kNn7zCEcPMPUt6qoeMgj8Q==","content":"
宋富，上海科技大学信息科学与技术学院长聘副教授，研究员。上海科技大学系统与安全中心主任。研究方向为形式化验证、系统安全和人工智能安全。主持和参与多项国家自然科学基金青年、面上、重点和中德国际合作项目。发表论文70余篇。获欧洲软件科学与技术协会最佳论文奖、亚马逊研究奖和上海市“浦江人才”、上海市“晨光学者”荣誉称号。电子信箱：songfu@shanghaitech.edu.cn。
"}, bioImg=kNn7zCEcPMPUt6qoeMgj8Q==, bioContent=
宋富，上海科技大学信息科学与技术学院长聘副教授，研究员。上海科技大学系统与安全中心主任。研究方向为形式化验证、系统安全和人工智能安全。主持和参与多项国家自然科学基金青年、面上、重点和中德国际合作项目。发表论文70余篇。获欧洲软件科学与技术协会最佳论文奖、亚马逊研究奖和上海市“浦江人才”、上海市“晨光学者”荣誉称号。电子信箱：songfu@shanghaitech.edu.cn。
, aboutCorrespAuthor=null)}, companyList=null)], keywords=[Keyword(id=1241719307902710777, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, orderNo=1, keyword=cryptographic implementations), Keyword(id=1241719307974013946, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, orderNo=2, keyword=security and privacy), Keyword(id=1241719308053705723, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, orderNo=3, keyword=formal verification), Keyword(id=1241719309496546304, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, orderNo=4, keyword=functional correctness), Keyword(id=1241719309567848449, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, orderNo=5, keyword=memory security), Keyword(id=1241719309647540227, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, orderNo=6, keyword=side-channel security), Keyword(id=1241719309723037702, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, orderNo=1, keyword=密码实现), Keyword(id=1241719309802729479, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, orderNo=2, keyword=安全与隐私), Keyword(id=1241719309861449736, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, orderNo=3, keyword=形式化验证), Keyword(id=1241719309924364297, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, orderNo=4, keyword=功能正确), Keyword(id=1241719310004056075, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, orderNo=5, keyword=内存安全), Keyword(id=1241719310079553548, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, orderNo=6, keyword=侧信道安全)], refs=[Reference(id=1241719311199432753, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2012, volume=null, issue=null, pageStart=57, pageEnd=76, url=null, language=null, rfNumber=[1], rfOrder=0, authorNames=Mouha N, Wang Q J, Gu D W, journalName=Yung M, Liu P, Lin D.Proceedings of 4th International Conference on Information Security and Cryptology. Berlin, refType=null, unstructuredReference=
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., articleTitle=Differential and linear cryptanalysis using mixed-integer linear programming, refAbstract=null), Reference(id=1241719311287513139, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2014, volume=null, issue=null, pageStart=158, pageEnd=178, url=null, language=null, rfNumber=[2], rfOrder=1, authorNames=Sun S W, Hu L, Wang P, journalName=Proceedings of the International Conference on the Theory and Application of Cryptology and Information Security. Berlin, refType=null, unstructuredReference=
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., articleTitle=Automatic security evaluation and (related-key) differential characteristic search:Application to SIMON, PRESENT, LBlock, DES(L) and other bit-oriented block ciphers, refAbstract=null), Reference(id=1241719311379787828, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2014, volume=null, issue=null, pageStart=146, pageEnd=166, url=null, language=null, rfNumber=[3], rfOrder=2, authorNames=Barthe G, Dupressoir F, Grégoire B, journalName=Aldini A, Lopez J, Martinelli F. Proceedings of the International School on Foundations of Security Analysis and Design Ⅶ, FOSAD 2012/2013, refType=null, unstructuredReference=
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., articleTitle=EasyCrypt: A tutorial, refAbstract=null), Reference(id=1241719311472062520, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=10.1007/s13389-012-0027-1, pmid=null, pmcid=null, year=2012, volume=2, issue=2, pageStart=77, pageEnd=89, url=http://link.springer.com/10.1007/s13389-012-0027-1, language=null, rfNumber=[4], rfOrder=3, authorNames=Bernstein D J, Duif N, Lange T, journalName=Journal of Cryptographic Engineering, refType=null, unstructuredReference=
Bernstein D J,
Duif N,
Lange T, et al. High-speed high-security signatures[J].
Journal of Cryptographic Engineering,
2012,
2(2): 77-89., articleTitle=High-speed high-security signatures, refAbstract=null), Reference(id=1241719311555948602, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=1996, volume=null, issue=null, pageStart=104, pageEnd=113, url=null, language=null, rfNumber=[5], rfOrder=4, authorNames=Kocher P C, journalName=Koblitz N. Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology—CRYPTO’96. Berlin, refType=null, unstructuredReference=
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., articleTitle=Timing attacks on implementations of diffie-Hellman, RSA, DSS, and other systems, refAbstract=null), Reference(id=1241719311623057468, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=1999, volume=null, issue=null, pageStart=388, pageEnd=397, url=null, language=null, rfNumber=[6], rfOrder=5, authorNames=Kocher P, Jaffe J, Jun B, journalName=Stern J. Proceedings of the International Conference on the Theory and Application of Cryptographic Techniques, Advances in Cryptology—EUKOCRYPT’99. Berlin, refType=null, unstructuredReference=
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., articleTitle=Differential power analysis, refAbstract=null), Reference(id=1241719311685972029, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2001, volume=null, issue=null, pageStart=200, pageEnd=210, url=null, language=null, rfNumber=[7], rfOrder=6, authorNames=Quisquater J J, Samyde D, journalName=Attali I, Jensen T. Proceedings of the International Conference on the Smart Card Programming and Security. Berlin, refType=null, unstructuredReference=
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., articleTitle=ElectroMagnetic analysis (EMA): Measures and counter-measures for smart cards, refAbstract=null), Reference(id=1241719311761469503, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2005, volume=null, issue=null, pageStart=157, pageEnd=171, url=null, language=null, rfNumber=[8], rfOrder=7, authorNames=Mangard S, Pramstaller N, Oswald E, journalName=Rao J R, Sunar B. Proceedings of the 7th International Workshop on Cryptographic Hardware and Embedded Systems—CHES 2005. Berlin, refType=null, unstructuredReference=
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., articleTitle=Successfully attacking masked AES hardware implementations, refAbstract=null), Reference(id=1241719311832772672, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2011, volume=null, issue=null, pageStart=355, pageEnd=371, url=null, language=null, rfNumber=[9], rfOrder=8, authorNames=Brumley B B, Tuveri N, journalName=Atluri V, Diaz C. Proceedings of the 16th European Symposium on Research in Computer Security—ESORICS 2011. Berlin, refType=null, unstructuredReference=
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., articleTitle=Remote timing attacks are still practical, refAbstract=null), Reference(id=1241719311904075841, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2016, volume=null, issue=null, pageStart=689, pageEnd=706, url=null, language=null, rfNumber=[10], rfOrder=9, authorNames=Aviram N, Schinzel S, Somorovsky J, journalName=Proceedings of the USENIX Security Symposium, refType=null, unstructuredReference=
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., articleTitle=DROWN: Breaking TLS using SSLv2, refAbstract=null), Reference(id=1241719311983767619, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2018, volume=null, issue=null, pageStart=973, pageEnd=990, url=null, language=null, rfNumber=[11], rfOrder=10, authorNames=Lipp M, Schwarz M, Gruss D, journalName=Proceedings of the USENIX Security Symposium, refType=null, unstructuredReference=
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., articleTitle=Meltdown: Reading kernel memory from user space, refAbstract=null), Reference(id=1241719312105402436, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=1, pageEnd=19, url=null, language=null, rfNumber=[12], rfOrder=11, authorNames=Kocher P, Horn J, Fogh A, journalName=Proceedings of the 2019 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2019, refType=null, unstructuredReference=
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., articleTitle=Spectre attacks: Exploiting speculative execution, refAbstract=null), Reference(id=1241719312193482821, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2013, volume=null, issue=null, pageStart=1217, pageEnd=1230, url=null, language=null, rfNumber=[13], rfOrder=12, authorNames=Almeida J B, Barbosa M, Barthe G, journalName=Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security, refType=null, unstructuredReference=
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., articleTitle=Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations, refAbstract=null), Reference(id=1241719312264785991, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=null, pageEnd=null, url=http://gfverif.cryptojedi.org, language=null, rfNumber=[14], rfOrder=13, authorNames=Bernstein D J, Schwabe P, journalName=Gfverif: Fast and easy verification of finite-field arithmetic, refType=null, unstructuredReference=
Bernstein D J,
Schwabe P.
Gfverif: Fast and easy verification of finite-field arithmetic[EB/OL]. [
2022-12-14]. http://gfverif.cryptojedi.org., articleTitle=null, refAbstract=null), Reference(id=1241719312352866377, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2016, volume=14, issue=6, pageStart=26, pageEnd=33, url=null, language=null, rfNumber=[15], rfOrder=14, authorNames=Tomb A, journalName=IEEE Security & Privacy, refType=null, unstructuredReference=
Tomb A. Automated verification of real-world cryptographic implementations[J].
IEEE Security & Privacy,
2016,
14(6): 26-33., articleTitle=Automated verification of real-world cryptographic implementations, refAbstract=null), Reference(id=1241719312411586635, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=1202, pageEnd=1219, url=null, language=null, rfNumber=[16], rfOrder=15, authorNames=Erbsen A, Philipoom J, Gross J, journalName=Proceedings of the 2019 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2019, refType=null, unstructuredReference=
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., articleTitle=Simple high-level code for cryptographic arithmetic-with proofs, without compromises, refAbstract=null), Reference(id=1241719312495472716, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=983, pageEnd=1002, url=null, language=null, rfNumber=[17], rfOrder=16, authorNames=Protzenko J, Parno B, Fromherz A, journalName=Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2020, refType=null, unstructuredReference=
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., articleTitle=EverCrypt: A fast, verified, cross-platform cryptographic provider, refAbstract=null), Reference(id=1241719313959284814, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2013, volume=null, issue=null, pageStart=125, pageEnd=128, url=null, language=null, rfNumber=[18], rfOrder=17, authorNames=Filliâtre J C, Paskevich A, journalName=Felleisen M, Gardner P. Proceedings of the 22nd European Symposium on Programming. Berlin, refType=null, unstructuredReference=
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., articleTitle=Why3—Where programs meet provers, refAbstract=null), Reference(id=1241719314085113936, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=304, pageEnd=321, url=null, language=null, rfNumber=[19], rfOrder=18, authorNames=Schoolderman M, Moerman J, Smetsers S, journalName=Dutle A, Moscato Mm, Titolo L, et al. Proceedings of the 13th International Symposium on NASA Formal Methods. Cham: Springer, refType=null, unstructuredReference=
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., articleTitle=Efficient verification of optimized code, refAbstract=null), Reference(id=1241719314169000017, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2012, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[20], rfOrder=19, authorNames=Appel A W, journalName=Goodloe A E, Person S.Proceedings of the 4th International Symposium on NASA Formal Methods. Berlin, refType=null, unstructuredReference=
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., articleTitle=Verified software toolchain, refAbstract=null), Reference(id=1241719314244497491, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2015, volume=null, issue=null, pageStart=207, pageEnd=221, url=null, language=null, rfNumber=[21], rfOrder=20, authorNames=Beringer L, Petcher A, Ye K Q, journalName=Proceedings of the USENIX Security Symposium, refType=null, unstructuredReference=
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., articleTitle=Verified correctness and security of OpenSSL HMAC, refAbstract=null), Reference(id=1241719314315800661, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2017, volume=null, issue=null, pageStart=2007, pageEnd=2020, url=null, language=null, rfNumber=[22], rfOrder=21, authorNames=Ye K Q, Green M, Sanguansin N, journalName=Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, refType=null, unstructuredReference=
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., articleTitle=Verified correctness and security of mbedTLS HMAC-DRBG, refAbstract=null), Reference(id=1241719314378715223, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[23], rfOrder=22, authorNames=Schwabe P, Viguier B, Weerwag T, journalName=Proceedings of the 2021 IEEE 34th Computer Security Foundations Symposium, refType=null, unstructuredReference=
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., articleTitle=A Coq proof of the correctness of X25519 in TweetNaCl, refAbstract=null), Reference(id=1241719314445824089, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2017, volume=null, issue=null, pageStart=1807, pageEnd=1823, url=null, language=null, rfNumber=[24], rfOrder=23, authorNames=Almeida J B, Barbosa M, Barthe G, journalName=Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, refType=null, unstructuredReference=
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., articleTitle=Jasmin: High-assurance and high-speed cryptography, refAbstract=null), Reference(id=1241719314521321563, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=1607, pageEnd=1622, url=null, language=null, rfNumber=[25], rfOrder=24, authorNames=Almeida J B, Baritel-Ruet C, Barbosa M, journalName=Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, refType=null, unstructuredReference=
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., articleTitle=Machine-checked proofs for cryptographic standards: Indifferentiability of sponge and secure high-assurance implementations of SHA-3, refAbstract=null), Reference(id=1241719314596819037, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=965, pageEnd=982, url=null, language=null, rfNumber=[26], rfOrder=25, authorNames=Almeida J B, Barbosa M, Barthe G, journalName=Proceedings of the 2020 IEEE Symposium on Security and Privacy, refType=null, unstructuredReference=
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., articleTitle=The last mile: High-assurance and high-speed cryptographic implementations, refAbstract=null), Reference(id=1241719314676510815, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=1884, pageEnd=1901, url=null, language=null, rfNumber=[27], rfOrder=26, authorNames=Barthe G, Cauligi S, Grégoire B, journalName=Proceedings of the 2021 IEEE Symposium on Security and Privacy, refType=null, unstructuredReference=
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., articleTitle=High-assurance cryptography in the spectre era, refAbstract=null), Reference(id=1241719314760396897, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=1591, pageEnd=1606, url=null, language=null, rfNumber=[28], rfOrder=27, authorNames=Fu Y F, Liu J X, Shi X M, journalName=Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, refType=null, unstructuredReference=
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., articleTitle=Signed cryptographic program verification with typed CryptoLine, refAbstract=null), Reference(id=1241719314844282979, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=552, pageEnd=564, url=null, language=null, rfNumber=[29], rfOrder=28, authorNames=Liu J X, Shi X M, Tsai M H, journalName=Proceedings of the 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). Piscataway:IEEE Press, 2020, refType=null, unstructuredReference=
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., articleTitle=Verifying arithmetic in cryptographic C programs, refAbstract=null), Reference(id=1241719314936557669, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=4, pageStart=718, pageEnd=750, url=null, language=null, rfNumber=[30], rfOrder=29, authorNames=Hwang V, Liu J X, Seiler G, journalName=IACR Transactions on Cryptographic Hardware and Embedded Systems, refType=null, unstructuredReference=
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., articleTitle=Verified NTT multiplications for NISTPQC KEM lattice finalists: Kyber, SABER, and NTRU, refAbstract=null), Reference(id=1241719315049803879, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2013, volume=null, issue=null, pageStart=431, pageEnd=446, url=null, language=null, rfNumber=[31], rfOrder=30, authorNames=Doychev G, Feld D, Köpf B, journalName=Proceedings of the 22nd USENIX conference on Security, refType=null, unstructuredReference=
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., articleTitle=CacheAudit: A tool for the static analysis of cache side channels, refAbstract=null), Reference(id=1241719315108524137, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2016, volume=null, issue=null, pageStart=53, pageEnd=70, url=null, language=null, rfNumber=[32], rfOrder=31, authorNames=Almeida J B, Barbosa M, Barthe G, journalName=Proceedings of the USENIX Security Symposium, refType=null, unstructuredReference=
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., articleTitle=Verifying constant-time implementations, refAbstract=null), Reference(id=1241719315179827307, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2017, volume=null, issue=null, pageStart=875, pageEnd=890, url=null, language=null, rfNumber=[33], rfOrder=32, authorNames=Chen J, Feng Y, Dillig I, journalName=Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, refType=null, unstructuredReference=
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., articleTitle=Precise detection of side-channel vulnerabilities using quantitative Cartesian Hoare logic, refAbstract=null), Reference(id=1241719315263713388, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2017, volume=null, issue=null, pageStart=362, pageEnd=375, url=null, language=null, rfNumber=[34], rfOrder=33, authorNames=Antonopoulos T, Gazzillo P, Hicks M, journalName=Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, refType=null, unstructuredReference=
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., articleTitle=Decomposition instead of self-composition for proving the absence of timing channels, refAbstract=null), Reference(id=1241719315360182383, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2018, volume=null, issue=null, pageStart=136, pageEnd=156, url=null, language=null, rfNumber=[35], rfOrder=34, authorNames=Yang W K, Vizel Y, Subramanyan P, journalName=Chockler H, Weissenbacher G.Proceedings of the 30th International Conference on Computer Aided Verification, refType=null, unstructuredReference=
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., articleTitle=Lazy self-composition for security verification, refAbstract=null), Reference(id=1241719315427291249, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2018, volume=null, issue=null, pageStart=15, pageEnd=26, url=null, language=null, rfNumber=[36], rfOrder=35, authorNames=Wu M, Guo S J, Schaumont P, journalName=Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, refType=null, unstructuredReference=
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., articleTitle=Eliminating timing side-channel leaks using program repair, refAbstract=null), Reference(id=1241719315498594419, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=174, pageEnd=189, url=null, language=null, rfNumber=[37], rfOrder=36, authorNames=Cauligi S, Soeller G, Johannesmeyer B, journalName=Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, refType=null, unstructuredReference=
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., articleTitle=FaCT: A DSL for timing-sensitive computation, refAbstract=null), Reference(id=1241719315590869109, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=10.1145/3290390, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[38], rfOrder=37, authorNames=Watt C, Renner J, Popescu N, journalName=Proceedings of the ACM on Programming Languages, refType=null, unstructuredReference=
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., articleTitle=CT-wasm: Type-driven secure cryptography for the web ecosystem, refAbstract=null), Reference(id=1241719315678949495, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=802, pageEnd=815, url=null, language=null, rfNumber=[39], rfOrder=38, authorNames=Wu M, Wang C, journalName=Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, refType=null, unstructuredReference=
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., articleTitle=Abstract interpretation under speculative execution, refAbstract=null), Reference(id=1241719315746058361, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=1235, pageEnd=1247, url=null, language=null, rfNumber=[40], rfOrder=39, authorNames=Guo S J, Chen Y Q, Li P, journalName=Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, refType=null, unstructuredReference=
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., articleTitle=SpecuSym: Speculative symbolic execution for cache timing leak detection, refAbstract=null), Reference(id=1241719315817361531, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=10.1145/3385897, pmid=null, pmcid=null, year=2020, volume=29, issue=3, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[41], rfOrder=40, authorNames=Wang G H, Chattopadhyay S, Biswas A K, journalName=ACM Transactions on Software Engineering and Methodology, refType=null, unstructuredReference=
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., articleTitle=KLEESpectre: Detecting information leakage through speculative cache attacks via symbolic execution, refAbstract=null), Reference(id=1241719315888664700, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=1021, pageEnd=1038, url=null, language=null, rfNumber=[42], rfOrder=41, authorNames=Daniel L A, Bardin S, Rezk T, journalName=Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2020, refType=null, unstructuredReference=
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., articleTitle=Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level, refAbstract=null), Reference(id=1241719315955773566, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2018, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[43], rfOrder=42, authorNames=Guarnieri M, Köpf B, Morales J F, journalName=Spectector: Principled detection of speculative information flows[DB/OL]. arXiv preprint:1812.08639, refType=null, unstructuredReference=
Guarnieri M,
Köpf B,
Morales J F, et al.
Spectector: Principled detection of speculative information flows[DB/OL]. arXiv preprint:1812.08639,
2018., articleTitle=null, refAbstract=null), Reference(id=1241719316035465344, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=913, pageEnd=926, url=null, language=null, rfNumber=[44], rfOrder=43, authorNames=Cauligi S, Disselkoen C, Gleissenthall K V, journalName=Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, refType=null, unstructuredReference=
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., articleTitle=Constant-time foundations for the new spectre era, refAbstract=null), Reference(id=1241719316115157122, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=10.1109/TSE.2019.2953709, pmid=null, pmcid=null, year=2021, volume=47, issue=11, pageStart=2504, pageEnd=2519, url=https://ieeexplore.ieee.org/document/8902081/, language=null, rfNumber=[45], rfOrder=44, authorNames=Wang G H, Chattopadhyay S, Gotovchits I, journalName=IEEE Transactions on Software Engineering, refType=null, unstructuredReference=
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., articleTitle=oo7: Low-overhead defense against spectre attacks via program analysis, refAbstract=null), Reference(id=1241719316173877380, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=10.1145/3434330, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[46], rfOrder=45, authorNames=Vassena M, Disselkoen C, Von Gleissenthall K, journalName=Proceedings of the ACM on Programming Languages, refType=null, unstructuredReference=
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., articleTitle=Automatically eliminating speculative leaks from cryptographic code with blade, refAbstract=null), Reference(id=1241719316266152070, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[47], rfOrder=46, authorNames=Daniel L A, Bardin S, Rezk T, journalName=Proceedings 2021 Network and Distributed System Security Symposium, refType=null, unstructuredReference=
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., articleTitle=Hunting the haunter—Efficient relational symbolic execution for spectre with haunted RelSE, refAbstract=null), Reference(id=1241719316333260936, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=83, pageEnd=96, url=null, language=null, rfNumber=[48], rfOrder=47, authorNames=Shivakumar B A, Barthe G, Grégoire B, journalName=Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, refType=null, unstructuredReference=
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., articleTitle=Enforcing fine-grained constant-time policies, refAbstract=null), Reference(id=1241719316412952714, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=872, pageEnd=884, url=null, language=null, rfNumber=[49], rfOrder=48, authorNames=Qin Q, Jiyang J, Song F, journalName=Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, refType=null, unstructuredReference=
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., articleTitle=DeJITLeak: Eliminating JIT-induced timing side-channel leaks, refAbstract=null), Reference(id=1241719316471672972, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=10.1145/2685616, pmid=null, pmcid=null, year=2014, volume=24, issue=2, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[50], rfOrder=49, authorNames=Eldib H, Wang C, Schaumont P, journalName=ACM Transactions on Software Engineering and Methodology, refType=null, unstructuredReference=
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., articleTitle=Formal verification of software countermeasures against side-channel attacks, refAbstract=null), Reference(id=1241719316542976142, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2014, volume=null, issue=null, pageStart=114, pageEnd=130, url=null, language=null, rfNumber=[51], rfOrder=50, authorNames=Eldib H, Wang C, journalName=Biere A, Bloem R.Proceedings of the 26th International Conference on Computer Aided Verification, refType=null, unstructuredReference=
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., articleTitle=Synthesis of masking countermeasures against side channel attacks, refAbstract=null), Reference(id=1241719316622667920, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2014, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[52], rfOrder=51, authorNames=Eldib H, Wang C, Taha M, journalName=Proceedings of the 2014 51st ACM/EDAC/IEEE Design Automation Conference (DAC), refType=null, unstructuredReference=
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., articleTitle=QMS: Evaluating the side-channel resistance of masked software from source code, refAbstract=null), Reference(id=1241719316689776786, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2015, volume=null, issue=null, pageStart=457, pageEnd=485, url=null, language=null, rfNumber=[53], rfOrder=52, authorNames=Barthe G, Belaïd S, Dupressoir F, journalName=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, refType=null, unstructuredReference=
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., articleTitle=Verified proofs of higher-order masking, refAbstract=null), Reference(id=1241719316769468564, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2016, volume=null, issue=null, pageStart=116, pageEnd=129, url=null, language=null, rfNumber=[54], rfOrder=53, authorNames=Barthe G, Belaïd S, Dupressoir F, journalName=Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, refType=null, unstructuredReference=
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., articleTitle=Strong non-interference and type-directed higher-order masking, refAbstract=null), Reference(id=1241719316849160342, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2017, volume=null, issue=null, pageStart=277, pageEnd=297, url=null, language=null, rfNumber=[55], rfOrder=54, authorNames=Blot A, Yamamoto M, Terauchi T, journalName=Maffei M, Ryan M.Proceedings of the 6th International Conference on Principles of Security and Trust. Berlin, refType=null, unstructuredReference=
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., articleTitle=Compositional synthesis of leakage resilient programs, refAbstract=null), Reference(id=1241719316912074904, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2018, volume=null, issue=null, pageStart=65, pageEnd=82, url=null, language=null, rfNumber=[56], rfOrder=55, authorNames=Coron J S, journalName=Preneel B, Vercauteren F. Proceedings of the 16th International Conference on Applied Cryptography and Network Security, refType=null, unstructuredReference=
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., articleTitle=Formal verification of side-channel countermeasures via elementary circuit transformations, refAbstract=null), Reference(id=1241719316979183770, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2018, volume=null, issue=null, pageStart=321, pageEnd=353, url=null, language=null, rfNumber=[57], rfOrder=56, authorNames=Bloem R, Gross H, Iusupov R, journalName=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, refType=null, unstructuredReference=
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., articleTitle=Formal verification of masked hardware implementations in the presence of glitches, refAbstract=null), Reference(id=1241719318040342684, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2018, volume=null, issue=null, pageStart=157, pageEnd=177, url=null, language=null, rfNumber=[58], rfOrder=57, authorNames=Zhang J, Gao P F, Song F, journalName=Chockler H, Weissenbacher G. Proceedings of the 30th International Conference on Computer Aided Verification, refType=null, unstructuredReference=
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., articleTitle=SCInfer: Refinement-based verification of software countermeasures against side-channel attacks, refAbstract=null), Reference(id=1241719318111645854, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=10.1145/3330392, pmid=null, pmcid=null, year=2019, volume=28, issue=3, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[59], rfOrder=58, authorNames=Gao P F, Zhang J, Song F, journalName=ACM Transactions on Software Engineering and Methodology, refType=null, unstructuredReference=
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., articleTitle=Verifying and quantifying side-channel resistance of masked software implementations, refAbstract=null), Reference(id=1241719318170366112, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=590, pageEnd=601, url=null, language=null, rfNumber=[60], rfOrder=59, authorNames=Wang J B, Sung C, Wang C, journalName=Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, refType=null, unstructuredReference=
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., articleTitle=Mitigating power side channels during compilation, refAbstract=null), Reference(id=1241719318237474978, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=300, pageEnd=318, url=null, language=null, rfNumber=[61], rfOrder=60, authorNames=Barthe G, Belaïd S, Cassiers G, journalName=Sako K, Schneider S, Ryan P Y A. Proceedings of the 24th European Symposium on Research in Computer Security—ESORICS 2019, refType=null, unstructuredReference=
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., articleTitle=MaskVerif: Automated verification of higher-order masking in presence of physical defaults, refAbstract=null), Reference(id=1241719318321361060, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2018, volume=null, issue=null, pageStart=343, pageEnd=372, url=null, language=null, rfNumber=[62], rfOrder=61, authorNames=Belaïd S, Goudarzi D, Rivain M, journalName=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, refType=null, unstructuredReference=
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., articleTitle=Tight private circuits: Achieving probing security with the least refreshing, refAbstract=null), Reference(id=1241719318401052838, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=311, pageEnd=341, url=null, language=null, rfNumber=[63], rfOrder=62, authorNames=Belaïd S, Dagand P É, Mercadier D, journalName=Canteaut A, Ishai Y. Proceedings of the 39th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Advances in Cryptology—EUROCRYPT 2020, refType=null, unstructuredReference=
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., articleTitle=Tornado: Automatic generation of probing-secure masked bitsliced implementations, refAbstract=null), Reference(id=1241719318463967400, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=787, pageEnd=816, url=null, language=null, rfNumber=[64], rfOrder=63, authorNames=Knichel D, Sasdrich P, Moradi A, journalName=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, refType=null, unstructuredReference=
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., articleTitle=SILVER—Statistical independence and leakage verification, refAbstract=null), Reference(id=1241719318535270569, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=339, pageEnd=368, url=null, language=null, rfNumber=[65], rfOrder=64, authorNames=Belaïd S, Coron J S, Prouff E, journalName=Micciancio D, Ristenpart T. Proceedings of the 40th Annual International Cryptology Conference, Advances in Cryptology—CRYPTO 2020, refType=null, unstructuredReference=
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., articleTitle=Random probing security:Verification, composition, expansion and new constructions, refAbstract=null), Reference(id=1241719318598185130, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=10.1145/3428015, pmid=null, pmcid=null, year=2021, volume=30, issue=3, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[66], rfOrder=65, authorNames=Gao P F, Xie H Y, Song F, journalName=ACM Transactions on Software Engineering and Methodology, refType=null, unstructuredReference=
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., articleTitle=A hybrid approach to formal verification of higher-order masked arithmetic programs, refAbstract=null), Reference(id=1241719318661099691, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=10.1109/TC.2020.3022979, pmid=null, pmcid=null, year=2021, volume=70, issue=10, pageStart=1677, pageEnd=1690, url=https://ieeexplore.ieee.org/document/9190067/, language=null, rfNumber=[67], rfOrder=66, authorNames=Cassiers G, Grégoire B, Levi I, journalName=IEEE Transactions on Computers, refType=null, unstructuredReference=
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., articleTitle=Hardware private circuits: from trivial composition to full verification, refAbstract=null), Reference(id=1241719318724014252, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=2022, volume=48, issue=3, pageStart=973, pageEnd=1000, url=null, language=null, rfNumber=[68], rfOrder=67, authorNames=Gao P F, Xie H Y, Sun P, journalName=IEEE Transactions on Software Engineering, refType=null, unstructuredReference=
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., articleTitle=Formal verification of masking countermeasures for arithmetic programs, refAbstract=null), Reference(id=1241719318778540205, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=142, pageEnd=160, url=null, language=null, rfNumber=[69], rfOrder=68, authorNames=Belaïd S, Mercadier D, Rivain M, journalName=Proceedings of the 2022 IEEE Symposium on Security and Privacy (SP). Piscataway:IEEE Press, 2022, refType=null, unstructuredReference=
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., articleTitle=IronMask: Versatile verification of masking security, refAbstract=null)], funds=null, companyList=[AuthorCompany(id=1241719307537806322, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, xref=null, ext=[AuthorCompanyExt(id=1241719307546194931, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, companyId=1241719307537806322, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=School of Information Science and Technology, ShanghaiTech University, Shanghai 201210, China), AuthorCompanyExt(id=1241719307550389236, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, companyId=1241719307537806322, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=上海科技大学信息科学与技术学院，上海 201210)])], figs=[ArticleFig(id=1241719310205382671, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, label=null, caption=null, figureFileSmall=080kD8wa6VOplBuDXg7+3w==, figureFileBig=KlmYvAiQMSkE9ucgDcb59A==, tableContent=null), ArticleFig(id=1241719310264102929, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, label=图1, caption=
密码对信息安全提供的安全保障, figureFileSmall=080kD8wa6VOplBuDXg7+3w==, figureFileBig=KlmYvAiQMSkE9ucgDcb59A==, tableContent=null), ArticleFig(id=1241719310423486483, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, label=null, caption=null, figureFileSmall=uqTzIpuaj45Mt5Tzl+siRg==, figureFileBig=29jyiJjEtl7Wxf/cs6QNIw==, tableContent=null), ArticleFig(id=1241719310482206740, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, label=图2, caption=
密码应用技术体系 USB Key，Universal Serial Bus Key，通用串行总线接口的加密锁;USIM，Universal Subscriber Identity Module，全球用户识别卡。
, figureFileSmall=uqTzIpuaj45Mt5Tzl+siRg==, figureFileBig=29jyiJjEtl7Wxf/cs6QNIw==, tableContent=null), ArticleFig(id=1241719310545121301, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, label=null, caption=null, figureFileSmall=PULG2n+TcOqn5W2Wo39QoA==, figureFileBig=GcXUNPq4/OsFZSNh9aZGRQ==, tableContent=null), ArticleFig(id=1241719310633201690, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, label=图3, caption=
密码实现侧信道攻击, figureFileSmall=PULG2n+TcOqn5W2Wo39QoA==, figureFileBig=GcXUNPq4/OsFZSNh9aZGRQ==, tableContent=null), ArticleFig(id=1241719310708699166, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, label=null, caption=null, figureFileSmall=null, figureFileBig=null, tableContent=
| 验证工具和文献 | 年份 | 内存
安全 | 验证技术 | 自动化
程度 | 输入语言 | 目标语言 | 应用 |
| 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等库函数 |
), ArticleFig(id=1241719310796779554, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, label=表1, caption=
密码实现功能正确性和内存安全性形式化验证的研究进展
, figureFileSmall=null, figureFileBig=null, tableContent=
| 验证工具和文献 | 年份 | 内存
安全 | 验证技术 | 自动化
程度 | 输入语言 | 目标语言 | 应用 |
| 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等库函数 |
), ArticleFig(id=1241719310876471332, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, label=null, caption=null, figureFileSmall=null, figureFileBig=null, tableContent=
| 验证工具和文献 | 年份 | 泄漏模型 | 验证技术 | 验证精度 | 输入语言 | 目标语言 | 应用 |
| 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 |
| 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测试集 |
), ArticleFig(id=1241719310956163110, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, label=表2, caption=
密码实现时间侧信道安全性形式化验证的研究进展
, figureFileSmall=null, figureFileBig=null, tableContent=
| 验证工具和文献 | 年份 | 泄漏模型 | 验证技术 | 验证精度 | 输入语言 | 目标语言 | 应用 |
| 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 |
| 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测试集 |
), ArticleFig(id=1241719311023271978, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=EN, label=null, caption=null, figureFileSmall=null, figureFileBig=null, tableContent=
| 验证工具和文献 | 年份 | 安全
模型 | 阶数 | 可组合验证 | 验证技术 | 验证
精度 | 输入语言 | 目标语言 | 应用 |
| 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 |
| QMVERIF[68] | 2022 | ①⑥⑦ | 1 | Y | 类型系统约束求解混合验证 | ● | 算术电路 | C | Keccak, AES-Sbox |
| IronMask[69] | 2022 | ②③④⑤⑥⑧ | ≥1 | N | 高斯消元 | ◉ | 布尔电路 | Sage | 乘法器 |
), ArticleFig(id=1241719311107158060, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719284355878952, language=CN, label=表3, caption=
密码实现功耗侧信道安全性形式化验证的研究进展
, figureFileSmall=null, figureFileBig=null, tableContent=
| 验证工具和文献 | 年份 | 安全
模型 | 阶数 | 可组合验证 | 验证技术 | 验证
精度 | 输入语言 | 目标语言 | 应用 |
| 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 |
| QMVERIF[68] | 2022 | ①⑥⑦ | 1 | Y | 类型系统约束求解混合验证 | ● | 算术电路 | C | Keccak, AES-Sbox |
| IronMask[69] | 2022 | ②③④⑤⑥⑧ | ≥1 | N | 高斯消元 | ◉ | 布尔电路 | Sage | 乘法器 |
)], attaches=null, journal=Journal(id=1129340393107079197, delFlag=0, nameCn=前瞻科技, nameEn=Science and Technology Foresight, nameHistory1=null, nameHistory2=null, issn=2097-0781, eissn=, cn=10-1786/N, coden=null, periodic=2, language=CN, oaType=null, ccby=null, superviseOffice=null, ownerOffice=null, pubOffice=null, editorOffice=null, officeType=null, aims=null, clcCode=null, officeProv=null, officeCity=null, officeAddr=null, officeZip=null, officeEmail=null, officePhone=null, editDirector=null, officeDirector=null, officeDirectorPhone=null, officeStaffNum=null, officeEmpNum=null, coverPicUrl=ti95jJIJzXaf02YNe1UF2A==, journalPrice=null, startedYear=null, abbrevIsoEn=Sci Technol Fore, journalRemark=null, publicationField=null, createdTime=null, updatedTime=1757931223825, createdBy=null, updatedBy=15831073675, firstLetterCn=S, firstLetterEn=S, subjectCode=Natural Sciences, subjectName=自然科学, subjectCodeEn=Natural Sciences, subjectNameEn=null, picCn=ti95jJIJzXaf02YNe1UF2A==, picEn=cuGsq8KPhoqtfsQROuZvoQ==, jcr=null, cjcr=null, exts=[JournalExt(id=1174411930946125939, language=CN, name=前瞻科技, nameHistory1=null, nameHistory2=null, managedBy=, sponsoredBy=, publishedBy=, editorOffice=, officeProv=null, officeCity=null, officeAddr=, officeZip=, editDirector=null, officeDirector=null, officePhone=null, coverPicUrl=null, journalRemark=, submitArticleUrl=null, websiteUrl=http://www.qianzhankeji.cn/CN/2097-0781/home.shtml, createdTime=1757931223856, updatedTime=1757931223856, createdBy=15831073675, updatedBy=15831073675, submissionGuidelinesUrl=http://www.qianzhankeji.cn/CN/column/column7.shtml, submissionAuthorUrl=https://qzkjauthor.cast.org.cn/webm/, submissionEditorUrl=https://qzkjeditor.cast.org.cn/webm/, submissionReviewUrl=https://qzkjauthor.cast.org.cn/webm/, submissionCeEditorUrl=https://qzkjeditor.cast.org.cn/webm/, submissionAeEditorUrl=https://qzkjeditor.cast.org.cn/webm/, option={"copyright":""}), JournalExt(id=1174411931076149364, language=EN, name=Science and Technology Foresight, nameHistory1=null, nameHistory2=null, managedBy=, sponsoredBy=, publishedBy=, editorOffice=, officeProv=null, officeCity=null, officeAddr=, officeZip=, editDirector=null, officeDirector=null, officePhone=null, coverPicUrl=null, journalRemark=, submitArticleUrl=null, websiteUrl=http://www.qianzhankeji.cn/EN/2097-0781/home.shtml, createdTime=1757931223887, updatedTime=1757931223887, createdBy=15831073675, updatedBy=15831073675, submissionGuidelinesUrl=http://www.qianzhankeji.cn/EN/column/column7.shtml, submissionAuthorUrl=https://qzkjauthor.manuscriptcloud.com/login, submissionEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, submissionReviewUrl=https://qzkjauthor.manuscriptcloud.com/login, submissionCeEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, submissionAeEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, option={"copyright":""})], databaseList=null, tenantJournalId=1146032081894723586, websiteList=[Website(id=1148243202353652128, webName=null, webTitle=null, webDomain=null, webCopyrigh=null, webIpcNo=null, seoTitle=null, seoKeywords=null, seoDescription=null, tenantJournalId=null, journalId=1146032081894723586, journalNameCn=null, journalNameEn=null, grayFlag=null, tenantId=1146029695717560320, platformId=null, journalGroupId=null, journalGroupNameCn=null, journalGroupNameEn=null, type=1, domain=https://castjournals.cast.org.cn/joweb/qzkj/CN, language=CN, createTime=1751692112768, createBy=18614031015, updateTime=1753516254852, updateBy=18614031015, name=《前瞻科技》中文站点, tplId=1146099689490845704, title=前瞻科技, delFlag=0, indexPage=/home, props=[WebsiteProps(id=1148618977242275853, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=articleTextType, value=kx, createTime=1751781704483, updateTime=1751781704483, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977217110026, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=banner, value=null, createTime=1751781704477, updateTime=1751781704477, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977204527113, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=logo, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic?fileId=skpCN5mVIzgEJbdUXu8/8A==, createTime=1751781704474, updateTime=1751781704474, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977233887244, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=picServerUrl, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic, createTime=1751781704481, updateTime=1751781704481, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977225498635, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=staticResourcePath, value=https://castjournals.cast.org.cn/joweb/cast_kjdb_cn_619/, createTime=1751781704479, updateTime=1751781704479, creator=18614031015, updator=18614031015)]), Website(id=1155894377965830154, webName=null, webTitle=null, webDomain=null, webCopyrigh=null, webIpcNo=null, seoTitle=null, seoKeywords=null, seoDescription=null, tenantJournalId=null, journalId=1146032081894723586, journalNameCn=null, journalNameEn=null, grayFlag=null, tenantId=1146029695717560320, platformId=null, journalGroupId=null, journalGroupNameCn=null, journalGroupNameEn=null, type=1, domain=https://castjournals.cast.org.cn/joweb/qzkj/EN, language=EN, createTime=1753516295187, createBy=18614031015, updateTime=1753516295187, updateBy=18614031015, name=《前瞻科技》英文站点, tplId=1146101810881728533, title=Science and Technology Foresight, delFlag=0, indexPage=/home, props=[WebsiteProps(id=1155894740970233959, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=articleTextType, value=kx, createTime=1753516381733, updateTime=1753516381733, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740953456740, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=banner, value=null, createTime=1753516381729, updateTime=1753516381729, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740945068131, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=logo, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic?fileId=skpCN5mVIzgEJbdUXu8/8A==, createTime=1753516381727, updateTime=1753516381727, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740966039654, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=picServerUrl, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic, createTime=1753516381732, updateTime=1753516381732, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740961845349, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=staticResourcePath, value=https://castjournals.cast.org.cn/joweb/cast_kjdb_cn_619/, createTime=1753516381731, updateTime=1753516381731, creator=18614031015, updator=18614031015)])], journalTitle=前瞻科技, weixinUrl=null, journalUrl=null, iacademicId=null, status=0, seqNo=null, journalTitleEn=Science and Technology Foresight, journalPhotoCn=ti95jJIJzXaf02YNe1UF2A==, journalPhotoEn=cuGsq8KPhoqtfsQROuZvoQ==, journalFirstLetter=S, journalRecommend=null, journalNew=null, journalCollection=null, jcrJf=null, cjcrJf=null, jcrJfStr=null, cjcrJfStr=null, submissionFirstDecision=null, sciSubjectClassification=null, casSubjectClassification=null, citeScore=null, totalCitationFrequency=null, icpCode=null, psCode=null, advertisingLicenseCode=null, copyrightInformation=null, country=null, option=, provinceCode=null, provinceName=null, collectFlag=false), detailUrlCn=https://castjournals.cast.org.cn/joweb/qzkj/CN/10.3981/j.issn.2097-0781.2023.01.007, detailUrlEn=https://castjournals.cast.org.cn/joweb/qzkj/EN/10.3981/j.issn.2097-0781.2023.01.007, pdfUrlCn=https://castjournals.cast.org.cn/joweb/qzkj/CN/PDF/10.3981/j.issn.2097-0781.2023.01.007, pdfUrlEn=https://castjournals.cast.org.cn/joweb/qzkj/EN/PDF/10.3981/j.issn.2097-0781.2023.01.007, aliStartDate=null, aliEndDate=null, collectionFlag=false, citedCount=null, citedUrl=null, reference=null)
PDF Download
Full
3013
1630
Close Full
