Verified Enforcement of Stateful Information Release Policies

被引：4

作者：

Swamy, Nikhil ^{[1
]}

Hicks, Michael ^{[1
]}

机构：

[1] Univ Maryland, Dept Comp Sci, College Pk, MD 20742 USA

来源：

PLAS'08: PROCEEDINGS OF THE ACM SIGPLAN THIRD WORKSHOP ON PROGRAMMING LANGUAGES AND ANALYSIS FOR SECURITY | 2008年

关键词：

declassification; certified evaluation; state modifying policies; dependent types; affine types; singleton types;

D O I：

10.1145/1375696.1375700

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Many organizations specify information release policies to describe the terms under which sensitive information may be released to other organizations. This paper presents a new approach for ensuring that security-critical software correctly enforces its information release policy. Our approach has two parts. First, an information release policy is specified as a security automaton written in a new language called AIR. Second, we enforce an AIR policy by translating it into an API for programs written in lambda AIR, a core formalism for a functional programming language. lambda AIR uses a novel combination of dependent. affine, and singleton types to ensure that the API is used correctly. As a consequence we can certify that programs written in lambda AIR meet the requirements of the original AIR policy specification.

引用

页码：21 / 31

页数：11

共 27 条

[1] AYDEMIR B, 2008, POPL 08
[2] Expressive declassification policies and modular static enforcement
Banerjee, Anindya
Naumann, David A.
Rosenberg, Stan
[J]. PROCEEDINGS OF THE 2008 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, 2008, : 339 - +
[3] BECKER MY, 2007, LECT NOTES COMPUTER, V4734
[4] Bertot Yves, 2004, TEXT THEORET COMP S, DOI 10.1007/978-3-662-07964-5
[5] Fuzzy multi-level security : An experiment on quantified risk-adaptive access control - Extended abstract
Cheng, Pau-Chen
Rohatgi, Pankaj
Keser, Claudia
Karger, Paul A.
Wagner, Grant M.
Reninger, Angela Schuett
[J]. 2007 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, PROCEEDINGS, 2007, : 222 - +
[6] Chong S., 2004, CCS 2004 P, P198
[7] CRARY K, 1999, P 26 ACM SIGPLAN SIG, P262
[8] DeLine Robert., 2001, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, P59, DOI DOI 10.1145/381694.378811
[9] LATTICE MODEL OF SECURE INFORMATION-FLOW
DENNING, DE
[J]. COMMUNICATIONS OF THE ACM, 1976, 19 (05) : 236 - 243
[10] ERLINGSSON U, 2004, THESIS CORNELL U

← 1 2 3 →