例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム(ディペンダブルコンピューティング)
スポンサーリンク
概要
- 論文の詳細を見る
本論文では,例外処理機能をもつオブジェクト指向プログラムの安全性を情報流解析に基づいて検証するための型システムを提案する.例外処理による情報流は,スローされる例外とそれを捕そくする箇所に依存して変化する.この情報流を解析するためには,プログラム中の各文についてどの例外からの制御依存が存在するか把握しなければならない.我々は文がスローし得る例外の集合と文に出現する情報流のあるデータの機密度からなる安全型を導入する.この安全型に基づいて従来の型システムを拡張し,本型システムが非干渉性に対し健全であることを示す.健全性により型付け可能なプログラムは機密データを外部に漏えいしないことが保証される.
- 社団法人電子情報通信学会の論文
- 2008-03-01
著者
-
桑原 寛明
立命館大学情報理工学部
-
山本 晋一郎
愛知県立大学情報科学部
-
酒井 正彦
名古屋大学大学院情報科学研究科
-
西田 直樹
名古屋大学大学院情報科学研究科
-
坂部 俊樹
名古屋大学大学院情報科学研究科
-
草刈 圭一朗
名古屋大学大学院情報科学研究科
-
黒川 翔
(株)デンソー
-
山本 晋一郎
愛知県立大学大学
-
山本 晋一郎
愛知県立大学
-
草刈 圭一朗
名古屋大学 大学院情報科学研究科
-
酒井 正彦
名古屋大学
-
桑原 寛明
立命館大学
-
坂部 俊樹
名古屋大学大学院 情報科学研究科
-
西田 直樹
名古屋大学大学院 情報科学研究科
-
坂部 俊樹
名古屋大学 大学院情報科学研究科
-
西田 直樹
名古屋大学 大学院情報科学研究科
関連論文
- 基本対称関数に基づく節をもつCNF論理式の充足可能性判定(計算論,計算モデル)
- 拡張可能ソフトウェアの動作情報を用いたプラグイン開発支援(開発支援(学生セッション))
- 3K-5 タスク分割によるCell用の自動並列化コンパイラの開発(チップマルチプロセッサと並列化技術,学生セッション,アーキテクチャ)
- ウインターワークショップ2008・イン・道後開催報告
- 4K-2 条件分岐のSIMD化手法のCellへの適用(HPCと高速化,学生セッション,アーキテクチャ)
- ビットエラー通信路におけるスケーラブルCANの動作解析
- 条件付き等式の変換に基づくプログラム生成 (ソフトウェアサイエンス)
- 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について (ソフトウェアサイエンス)
- シャローな依存対から構成される項書換え系の停止性の決定可能性
- 基本対称関数を付加したCNF論理式の充足可能性判定
- 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序
- プレスブルガー文付き項書換え系における書換え帰納法について
- フォーマルアプローチ論文特集の発行にあたって
- 例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム(ディペンダブルコンピューティング)
- 等式を規則化する変換の停止条件
- 単純型付き項書き換え系における静的依存対法とその周辺
- 動的型言語への柔らかい型付けによるエラー検出
- 対話型埋込みによる数独問題の設計ツール
- プログラム生成系GeneSysにおける等式仕様への否定の導入
- 導出木からのループ検出による論理プログラムの非停止性証明法
- 振舞等価性の証明のための等式付き書換えに基づく潜在帰納法
- 左線形な定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン
- 5K-8 消費電力の実行時予測を用いた電力最適化(マルチスレッドと省電力,学生セッション,アーキテクチャ)
- 細粒度リポジトリに基づくVHDLツールプラットフォーム(ツール,開発環境)
- プログラムの正規化に基づいた差分抽出法の提案
- On the Job Learning : 産学連携による新しいソフトウェア工学教育手法
- 高精度なデータ依存解析に基づくシーケンス図スライシング手法(モデリング(学生セッション))
- ソフトウェア理解支援のための多粒度ソフトウェアマップ(インタフェース・ナビゲーション(学生セッション))
- ソフトウェアの大局的可視化のための組織化メトリクス
- StrutsLint : Web アプリケーションコーディングチェッカ
- 7.高信頼WebWare生成技術 : WebWareのテスト・解析・作成支援(第1部:高い生産性を持つ高信頼ソフトウェア作成技術の開発,学と産の連携による基盤ソフトウェアの先進的開発)
- ウインターワークショップ2008・イン・道後開催報告
- 制御ソフトウェアの固定小数点演算化ツールの設計と実装
- 飛行船制御を題材としたプロジェクト型ソフトウェア開発実習
- 4M-4 細粒度マークアップに基づくカスタマイズ可能なコーディング規約検査器(リーディングプロジェクト e-society:高信頼ソフトウェア・WebWare開発支援システム,一般セッション,リーディングプロジェクト e-society)
- アマゾンバグ防止フレームワークのためのWebアプリケーション双実行モデル
- GUI抽象化規則を用いたモデル生成手法(開発支援(2)(学生セッション))
- Web抽象プログラムを用いたリファクタリング(開発支援(2)(学生セッション))
- メタ情報とコンテキスト情報を用いた入力補完機能とXPath入力への応用
- デ-25 CX-Checker : 柔軟なカスタマイズが可能なC言語コーディングルールチェッカー(デモセッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- メタ情報とコンテキスト情報を用いた入力補完機能と XPath 入力への応用
- バリエーション並行開発のための版管理ツールと統合開発環境
- 付箋による一時的情報の管理とその応用
- 5L-8 コード視覚化手法を用いたMPIプログラム開発環境のユーザインタフェース(プログラミング支援環境,学生セッション,ソフトウェア科学・工学)
- 1K-6 静的解析情報を利用したセキュアシステムの侵入検知精度向上(仮想化と言語処理系,学生セッション,アーキテクチャ)
- 1X-2 冗長な検査の削除を行う整数オーバーフロー対策ツールの実装(セキュア設計・実装・フォレンジクス,学生セッション,セキュリティ)
- 時間付き$\pi$計算における有限プロセスの時間動作抽象化(計算機科学の理論とその応用)
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- Javaプログラム理解支援のための不変性解析
- Java プログラム理解支援のための不変性解析
- π計算に対する時間拡張と合同的性質(計算モデル,フォーマルアプローチ論文)
- π計算に基づくプログラミング言語NepiのためのGUI機能
- 時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述(オブジェクト指向とWeb技術)
- π計算による優先度継承プロトコルの形式的記述
- 形式的手法に基づくJavaScriptプログラムの型検査系の実現
- 宣言的なプログラム解析が可能なRDFに基づく細粒度ソフトウェアリポジトリ(開発支援(2)(学生セッション))
- 宣言的なプログラム解析が可能なRDFに基づく細粒度ソフトウェアリポジトリ
- (開発支援環境)XMLを用いた汎用的な細粒度ソフトウェアリポジトリの実装(オブジェクト指向技術)
- B-017 リバースエンジニアリングによるUMLをベースとした拡張シーケンス図の生成(B分野:ソフトウェア)
- 形式的概念分析を用いたグルーピングによるCプログラム理解支援手法(学生セッション H_開発支援)
- UMLをベースとしたJavaプログラムの視覚化における手続的処理部の表現について
- イディオム検索のための関数呼出依存グラフのクラスタリング手法(ソフトウェア工学)
- XML記述によるソフトウェアリポジトリを用いたコード検索(開発支援環境)
- FCDGに基づいたコーディングパターン
- ラウンドトリップエンジニアリングを目指したWebアプリケーションのための意味モデル(産学連携論文)
- 4M-6 WebブラウザのCSSレンダリング妥当性検査手法の提案(リーディングプロジェクト e-society:高信頼ソフトウェア・WebWare開発支援システム,一般セッション,リーディングプロジェクト e-society)
- 構造に基づいたXML文書のスキーマ変換器自動生成
- モデル生成法に基づくJavaScriptプログラム型検査の機械実行(ソフトウェア,フォーマルアプローチ論文)
- 構文木に着目してXMLマークアップされたソースプログラム間の差分抽出(開発支援(1)(学生セッション))
- モデル生成に基づくJavaScriptプログラムの型検査系
- ミューテーション法を用いたテストセット構成支援に関する研究(開発支援(2)(学生セッション))
- 文脈に基づいたソースプログラムとドキュメント間の識別子対応付け手法(開発支援(2)(学生セッション))
- ミューテーション法を用いたテストセット構成支援に関する研究
- モデル生成に基づくJavaScriptプログラム型検査のためのフロントエンド
- Cプログラムの理解を支援するナビゲーション機能(開発支援(学生セッション))
- 構文解析器の開発支援環境(開発支援(学生セッション))
- 付箋によるコミュニケーション機能を備えたソフトウェアブラウザ
- オブジェクト指向言語のための細粒度システム依存グラフ
- 動作履歴を用いた焦点絞り込みによるプログラム理解
- 細粒度リポジトリに基づくVHDLツールプラットフォーム
- 前バージョンの整合性を用いた設計復元
- サンプルプログラム自動生成のためのリソースを考慮した依存グラフ
- 空欄補充問題の自動生成によるHaskellプログラミング学習支援環境
- ウィンターワークショップ2011・イン・修善寺開催報告
- テストプログラム生成ツールのフロントエンドプロセッサの開発
- マルチプロセッサ対応RTOS向けテストプログラム生成ツールにおけるプロセッサ間同期の実現
- テストプログラム生成ツールのフロントエンドプロセッサの開発
- マルチプロセッサ対応RTOS向けテストプログラム生成ツールにおけるプロセッサ間同期の実現
- 項集合書換え系の完備化について
- CX-Checker:柔軟にカスタマイズ可能なC言語プログラムのコーディングチェッカ
- コールスタックの制御データ検査によるスタック偽装攻撃検知
- APIの使用状況に基づくイディオムの抽出とそれを用いたソフトウェア自動分類
- 大規模ソフトウェアの概要把握の支援を目的とした構造体型の特徴付け
- B-024 Webサイト群の構造分析による典型的構造の抽出法(デジタルドキュメント・ソフトウェアサイエンス,B分野:ソフトウェア)
- A-011 既存のプログラミング言語のための量子探索機構(アルゴリズム・コンピュテーション(1),A分野:モデル・アルゴリズム・プログラミング)
- ソフトウェア開発支援基盤のためのソースプログラムのXML表現(ソフトウェア工学,ソフトウェア基礎・応用論文)
- コーディング規約違反の局所性に着目した自動検出不可能な違反の検出に向けて
- コーディング規約違反の局所性に着目した自動検出不可能な違反の検出に向けて
- ソフトウェア理解支援のためのデータ構造の重要度評価手法