機械語コードおよびコード生成のための論理学的基礎の研究

2001 年度 実績報告書

• 研究課題/領域番号: 12680345
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 大堀 淳 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (60252532)
• キーワード: 機械語コード / 論理学 / コンパイル / 逆コンパイル / 型理論

研究概要

本研究の目的は,論理学における証明論の枠組を用いて,現実のコンピュータの機械語コードに論理学的解釈を与えることである.昨年度に引き続き研究を行い,所期の成果をあげることができた.研究実績の概要は以下の通りである.
1.機械語コードの解析の基礎の確立
機械語コードを静的に解析し,それと等価なより高水準の論理体型へ変換する方式を確立し,その成果を2002年度のEuropean Symposium on Programmingにて発表した.
2.機械語解析における論理学型理論の関係の解明
型理論的方法によって機械語の解析の研究を行っているAran Mycroftと共同で,本研究における論理学的方法と型理論との関係を解明し,2002年度のIEEE WCRE Workshop of Decompilation Techniqueにて発表した.
3.JAVAバイトコードの解析の基礎の確立
昨年度までの成果である機械語コードの論理学を,現実に広く使用されているJAVAバィトコードに応用し,その論理学的基礎を確立した.具体的には,JAVAバイトコードプログラムに対する証明システムを定義し,JAVAバイトコードに対するCurry-Howard対応を確立した.これによって,JAVAのバイトコードの検証が型推論の枠組みで行えることを確立した.この成果は,現在国際会議に投稿中である.

研究成果

• [文献書誌] S.Hashimoto, A.Ohori: "A Typed Context Calculus"Theoretical Computer Science. 266・1-2. 249-272 (2001)
• [文献書誌] S.Katsumata, A.Ohori: "Proof-Directed De-Compilation of Low-Level Code"Proc. European Symposium on Programming, Lecture Notes in Computer Science. 2028. 352-366 (2001)
• [文献書誌] A.Mycroft, A.Ohori, S.Katsumata: "Comparing Type-Based and Proof-Based Decompilation"Proceedings of IEEE WCR Workshop of Decompilation Technique, IEEE Press. (2001)