Study of Verification of Security of Programs based on Term Rewriting Systems and Tree Automata

基于术语重写系统和树自动机的程序安全性验证研究

• 批准号: 20300010
• 负责人: SAKABE Toshiki
• 金额: $ 8.07万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20300010/
• 关键词: 仕様記述; 仕様検証; 安全性; 非干渉性; 項書き換え系; 木オートマトン; SMTソルバー; ホオートマトン; モデル検査; 車載LANプロトコル

The purpose of this project is to develop methods for verifying properties of programs by applying techniques of term rewriting and tree automata. The results are methods for verifying automotive LAN protocols and proving program equivalence, and automated generation of loop invariants of imperative programs. In addition, we have obtained several results which are basic to program verification : methods for proving termination of term rewriting systems, efficient SAT solvers for propositional logic and SMT solvers for equational logic.

本计画的目的是利用术语重写和树自动机的技术，发展验证程式属性的方法。结果是验证汽车局域网协议和证明程序等价的方法，以及命令程序循环不变量的自动生成。此外，我们还获得了几个基本的程序验证结果：证明项重写系统终止的方法，命题逻辑的有效SAT求解器和等式逻辑的SMT求解器。

项目成果

プレスブルガー文付き項書換え系における書換え帰納法について

用 Presburger 语句重写术语重写系统中的归纳法

• 发表时间: 2008
• 期刊: 電子情報通信学会技術研究報告(SS2008-1)
• 作者: 坂田翼;西田直樹;酒井正彦;草刈圭一朗;坂部俊樹
• 通讯作者: 坂部俊樹

ビットエラー通信路におけるスケーラブルCANの動作解析

可扩展CAN在误码通信路径中的运行分析

• 发表时间: 2008
• 期刊: 電子情報通信学会技術研究報告(SS2008-37) 108
• 作者: 鵜飼謙児;坂部俊樹;高田広章;倉地亮;酒井正彦;草刈圭一朗;西田直樹
• 通讯作者: 西田直樹

On Proving Termination of Constrained Term Rewriting Systemsby Elim-inating Edges from Dependency Graphs

通过消除依赖图中的边来证明约束项重写系统的终止

• 发表时间: 2011
• 期刊: LNCS
• 作者: SAKATA Tsubasa;NISHIDA Naoki;SAKABE Toshiki
• 通讯作者: SAKABE Toshiki

スケーラブルCANプロトコルの動作解析に関する予備的考察

可扩展CAN协议运行分析的初步思考

• 发表时间: 2008
• 期刊: 平成20年度電気関係学会東海支部連合大会講演論文集 O-262
• 作者: 鵜飼謙児;坂部俊樹;高田広章;倉地亮;酒井正彦;草刈圭一朗;西田直樹
• 通讯作者: 西田直樹

制約付き木オートマトンとその閉包性

约束树自动机及其闭包性质

• 发表时间: 2011
• 期刊: 電子情報通信学会ソフトウェアサイエンス研究会
• 作者: 倉橋克尚;酒井正彦;西田直樹;坂部俊樹;草刈圭一朗
• 通讯作者: 草刈圭一朗