Stack inspection is now broadly used as dynamic access control infrastructure in such runtime environments as Java virtual machines and Common Language Runtime. However, stack inspection is not sufficient for security assurance since the stack does not retain security information on the invoked methods for which execution is finished. To solve this problem, access control models based on execution history have been proposed. This paper presents a formal model for programs with access control based on execution history, which are called HBAC programs. Their expressive power is shown to be strictly stronger than programs with stack inspection. It is also shown that the verification problem for HBAC programs is EXPTIME-complete, while the problem is solvable in polynomial time under a reasonable assumption. Finally, this paper presents a few optimization techniques used in the implementation of a verification tool for HBAC programs. The results of experiments show that the tool can verify practical HBAC programs within a reasonable time. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Wang, J., Takata, Y., & Seki, H. (2006). HBAC: A model for history-based access control and its model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4189 LNCS, pp. 263–278). Springer Verlag. https://doi.org/10.1007/11863908_17
Mendeley helps you to discover research relevant for your work.