様相論理に基づいたプログラム解析手法の研究

基于模态逻辑的程序分析方法研究

• 批准号: 15700011
• 负责人: 五十嵐 淳
• 金额: $ 1.79万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2003
• 资助国家: 日本
• 起止时间: 2003 至 2005
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15700011/
• 关键词: 情報流解析; 様相論理; 非干渉性; 型システム; 論理関係; メタプログラミング; 直観主義; 不干渉性; 線形時間時相論理

本研究の主な目的は,様々なプログラム解析を統一的に扱える枠組みを,様相論理という論理体系を元にして開発し,実際のプログラミング言語の解析のための型システムとして応用することにある.本年度は,昨年度まで研究を行ってきた様相論理体系に基づく情報流解析の枠組に関する考察と,論理関係を用いた非干渉性定理の一般化を行った.非干渉性とは,秘匿性の低い計算結果は,秘匿性の高い入力に依存しないこと,すなわち,秘匿性の高い入力の情報が1ビットたりとも漏洩していなことを示す性質であり,情報流解析の正当性として用いられている.従来の多くの研究では,入力と出力に関しては,整数などの基本的データ型に限って非干渉性が考察されてきた.我々の研究では,プログラムの等しさを論理関係というプログラム意味論の分野で使われている技法を用いて定式化することにより,基本的データだけではなく,関数値などの高階なデータ型に関しても適用可能な形に,非干渉性定理を一般化し,それを証明することに成功した.またこの結果から昨年まで行ってきたDCCという別の情報流解析の枠組との比較についても,両者は,比較不可能(どちらも相手よりも勝っている部分がある)という結論が出た.今後は両者の長所を統合したような,より一般的な情報流解析の枠組を目指すことが望まれる.

The main purpose of this study is to develop a unified logic system for speech analysis and application. This year, we will study the basic information flow analysis and generalization of logical relations. Non-interference, secrecy and low middle calculation results, secrecy and high middle penetration of the information is dependent on the information, secrecy and high middle penetration of the information is not the same, information flow analysis legitimacy is not the same. In recent years, many studies have been conducted on the relationship between input force and output force, integer and basic data type, non-interference and non-interference. In this paper, we study the logical relationship between the class and the class, and generalize and prove the theory of non-interference by using the technique of formalizing the basic class and the high order class. The result of the analysis of information flow in different groups and comparisons is that it is impossible to compare the results of the analysis. In the future, we hope to integrate the strengths of experts and provide a comprehensive set of general information flow analysis.

项目成果

様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明

基于模态类型的信息流分析中非相干逻辑关系的概括与证明

• 发表时间: 2006
• 期刊: 第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)オンライン論文集
• 作者: 四熊尚方;五十嵐淳
• 通讯作者: 五十嵐淳

Masahiko Sato: "Calculi of Meta-variables"Proceedings of CSL'03, LNCS. 2803. 484-497 (2003)

Masahiko Sato：“元变量的计算”CSL03 论文集，LNCS。

例外機構を備えた言語のための資源使用法解析

具有异常机制的语言的资源使用分析

• 发表时间: 2005
• 期刊: PPL2005予稿集
• 作者: Futoshi Iwama;四熊 尚方;湯瀬 芳洋;岩間 太
• 通讯作者: 岩間 太

Atushi Igarashi: "A Generic Type System for the Pi-Calculus"Theoretical Computer Science. 311・1-3. 121-163 (2004)

Atushi Igarashi：“Pi 演算的通用类型系统”理论计算机科学 311・1-163（2004）。

Resource Usage Analysis for a Functional Language with Exceptions

带有异常的函数式语言的资源使用分析

• 发表时间: 2006
• 期刊: Proceedings of ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation(PEPM'06)
• 作者: Futoshi Iwama;Atsushi Igarashi;Naoki Kobayashi
• 通讯作者: Naoki Kobayashi