c程序运行时监控和验证的插桩方法研究与应用

《c程序运行时监控和验证的插桩方法研究与应用》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中图分类号：TP311论文编号：102871616-SZ010学科分类号：085211硕士学位论文C程序运行时监控和验证的插桩方法研究与应用研究生姓名朱云龙专业类别工程硕士专业领域计算机技术指导教师李绪蓉副教授（陈哲副教授）南京航空航天大学研究生院计算机科学与技术学院二О一六年三月NanjingUniversityofAeronauticsandAstronauticsTheGraduateSchoolCollegeofComputerScienceandTechnologyResearchonInstrumentationMethodsinRun

2、timeMonitoringandVerificationforCProgramsandApplicationsAThesisinComputerTechnologybyZhuYunlongAdvisedbyAssociateProf.LiXurong(AssociateProf.ChenZhe)SubmittedinPartialFulfillmentoftheRequirementsfortheDegreeofMasterofEngineeringMarch,2016承诺书本人声明所呈交的硕±学位论文是本人在导师指导下进行的研究工作及取

3、得的研究成果。除了文中特别加标注和致谢的地方外，论文中不包含其他人己经发表或撰写过的研究成果，也不包含为获得南京航空航天大学或其他教育机构的学位或证书而使用过的材料。本人授权南京航空航天大学可Ｗ将学位论文的全部或部分内容编入有关数据库进行检索，可采用影印、缩印或扫描等是制手段保存、汇编学位论文。（保密的学位论文在解密后适用本承诺书）ｔｉＩ作者签名：ｆ日期ｌｏｌＵ．巧：南京航空航天大学全日制专业硕士学位论文摘要随着软件在社会生活应用中的不断深入，软件系统的体积和复杂度都呈现出迅速增长的态势，软件可靠性问

4、题也相应成为软件行业发展不容忽视的重要方面。在现有的软件验证技术中，运行时验证作为一种轻量级的验证技术，综合了运行时监控技术和形式化规约技术，是当前软件验证领域的一个研究热点问题。而在运行时验证的技术实现中，一方面需要实现待验证性质的描述和相应验证器的生成，另一方面需要将监控器和验证器集成到待监控的软件系统中，即监控和验证代码的插桩。由于软件体积和复杂度的不断增加，基于日志API监控或手动进行监控验证代码插桩明显不能满足不同平台，不同类型系统监控验证的需求。随着编译器技术和面向方面编程技术的不断发展，利用编译器实现代码自动插桩，借助面向方面语言实现

5、插桩位置描述和模块化管理，正在成为推动运行时验证实际应用的重要研究领域。本文分析了C语言的编译流程，LLVM开源编译器框架及其Clang编译器前端，在此基础上参照面向方面编程的概念，设计并实现了一种针对C程序的面向方面语言MOVEC，其相应编译器能够解析监控器插桩位置的描述并利用源代码插桩技术实现插桩需求。同样基于源代码插桩的技术，本文设计并实现了软件中除0，整数溢出和变量使用前未初始化错误验证器的插桩。通过将MOVEC语言编译器和现有针对C/C++程序的面向方面语言编译器AspectC，AspectC++在准确性，插桩时间，程序性能影响和程序代码

6、膨胀等方面进行对比，表明MOVEC语言能够在保证对程序性能的低影响前提下，实现更高的准确性，更低的插桩时间，更小的代码膨胀率。实验同时验证了三种常见错误验证器设计和插桩方法的正确性。本文的工作为运行时验证监控器和验证器插桩的自动化，高效率，跨平台实现提供了基础，能够促进运行时验证在实际生活中的应用。关键词：运行时监控，运行时验证，源代码插桩，C语言，面向方面编程IC程序运行时监控和验证的插桩方法研究与应用ABSTRACTWithmoreandmoresoftwareisappliedinsociallife,thesizeandcomplexity

7、ofsoftwaresystemsareincreasingrapidly,softwarereliabilitybecomesanimportantaspectofsoftwaredevelopmentaccordingly.Amongtheexistsoftwareverificationtechnologies,asalightweightsoftwareverificationmethod,runtimeverificationcombinesthetechnologyofruntimemonitoringandthetechonolgyo

8、fformalspecification,soitisrisingasapopresearcharea.Thekeytor