如何解决软件知识产权的保护问题,已成为近年来国内外的一个研究热点,具有重要的学术价值和现实意义。目前,研究者们在软件保护方面已经取得了一些优秀的研究成果,但仍有许多问题亟待研究和解决。本文主要围绕软件保护方面三种主要的技术——代码迷惑、软件胎记和软件水印的性能评价问题展开研究,主要包括:1、针对数据迷惑性能评价困难,缺乏统一的形式化框架的问题,利用抽象解释理论,提出了一种数据迷惑的正确性与有效性的形式化分析方法。首先,使用抽象解释理论对数据迷惑进行了形式化地描述。在给出了变量变换函数和变量变换反函数的基础上,将数据迷惑这一类变换统一地描述为一种以变量变换函数和变量变换反函数为参数的语义变换,即语义数据迷惑。然后,在语义数据迷惑的基础上,由语义变换和语法变换之间的关系,构造得到语法数据迷惑,即数据迷惑算法。之后基于数据迷惑的形式化描述,给出了一种可观察行为的形式化描述,分析了数据迷惑对于该可观察行为的正确性;并以针对数据属性的程序静态分析作为数据迷惑的攻击模型,讨论了数据迷惑的有效性。最后,以一种典型的数据迷惑变换——变量编码为例,验证了该形式化分析方法的有效性。2、针对现有软件胎记的评价多依赖于实验,缺乏理论支持的问题,给出了一种基于抽象解释的软件胎记的可信性与鲁棒性的分析方法。首先,从语义的角度分别对程序拷贝关系和语义保持变换攻击进行了形式化地描述。程序拷贝关系可以用与其对应的程序语义属性的等价性来描述,而语义保持变换则可以描述为语义程序变换。然后,在此形式化描述的基础上,使用抽象解释理论给出了软件胎记的语义定义,并讨论软件胎记的可信性和鲁棒性。最后,以Choi等人提出的经典的静态API软件胎记为例,验证了该形式化分析方法的有效性。在对静态API软件胎记形式化描述的基础上,使用上述形式化方法,分析了该软件胎记对于某种给定的程序拷贝关系的可信性和对于指令等价替换变换的鲁棒性。3、为提高软件水印算法的抗攻击性,尤其是抗裁减攻击和变形攻击的能力,给出了一种基于数据迷惑和软件胎记的软件水印框架,并利用抽象解释理论对该类软件水印的抗攻击性进行了分析。首先将数据迷惑和软件胎记技术引入到软件水印之中,提出了一个软件水印框架。该水印框架将软件胎记引入到水印的生成过程中,把水印信息编码为某种软件胎记,并通过构造具有该特定软件胎记的代码生成含水印信息的代码,从而提高水印抵抗变形攻击的能力;同时利用数据迷惑嵌入含水印信息的代码,增大攻击者逆向工程的难度,增强水印抵抗裁减攻击的能力。然后,在该框架下,从程序语义的角度利用抽象解释理论对软件水印的抗攻击性进行分析,包括:抗裁减攻击和抗变形攻击的能力。最后,给出一个具体的软件水印算法,并以其为例对该水印抗裁减攻击和抗变形攻击的能力进行具体地分析。实例分析表明数据迷惑和软件胎记的引入提高了水印抗裁减攻击和变形攻击的能力。最后,对全文工作进行了总结,并对下一步的研究方向进行了展望。