Verification of a Cryptographic Primitive: SHA-256

被引：97
作者：
Appel, Andrew W. [1 ]
机构：
[1] Princeton Univ, Dept Comp Sci, Princeton, NJ 08540 USA
来源：
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 2015年 / 37卷 / 02期
关键词：
Verification; Cryptography; SECURITY; PROOFS; NMAC;
D O I：
10.1145/2701415
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This article presents a full formal machine-checked verification of a C program: the OpenSSL implementation of SHA-256. This is an interactive proof of functional correctness in the Coq proof assistant, using the Verifiable C program logic. Verifiable C is a separation logic for the C language, proved sound with respect to the operational semantics for C, connected to the CompCert verified optimizing C compiler.
引用
收藏
页数：31
相关论文
共 29 条
[21]  
Schneier Bruce, 2013, CRYPTO GRAM NEWSLETT
[22]  
Schneier Bruce, 1999, CRYPTO GRAM NEWSLETT
[23]   Translation Validation for a Verified OS Kernel [J].
Sewell, Thomas ;
Myreen, Magnus ;
Klein, Gerwin .
ACM SIGPLAN NOTICES, 2013, 48 (06) :471-481
[24]  
SMITH E. W., 2008, FORMAL METHODS COMPU, P1
[25]   REFLECTIONS ON TRUSTING TRUST [J].
THOMPSON, K .
COMMUNICATIONS OF THE ACM, 1984, 27 (08) :761-763
[26]  
Toma D, 2005, LECT NOTES COMPUT SC, V3603, P326
[27]   Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior [J].
Wang, Xi ;
Zeldovich, Nickolai ;
Kaashoek, M. Frans ;
Solar-Lezama, Armando .
SOSP'13: PROCEEDINGS OF THE TWENTY-FOURTH ACM SYMPOSIUM ON OPERATING SYSTEMS PRINCIPLES, 2013, :260-275
[28]  
Wu Dinghao., 2003, Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, PPDP'03, P264
[29]  
Yang Xuejun, 2012, ACM SIGPLAN C PROGR, V47, P283
123