Verified correctness and security of OpenSSL HMAC

被引：0

作者：

Beringer, Lennart ^{[1
]}

Petcher, Adam ^{[2
,3
]}

Ye, Katherine Q. ^{[1
]}

Appel, Andrew W. ^{[1
]}

机构：

[1] Princeton Univ, Princeton, NJ 08544 USA

[2] Harvard Univ, Cambridge, MA 02138 USA

[3] MIT, Lincoln Lab, Cambridge, MA 02139 USA

来源：

PROCEEDINGS OF THE 24TH USENIX SECURITY SYMPOSIUM | 2015年

关键词：

FORMAL VERIFICATION; PROOF;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We have proved, with machine-checked proofs in Coq, that an OpenSSL implementation of HMAC with SHA-256 correctly implements its FIPS functional specification and that its functional specification guarantees the expected cryptographic properties. This is the first machine-checked cryptographic proof that combines a source-program implementation proof, a compiler-correctness proof, and a cryptographic-security proof, with no gaps at the specification interfaces. The verification was done using three systems within the Coq proof assistant: the Foundational Cryptography Framework, to verify crypto properties of functional specs; the Verified Software Toolchain, to verify C programs w.r.t. functional specs; and CompCert, for verified compilation of C to assembly language.

引用

页码：207 / 221

页数：15

共 41 条

[21] A proof of GMP square root [J].

Bertot, Y ;

Magaud, N ;

Zimmermann, P .

JOURNAL OF AUTOMATED REASONING, 2002, 29 (3-4) :225-252

[22] Implementing TLS with Verified Cryptographic Security [J].

Bhargavan, Karthikeyan ;

Fournet, Cedric ;

Kohlweiss, Markulf ;

Pironti, Alfredo ;

Strub, Pierre-Yves .

2013 IEEE SYMPOSIUM ON SECURITY AND PRIVACY (SP), 2013, :445-459

[23] A Computationally Sound Mechanized Prover for Security Protocols [J].

Blanchet, Bruno .

IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING, 2008, 5 (04) :193-207

[24]

Cadé D, 2013, LECT NOTES COMPUT SC, V7796, P63, DOI 10.1007/978-3-642-36830-1_4

[25] Verifying Curve25519 Software [J].

Chen, Yu-Fang ;

Hsu, Chang-Hong ;

Lin, Hsin-Hung ;

Schwabe, Peter ;

Tsai, Ming-Hsien ;

Wang, Bow-Yaw ;

Yang, Bo-Yin ;

Yang, Shang-Yi .

CCS'14: PROCEEDINGS OF THE 21ST ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, 2014, :299-309

[26]

Erkok Levent, 2009, Proceedings of the 2009 9th International Conference Formal Methods in Computer-Aided Design (FMCAD), P188, DOI 10.1109/FMCAD.2009.5351121

[27] Verification of non-functional programs using interpretations in type theory [J].

Filliâtre, JC .

JOURNAL OF FUNCTIONAL PROGRAMMING, 2003, 13 :709-745

[28]

Gu L., 2011, P 2 AS PAC WORKSH SY, P3

[29]

HALEVI S, 2005, PLAUSIBLE APPROACH C

[30] AN AXIOMATIC BASIS FOR COMPUTER PROGRAMMING [J].

HOARE, CAR .

COMMUNICATIONS OF THE ACM, 1969, 12 (10) :576-&

← 1 2 3 4 5 →