SpecCert: Specifying and Verifying Hardware-Based Security Enforcement

被引：3

作者：

Letan, Thomas ^{[1
,2
]}

Chifflier, Pierre ^{[1
]}

Hiet, Guillaume ^{[2
]}

Neron, Pierre ^{[1
]}

Morin, Benjamin ^{[1
]}

机构：

[1] French Network Informat Secur Agcy ANSSI, Paris, France

[2] Cent Supelec, IRISA, CIDRE Inria, Rennes, France

来源：

FM 2016: FORMAL METHODS | 2016年 / 9995卷

关键词：

D O I：

10.1007/978-3-319-48989-6_30

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Over time, hardware designs have constantly grown in complexity and modern platforms involve multiple interconnected hardware components. During the last decade, several vulnerability disclosures have proven that trust in hardware can be misplaced. In this article, we give a formal definition of Hardware-based Security Enforcement (HSE) mechanisms, a class of security enforcement mechanisms such that a software component relies on the underlying hardware platform to enforce a security policy. We then model a subset of a x86-based hardware platform specifications and we prove the soundness of a realistic HSE mechanism within this model using Coq, a proof assistant system.

引用

页码：496 / 512

页数：17

共 27 条

[1]

Barthe Gilles, 2011, FM 2011: Formal Methods. Proceedings 17th International Symposium on Formal Methods, P231, DOI 10.1007/978-3-642-21437-0_19

[2] System-level Non-interference for Constant-time Cryptography [J].

Barthe, Gilles ;

Betarte, Gustavo ;

Diego Campo, Juan ;

Luna, Carlos ;

Pichardie, David .

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

[3] Cache-leakage resilient OS isolation in an idealized model of virtualization [J].

Barthe, Gilles ;

Betarte, Gustavo ;

Campo, Juan Diego ;

Luna, Carlos .

2012 IEEE 25TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2012, :186-197

[4] Enforceable Security Policies Revisited [J].

Basin, David ;

Juge, Vincent ;

Klaedtke, Felix ;

Zalinescu, Eugen .

ACM TRANSACTIONS ON INFORMATION AND SYSTEM SECURITY, 2013, 16 (01)

[5]

Bulygin Yuriy., 2014, Summary of attacks against BIOS and secure boot

[6]

DOMAS C., 2015, BLACKHAT US

[7]

Drzevitzky S., 2010, Proceedings 2010 International Conference on Field Programmable Logic and Applications (FPL 2010), P255, DOI 10.1109/FPL.2010.59

[8]

Duflot L., 2009, Getting into the SMRAM: SMM reloaded

[9]

Guo XL, 2016, PROCEEDINGS OF THE 2016 IEEE INTERNATIONAL SYMPOSIUM ON HARDWARE ORIENTED SECURITY AND TRUST (HOST), P124, DOI 10.1109/HST.2016.7495569

[10]

Intel, 2015, INT TRUST EX TECHN I

← 1 2 3 →