A Formal Verification of a Subset of Information-Based Access Control Based on Extended Weighted Pushdown System

被引：0

作者：

Lamilla Alvarez, Pablo ^{[1
]}

Takata, Yoshiaki ^{[1
]}

机构：

[1] Kochi Univ Technol, Kami 7828502, Japan

来源：

IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS | 2014年 / E97D卷 / 05期

关键词：

weighted pushdown systems; access control; model checking;

D O I：

10.1587/transinf.E97.D.1149

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Information-Based Access Control (IBAC) has been proposed as an improvement to History-Based Access Control (HBAC) model. In modern component-based systems, these access control models verify that all the code responsible for a security-sensitive operation is sufficiently authorized to execute that operation. The HBAC model, although safe, may incorrectly prevent the execution of operations that should be executed. The IBAC has been shown to be more precise than HBAC maintaining its safety level while allowing sufficiently authorized operations to be executed. However the verification problem of IBAC program has not been discussed. This paper presents a formal model for IBAC programs based on extended weighted pushdown systems (EWPDS). The mapping process between the IBAC original semantics and the EWPDS structure is described. Moreover, the verification problem for IBAC programs is discussed and several typical IBAC program examples using our model are implemented.

引用

页码：1149 / 1159

页数：11

共 14 条

[1] ABADI M, 2003, P 11 NETW DISTR SYST
[2] Banerjee A., 2004, LNCS, V3362, P27
[3] Cong Sun, 2009, 2009 Symposia and Workshops on Ubiquitous, Autonomic and Trusted Computing in conjunction with the UIC 2009 and ATC 2009 Conferences, P586, DOI 10.1109/UIC-ATC.2009.44
[4] Gong L, 1997, PROCEEDINGS OF THE USENIX SYMPOSIUM ON INTERNET TECHNOLOGIES AND SYSTEMS, P103
[5] He Y., 2009, MULTICORE ENABLING B
[6] Jha S, 2006, LECT NOTES COMPUT SC, V3920, P1
[7] KIDD N, 2008, WALI A C LIB WEIGHTE
[8] Lal A, 2005, LECT NOTES COMPUT SC, V3576, P434
[9] Lind-Nielsen J., 2004, DUBBY BINARY DECISIO
[10] Beyond stack inspection: A unified access-control and information-flow security model
Pistoia, Marco
Banerjee, Anindya
Naumann, David A.
[J]. 2007 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, PROCEEDINGS, 2007, : 149 - +

← 1 2 →