For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
A Formal Verification of a Subset of Information-Based Access Control Based on Extended Weighted Pushdown System
Pablo LAMILLA ALVAREZ Yoshiaki TAKATA
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2014/05/01
Online ISSN: 1745-1361
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Formal Verification
weighted pushdown systems, access control, model checking,
Full Text: PDF(886.3KB)>>
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.