一种基竽符号执行的Java缺陷检测工具的设计与实现的任务书.docx

一种基竽符号执行的Java缺陷检测工具的设计与实现的任务书
任务书
一种基于符号执行的Java缺陷检测工具的设计与实现
背景
Java是一种广泛使用的编程语言，它被广泛应用于Web开发、移动应用程序、桌面应用程序甚至是嵌入式系统等领域。作为一种类型安全的语言，Java能够有效地减少程序中的一些常见缺陷，例如缓冲区溢出、空指针引用和类型转换错误等。但是，仍然存在一些难以避免的缺陷，如逻辑错误和数据竞争。为了提高程序的质量和可靠性，需要一种高效、准确的缺陷检测工具进行检测和修复。
任务描述
本任务的主要目的是设计和实现一种基于符号执行的Java缺陷检测工具。该工具将使用符号执行技术，遍历程序的所有路径，并生成符号执行路径约束条件。然后，将路径约束条件传递给符号求解器，以检查这些路径条件是否可以满足（即确定这些路径是否可达），并生成输入，以对可达路径进行测试。
具体而言，本任务的主要内容如下：
1.了解符号执行技术的基本原理和Java语言的相关特性。学习如何将符号执行技术应用于Java程序分析中。
2.设计和实现Java符号执行引擎。该引擎将被用于遍历Java程序，并为程序路径生成符号执行路径约束条件。Java符号执行引擎需要支持Java语言的所有基本特性（包括控制流、条件语句、函数调用等），并将基本块转换为约束条件。
3.设计和实现Java符号求解器。符号求解器将接受Java符号执行引擎生成的约束条件，并通过将其转换为SMT（SatisfiabilityModuloTheories）问题来解决它们。Java符号求解器需要支持整数和实数类型，以及Java语言中的其他类型，例如字符串和布尔值。
4.设计和实现Java缺陷检测器。Java缺陷检测器将使用Java符号执行引擎和Java符号求解器来检测程序中的逻辑错误和数据竞争。为逻辑错误，Java缺陷检测器将设计检查程序路径的超出约束是否满足预期。对于数据竞争，Java缺陷检测器将设计检查程序中的共享内存访问，在发现冲突的情况下生成访问顺序约束以进行检查。
5.进行实验和评估。使用合适的基准测试集和真实应用程序对该工具进行评估，以检查其检测效率和准确性。
6.编写实验报告。编写一份实验报告，介绍该工具的设计和实现，以及实验结果和分析。
任务要求
1.使用Java作为主要开发语言，使用符号执行技术和SMT求解器进行设计和实现。
2.要求使用开源工具，并对所有代码进行注释。
3.要求对符号执行技术和SMT求解器进行深入研究，并使用相应的算法和数据结构。
4.要求使用适当的测试和评估方法对该工具进行评估，并撰写一份实验报告，详细介绍该工具的设计和实现，以及实验结果和分析。
5.任务完成后，要撰写一份技术报告，介绍该工具的设计和实现，以及对Java程序进行缺陷检测的可能性和局限性。
参考文献
1.SenK.etal.Asurveyofresearchonsoftwareclones.TechnicalReportTR1267.UniversityofIllinoisatUrbana-Champaign,2006.
2.CadarC.etal.KLEE:unassistedandautomaticgenerationofhigh-coveragetestsforcomplexsystemsprograms.InOSDI’08:Proceedingsofthe8thUSENIXconferenceonOperatingsystemsdesignandimplementation,pages209–224,Berkeley,CA,USA,2008.USENIXAssociation.
3.CadarC.etal.Executor:automatictestgenerationfromhigher-ordermodelsofsystembehavior.InOSDI’06:Proceedingsofthe7thsymposiumonOperatingsystemsdesignandimplementation,pages69–84,Berkeley,CA,USA,2006.USENIXAssociation.
4.FlanaganC.etal.TheConfluenceofLightweightStaticAnalysisandConcolicTestingforEffectiveBugFinding.Inproceedingsofthe2007IEEE/ACMinternationalconferenceonAutomatedsoftwareengineering.IEEEComputerSociety,2007:389–392.
5.TillmannN.etal.Pex:whiteboxtestge