请问是否有论文或组织对密码学原语进行形式化验证

[lovelxc]

如题，许多学者对openssl，boringssl之类的密码学实现进行了原语级别的形式化的验证，那么现有的工作是否对tongsuo进行了这方面的测试呢？

[InfoHunter]

暂无。您这边是否有相关建议？

[lovelxc]

感谢您的及时回复！ 基于我个人浅显的视角，我所知的密码学程序验证手段（非协议级别而是具体到实现程序）就是 fuzzing test 以及提取中间语言进行形式化验证。但就我所阅读的一些文章，似乎像是tongsuo，gmssl一类的国产密码库并未受到相关研究人员的重视。

我刚刚大概看了一下tongsuo的相关实现，发现原语级的代码似乎继承自openssl，那么对原语形式化验证似乎就不是特别重要（安全性来自openssl）

[johnshajiang]

@lovelxc

我所知的密码学程序验证手段（非协议级别而是具体到实现程序）就是 fuzzing test 以及提取中间语言进行形式化验证

你能否了解到有针对国密的fuzzing test？ 关于“提取中间语言进行形式化验证”，你是否指的像CodeQL这类的工具？

[lovelxc]

@lovelxc

我所知的密码学程序验证手段（非协议级别而是具体到实现程序）就是 fuzzing test 以及提取中间语言进行形式化验证

你能否了解到有针对国密的fuzzing test？ 关于“提取中间语言进行形式化验证”，你是否指的像CodeQL这类的工具？

我了解的形式化验证工具应该是这种，里面有该工具的相关论文。我似乎没看到有专门针对国密实现进行fuzzing test的，而且用fuzzing对密码学实现进行测试的论文似乎也不多，不确定是不是效果不好所导致的