A Formal Framework for Access Rights Analysis

A stack-based access control mechanism is to prevent untrusted codes from accessing protected resources in distributed application systems, such as Java-centric web applications and Microsoft .NET framework. Such an access control mechanism is enforced at runtime by stack inspection that inspects methods in the current call stack for granted permissions. Nowadays practiced approaches to generating policy files for an application are still manually done by developers based on domain-specific knowledges and testing, due to overwhelming technical challenges involved and engineering efforts in the automation. This paper presents a formal framework of access rights analysis for Java applications, which includes both policy generation and checking. The analysis of policy generation automatically generates access control policies for the given program that necessarily ensure the program to pass stack inspections. The analysis of policy checking takes as input a policy file and determines whether access control in the concerned domain always succeed or may fail. The answer can either help detect redundant inspection points or refine the given policies. All of our analysis algorithms are novelly designed in the framework of conditional weighted pushdown systems, and are expected to achieve a high level of precision in the literature.リサーチレポート（北陸先端科学技術大学院大学情報科学研究科