@techreport{oai:ipsj.ixsq.nii.ac.jp:00227080,
 author = {奥田, 哲矢 and 中林, 美郷 and 堀之内, 謙一 and 岡崎, 智行 and 小林, 鉄太郎 and 山村, 和輝 and 宮澤, 俊之 and 福永, 利徳},
 issue = {3},
 month = {Jul},
 note = {本研究では，形式検証分野の技術である Proof-Carrying Code を用いて，解析対象プログラムが扱うパーソナルデータなどの秘匿情報について，秘匿情報を格納する変数にラベリングして追跡を行い，秘匿情報に対して適正に暗号化処理やハッシュ処理を行っているかを解析して，プログラムに証拠となる検証論理式を付与することで，秘匿情報が適正に管理されていることをプログラム実行者が検証可能となる仕組みを提案する．先行研究に比べて，LLVM-IR（中間表現）に基づいて解析を行うことで，解析対象プログラムの開発言語が限定されないこと，および，検証論理式の結合が可能なため，例えば，ソフトウェアサプライチェーンにおいてプログラムの追加や改変が行われる場合に，検証論理式のデータサイズと検証時間を低減し得ることが利点である．提案手法の評価として，暗号化処理やハッシュ処理を行う計 6 点の OSS 等サンプルプログラムに対して解析を行い，出力された検証論理式の全 57 件の内 53 件で安全性要件を充足するという検証結果が正しく得られることを確認した．また，内 4 件の安全性要件を充足しない検証結果については，デバッグ出力のコードが存在していることを確認し，デバッグ用のテストコードとしては問題がないこと，一方で，そのようなデバッグ用のコードが商用向けのコードに存在する場合など，開発者の意図しない設定や実装の誤りを是正することに本提案手法が有効であることが示唆された．},
 title = {秘匿情報を格納する変数のProof-Carrying Codeを用いた追跡と安全性評価},
 year = {2023}
}