An Accurate Type System for Information Flow in Presence of Arrays

被引：0

作者：

Fratani, Severine ^{[1
]}

Talbot, Jean-Marc ^{[1
]}

机构：

[1] Univ Provence, CNRS, UMR6166, Univ Mediterranee,Lab Informat Fondamentale Marse, Marseille, France

来源：

FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS | 2011年 / 6722卷

关键词：

CERTIFICATION; VERIFICATION; PROGRAMS; TOOL;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Secure information flow analysis aims to check that the execution of a program does not reveal information about secret data manipulated by this program. In this paper, we consider programs dealing with arrays; unlike most of existing works, we will not assume that arrays are homogeneous in terms of security levels. Some part of an array can be declared as secret whereas another part is public. Based on a pre-computed approximation of integer variables (serving as indices for arrays), we devise a type system such that typed programs do not leak unauthorized information. Soundness of our type system is proved by a non-interference theorem.

引用

页码：153 / 167

页数：15

共 17 条

[1] Amtoft T, 2010, LECT NOTES COMPUT SC, V6012, P43, DOI 10.1007/978-3-642-11957-6_4
[2] Annichini A, 2001, LECT NOTES COMPUT SC, V2102, P368
[3] [Anonymous], 2006, USA, DOI DOI 10.1145/1180405.1180417
[4] [Anonymous], 1999, P 26 ACM SIGPLAN SIG
[5] Bardin S, 2003, LECT NOTES COMPUT SC, V2725, P118
[6] Bonelli E, 2006, LECT NOTES COMPUT SC, V3956, P37
[7] Lenient array operations for practical secure information flow
Deng, ZY
Smith, G
[J]. 17TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2004, : 115 - 124
[8] LATTICE MODEL OF SECURE INFORMATION-FLOW
DENNING, DE
[J]. COMMUNICATIONS OF THE ACM, 1976, 19 (05) : 236 - 243
[9] CERTIFICATION OF PROGRAMS FOR SECURE INFORMATION-FLOW
DENNING, DE
DENNING, PJ
[J]. COMMUNICATIONS OF THE ACM, 1977, 20 (07) : 504 - 513
[10] Genaim S, 2005, LECT NOTES COMPUT SC, V3385, P346

← 1 2 →