论文摘要：模型检测在嵌入式系统的应用及并行化研究

软件安全日益重要，对软件安全要求高的嵌入式领域，如航空航天等，迫切需要完备的检测方法来保证软件的安全可靠性，以弥补测试技术的不足。近年来，模型检测越来越受到人们的关注。模型检测方法具有检测精度高、自动程度高等优点，并且在硬件系统和通信协议验证等方面的应用中取得了巨大成功。本文尝试将模型检测技术应用于嵌入式软件的安全检测方面，静态检查软件源代码以发现其中的安全漏洞。本文首先分析了嵌入式内存分配的特点，发现对安全可靠性很高的嵌入式软件多采用静态分配方式，静态分配内存的方式很适合模型检测进行漏洞检测的应用。但由于模型检测还不能直接应用于缓冲区溢出漏洞检测，因此本文利用约束分析技术构建了关于缓冲区属性的属性约束系统，并使用模型检测技术对约束系统进行求解，从而实现缓冲区漏洞的检测。同时，本文将属性约束系统的构建过程抽象成约束规则，提出了一套基于偏序理论的形式化漏洞检测描述方法。为了进一步扩展模型检测的应用范围，扩大检测规模，本文对模型检测在应用中的性能和效率作了统计和分析，研究适用于漏洞检测方法中的并行优化方法。本文在基于模型检测的漏洞检测方法基础上，实现了MPI并行优化方案和pthreads并行优化方案，并通过monkey和corehttp的检测结果，分析和比较了并行优化的效果。然后使用pthreads对超过1万行的VxWorks的usb驱动模块进行检测，并发现了一个漏洞。同时，本文还通过统计定理证明器Simplify的查询次数和搜索的最深路径长度，分析了状态空间在并行优化前后的对比。

来源：半壳优胜育转载请保留出处和链接！

本文链接：http://87cpy.com/203765.html