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 条

[1]

Affeldt R, 2014, J FORMALIZ REASON, V7, P63

[2] On construction of a library of formally verified low-level arithmetic functions [J].