Formal models for verifying multi-threaded recursive programs

用于验证多线程递归程序的形式化模型

• 批准号: 21700045
• 负责人: TAKATA Yoshiaki
• 金额: $ 2.33万
• 依托单位: Kochi University of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2009
• 资助国家: 日本
• 起止时间: 2009 至 2010
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-21700045/
• 关键词: 自動検証; モデル検査; 形式モデル; プッシュダウンシステム; 形式的検証; 形式言語理論; マルチスレッド

In this study, we proposed 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) was assumed as the access control model. A security specification is given in terms of information flow. We say that a program P satisfies a specification S if P is type-safe when we consider each security class in S as a type. We first defined the problem as the one to insert check statements into a given program P to obtain a program P' that is type-safe for a given specification S. This type system is sound in the sense that if a program P is type-safe for a specification S, then P has noninterference property for S. Next, the problem was shown to be co-NP-hard and we proposed a fix-point computation algorithm for solving the problem. The experimental results based on our implemented system showed that the proposed method can work within reasonable time.

在这项研究中，我们提出了一种方法，自动插入检查语句的访问控制到一个给定的递归程序根据给定的安全规范。基于历史的访问控制（HBAC）被假定为访问控制模型。从信息流的角度给出了安全规范。我们说一个程序P满足一个规范S，如果P是类型安全的，当我们考虑S中的每个安全类作为一个类型时。我们首先将问题定义为将检查语句插入到给定程序P中以获得对于给定规范S是类型安全的程序P'的问题。这个类型系统是合理的，如果程序P对于规范S是类型安全的，那么P对于规范S具有不干涉属性。其次，我们证明了该问题是co-NP-hard的，并提出了一个不动点算法来求解该问题。实验结果表明，该方法可以在合理的时间内工作。

项目成果

Automatic generation of history-based access control from information flow specification, Automated Technology for Verification and Analysis, ATVA 2010

根据信息流规范自动生成基于历史的访问控制，验证和分析自动化技术，ATVA 2010

• 发表时间: 2010
• 期刊: Lecture Notes in Computer Science Vol.6252
• 作者: Yoshiaki Takata;Hiroyuki Seki
• 通讯作者: Hiroyuki Seki

情報流仕様に基づくアクセス権検査文自動挿入法

根据信息流规范自动插入访问权限检查文本

• 发表时间: 2010
• 作者: Yoshiaki Takata;Hiroyuki Seki;高田喜朗
• 通讯作者: 高田喜朗

Automatic generation of history-based access control from information flow specification

根据信息流规范自动生成基于历史的访问控制

• 发表时间: 2010
• 期刊: 8th International Symposium on Automated Technology for Verification and Analysis
• 作者: Yoshiaki Takata;Hiroyuki Seki
• 通讯作者: Hiroyuki Seki