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


IEICE TRANSACTIONS on Information and Systems   Vol.E97-D   No.5   pp.1149-1159
Publication Date: 2014/05/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E97.D.1149
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)>>
Buy this Article

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.