A Verified Information-Flow Architecture

被引：34

作者：

de Amorim, Arthur Azevedo ^{[1
]}

Collins, Nathan ^{[2
]}

DeHon, Andre ^{[1
]}

Demange, Delphine ^{[1
]}

Hritcu, Catalin ^{[1
,3
]}

Pichardie, David ^{[3
,4
]}

Pierce, Benjamin C. ^{[1
]}

Pollack, Randy ^{[4
]}

Tolmach, Andrew ^{[2
]}

机构：

[1] Univ Penn, Philadelphia, PA 19104 USA

[2] Portland State Univ, Portland, OR 97207 USA

[3] INRIA, Paris, France

[4] Harvard Univ, Cambridge, MA 02138 USA

来源：

ACM SIGPLAN NOTICES | 2014年 / 49卷 / 01期

关键词：

security; clean-slate design; tagged architecture; information-flow control; formal verification; refinement;

D O I：

10.1145/2535838.2535839

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to control information flow in SAFE and an end-to-end proof of noninterference for this model.

引用

页码：165 / 178

页数：14