×

基于定理证明的内存安全验证工具算法综述

消耗积分:0 | 格式:rar | 大小:1.37 MB | 2021-04-20

分享资料个

　　随着软件运行时验证技术的发展，出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是，其中一些没有经过严格证明的验证工具往往存在两方面的问题，是插桩程序的加入可能会改变源程序的行为及语义，二是插桩程序并不能有效保证内存安全。为了解决这些问题，文中提出了一种使用Coq定理证明器来判定内存安全验证工具算法是否正确的形式化方法，并使用该方法对C语言运行时验证工具Move的动态检测算法的正确性进行了证明。对安全规范性质的证明结果表明了Mσve的内存安全性动态检测算法是正确的。

下载并关注上传者 开通VIP，低至0.08元下载/次

声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉

评论(0)
发评论

下载排行榜

全部0条评论

快来发表一下你的评论吧 !