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 条
[1]  
Almeida J.B., 2013, P 2013 ACM SIGSAC C, P1217, DOI 10.1145/2508859.2516652
[2]  
[Anonymous], 1979, LECT NOTES COMPUTER
[3]  
[Anonymous], 2014, WASHINGTON POST
[4]  
Appel A.W., 2014, PROGRAM LOGICS CERTI
[5]  
Armand Michael, 2011, P 1 INT C CERT PROGR
[6]   Verified Security of Merkle-Damgard [J].
Backes, Michael ;
Barthe, Gilles ;
Berg, Matthias ;
Gregoire, Benjamin ;
Kunz, Cesar ;
Skoruppa, Malte ;
Beguelin, Santiago Zanella .
2012 IEEE 25TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2012, :354-368
[7]  
Barthe Gilles, 2012, Interactive Theorem Proving. Proceedings of the Third International Conference, ITP 2012, P11, DOI 10.1007/978-3-642-32347-8_2
[8]  
Bellare M., 1996, Advances in Cryptology - CRYPTO'96. 16th Annual International Cryptology Conference. Proceedings, P1
[9]  
Bellare M, 2006, LECT NOTES COMPUT SC, V4117, P602
[10]  
Besson Frederic, 2011, P 1 INT C CERT PROGR
123