Automatic Generation of History-Based Access Control from Information Flow Specification

This paper proposes a method for automatically inserting check statements for access control into a given recursive program according to a given security specification. A history-based access control (HBAC) is assumed as the access control model. A security specification is given in terms of information flow. We say that a program satisfies a specification if is type-safe when we consider each security class in as a type. We first define the problem as the one to insert check statements into a given program to obtain a program that is type-safe for a given specification . This type system is sound in the sense that if a program is type-safe for a specification , then has noninterference property for . Next, the problem is shown to be co-NP-hard and we propose an algorithm for solving the problem. The paper also reports experimental results based on our implemented system and shows that the proposed method can work within reasonable time.

• Type: Conference
• Year: 2010
• Where: ATVA
• Authors: Yoshiaki Takata, Hiroyuki Seki
• Keywords: Access Control, ATVA 2010, Hardware, Security Specification, Specification