Verification of a Cryptographic Primitive: SHA-256

被引：92
作者：
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
    Backes, Michael
    Barthe, Gilles
    Berg, Matthias
    Gregoire, Benjamin
    Kunz, Cesar
    Skoruppa, Malte
    Beguelin, Santiago Zanella
    [J]. 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