基于抽象解释的移动代码安全方法

理论计算机科学电子笔记132（2005）113-129www.elsevier.com/locate/entcs一种基于抽象解释的移动代码安全方法埃尔维拉·阿尔伯特，Germ'anPuebla，Manuel Hermenegildo，3岁马德里康普顿斯大学马德里工业大学新墨西哥大学University of New Mexico摘要最近的移动代码安全方法，如携带证明的代码，涉及将安全信息与程序相关联。代码供应商提供一个程序，并附带一个证书（或证明），其有效性需要遵守预定义的安全政策。 预期的好处是程序消费者可以在本地验证证书w.r.t.。“不可信”的程序通过一个证书检查器-一个过程，这应该是更简单，高效，自动生成比原来的证明。我们在这里介绍了一种新的方法，移动代码安全遵循类似的计划，但它是基于整个抽象解释技术的使用。在我们的框架中，安全策略通过使用抽象域上定义的表达性断言语言来指定。我们确定了基于抽象解释的静态分析结果中的一个特定片段，它作为证书特别有用。 在消费者方面，证书的有效性由一个非常简单和高效的专用抽象解释器来检查。我们的想法说明通过一个例子中实现的约束逻辑程序的背景下，使用CiaoPP系统。虽然还需要进一步的实验，但我们相信，提出的方法是有趣的，因为它带来了自动化和表现力，这是固有的，抽象解释技术应用于移动代码安全领域。关键词：移动代码安全，认证编译，携带证明代码，抽象解释，静态分析。1 电子邮件地址：elvira@sip.ucm.es2 电子邮件地址：german@fi.upm.es3电子邮件：herme@unm.edu或herme@fi.upm.es1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.032114E. Albert等人理论计算机科学电子笔记132（2005）1131介绍当今计算研究面临的最重要的挑战之一是开发用于验证由不可信源（可能）提供的程序的执行是安全的安全技术，即，它根据预定义的安全策略满足某些属性。移动代码安全的最新方法涉及将安全信息以一个程序的证书[13，11，12]。证书（或证明）在编译时创建，并与不受信任的代码一起打包。接收或下载代码+证书包的消费者可以运行验证器，通过直接检查代码和证书，可以验证证书的有效性，从而符合安全策略。这种“基于证书”的移动代码安全方法的主要好处是，确保遵守所需安全政策的负担从消费者转移到供应商。消费者的任务从证明的层次减少到检查的层次。事实上，验证者或证明检查器执行的任务应该比生成原始证书简单得多，高效，遵循这种方法的着名方法包括证明携带代码（PCC）[13]和类型化汇编语言（TAL）[12]。值得注意的一点是，证书可以采取不同的形式。例如，在PCC中，证书最初是某些验证条件的一阶逻辑证明，验证过程涉及检查证书是否确实是有效的一阶证明。最近的提议[1]使用时态逻辑来指定PCC中的安全策略。在TAL中，证书是汇编语言程序的类型注释，验证过程涉及一种类型检查。然而，基于证书的移动代码安全系统的设计面临着相同的基本挑战：(i) 定义涵盖广泛属性的明确安全策略(ii) 解决了如何自动生成证书的问题，(iii) 为证书设计简单、可靠、高效的检验器各种方法在表现力、灵活性和效率上有所不同，但它们都有一个共同的目标，即使用安全信息使消费者安全高效地在本地执行不受信任的移动代码。我们的主要贡献是引入一种新的基于证书的移动代码安全方法，该方法遵循整体方案，但始终基于抽象解释技术的使用[3]，以处理上述基本和困难的问题。我们工作的一个出发点是观察到，现在已经建立了良好的-E. Albert等人理论计算机科学电子笔记132（2005）113115抽象解释的成熟技术已经允许开发非常复杂的全局静态程序分析，这些分析同时是自动的、可证明正确的和实用的。抽象解释的基本思想是通过使用抽象值而不是具体值来解释（“运行”）程序来推断程序上的信息例如，该技术允许推断比传统类型更丰富的信息。这包括数据结构形状（如指针共享）、数据结构大小的界限和其他操作变量实例化属性，以及过程级属性，如确定性、终止性、非故障性和资源约束的界限。消耗（时间或空间成本）。CiaoPP[7]是Ciao多范式约束逻辑程序设计系统的基于抽象解释的预处理器。它使用模块化的增量抽象解释作为获取程序信息的基本工具。在CiaoPP中，通过分析产生的语义近似已被应用于高层和低层程序编译期间的优化，包括多抽象专门化、并行化和资源使用控制等转换最近，这种语义近似的新的和有前途的应用程序已经提出了更一般的程序开发的背景下在CiaoPP系统的背景下，我们在这里介绍了一种新的方法来移动代码安全，遵循基于证书的计划，但它是基于整个抽象解释的技术。 的设计我们的基于抽象解释的系统由三个主要元素组成：(i) 一种用于定义安全策略的表达性断言语言。因为- sertions允许我们表达“抽象”-即符号-属性在不同的抽象域。我们的框架是参数w.r.t.兴趣的抽象领域，它赋予我们概括性和表现力。(ii) 一个fixpoint静态分析器用于自动推断有关移动代码的信息，然后可以用来证明代码是安全的w.r.t.以一种简单的方式给出断言。我们确定了分析结果的特定切片，这对于此目的是足够的。(iii) 一个简单、易于信任的分析检查器可验证移动代码上信息的有效性。它实际上是一个专门的抽象解释器，不需要编译器来达到一个定点（相反，标准分析仪）。通过利用在先前分析阶段中收集的分析信息所得到的方案已被纳入CiaoPP预处理器，其效率正在进行实验评估。本文的结构如下。 第2节描述了断言lan-116E. Albert等人理论计算机科学电子笔记132（2005）113create_streams（[]，[]）.create_streams（[N|荷兰]、[法|FL]）：-number_codes（N，ChInN），generate（ChInN，Fname），safe_open（Fname，write，F），create_streams（NL，FL）.generate（ChInN，Fname）：- app（“/tmp/"，ChInN，Fname）. safe_open（Fname，Mode，Stream）：-atom_codes（File，Fname），open（File，Mode，Stream）.Fig. 1. 示例移动代码这是用来定义我们的安全政策的标准。第3节介绍了认证过程以及验证条件的生成，以证明符合安全政策。在第4节中，我们概述了检查安全性信息有效性的过程。最后，第5节讨论了本文所做的工作以及相关的工作。2一种指定安全策略安全策略的目的是精确地规定程序的执行被认为是安全的条件。在现有的方法中，安全策略通常对应于类型安全的一些变体（也可以控制内存或数组边界的正确访问[14]）。我们建议使用CiaoPP中可用的高级断言语言[15]（的子集）来定义约束逻辑程序上下文中的安全策略。2.1预赛我们首先介绍约束逻辑编程[9]（CLP）的一些符号和初步概念。术语是从变量（例如， X）、函子（例如， f）和谓词s（例如，，p）。 We表示by{X1<$→t1， . . ，Xn<$→t n}证明了用σ（Xi）= t i替换σ对所有i = 1，.，n（其中X i/=X j如果ii=j）和σ（X）=X，其中ti是项。一个重命名是一个置换ρ，其中存在逆ρ−1使得ρρ−1<$ρ− 1ρ <$id。约束本质上是由预定义谓词（例如实数上的项方程或不等式）构建的表达式的合取，其参数使用预定义函数（例如实数加法）构建。原子具有形式p（t1，...，其中p是谓词符号，t i是项。一个文字是一个原子或一个约束。 一个目标是一个有限的文字序列。规则的形式是H：-B，其中H，头部，是原子，B，主体，是一个可能为空的有限文字序列约束逻辑程序或程序是一组有限的规则。E. Albert等人理论计算机科学电子笔记132（2005）113117例2.1让我们考虑图1中的CLP程序。主pred- icatecreate streams/2接收一个数字列表作为第一个参数，并在第二个参数中返回相关的文件处理程序（流）列表打开的文件。谓词numbercodes/2、atomcodes/2和open/3是ISO标准的Prolog谓词，因此它们在CiaoPP中可用。 在我们的示例中，呼叫号码代码（N，ChInN）接收号码N，并在ChInN中返回包括N的表示的字符的ASCII代码的列表。此外，调用atomcodes（File，Fname）在Fname中接收ASCII代码列表， 并返回由相 应字符组成 的atomFile。调用open（File，Mode ，Stream）打开名为File的文件，并在Stream中返回与该文件相关的流。参数Mode可以有任何值：read、write或append。辅助 谓词generate通过 使用众 所周知的 列表连 接谓词 app/3 将前 缀“/tmp/“连接到作为第一个参数接收的数字。请注意，谓词创建流并不直接调用系统谓词open，而是调用辅助谓词safeopen。其原因将在例2.3中讨论。2.2抽象属性断言是语法对象，它允许表达程序的各种高级属性（在我们的例子中是CLP-）例如，声明程序模块入口点信息的断言，描述内置程序属性的断言，提供某些类型声明的断言，成本界限等。我们的方法的一个显着特点是，安全属性表示为抽象域（D α）的上下文中的替换，它比具体域（D）简单。 一个抽象值是一个有限的表示，可能是有限的，在具体领域的实际值的集合 我们的方法依赖于抽象解释理论[3]，其中表示Dα的所有可能的抽象语义值的集合通常是一个完整的格或cpo，它是升链有限的。然而，在本研究中，抽象解释仅限于集上的完备格，无论是具体的α 2D，α 2 D和抽象的α 2Dα，± α2 D域。抽象值和具体值的集合通过一对单调映射<$α，γ<$：抽象化α：2D→D α，具体化γ：D α→2 D联系起来，例如证明了<$x∈ 2 D：γ（α（x））<$x和<$y∈D α：α（γ（y））= y. 一般来说，±是由α和α诱导的。类似地，最小上界（H）和最大下界（H）的运算在精确意义上模仿2D的运算。在这个框架中，抽象属性被定义为抽象替换，它允许我们用抽象域来表达属性，118E. Albert等人理论计算机科学电子笔记132（2005）113：-regtype safe_name/1.安全名称（“/tmp/”）||L）：-list（L，数组_code）。：-regtype_code/1. 函数A_code（X）：- alpha_code（X）。numnum_code（X）：-num_code（X）。：-regtype alpha_code/1。alpha_code（A）：- member（A，“abcdefghijklmnopqrstuvwzyz”）. alpha_code（A）：-member（A，“ABCDEFGHIJKLMNOPQRSTUVWXYZ“）.：-regtype num_code/1。num_code（C）：-member（C，“0123456789”）.图二. 示例的常规类型程序的执行必须满足。我们在示例中使用的描述域是一个常规类型do- main [4]。我们通常将这个域称为etremes[19]，因为它是CiaoPP中的名称。 一个常规类型是一组术语，可以描述为： 一个规则的术语语法，或者等价地，一个有限树自动机。为了定义一个正则类型，我们可以选择正则一元逻辑程序作为一个树自动机的表示（如[5，6]）。我们也采用这种表示法作为Ex。2.2我会解释的。在一组变量V上的eterms域中的抽象替换为V中的每个变量分配一个正则类型。除了用户例如，我们将在示例中使用术语，这是最通用的类型，即，它对应-回答所有可能的条件。类型常量表示带零的函子arguments，num，所有可能的数字的集合，string，字符列表，list，任何可能的列表，io term访问文件的模式（即， 写、读或追加）和流 ， 用 于 顺 序 文 件 的 处 理 程 序 。 我 们 允 许 参 数 类 型 ， 例 如 list（T），它表示所有元素都是T类型的列表。请注意，类型list等效于list（term）。显然，对于任何类型的T，列表（T）±列表±项。在e项中，最一般的替换T是V中所有变量的-符号项.最小一般替换将空的值集赋给每个变量。为了简洁起见，在示例中，我们经常跳过其类型是最一般的替换的变量（即，术语）。例2.2在移动代码的上下文中，代码是否试图访问与使用代码的机器中的应用程序无关的文件是一个安全问题。 一个非常简单的安全策略可以是强制移动代码只访问临时文件。例如，在UNIX系统中，这可以通过确保文件驻留在目录/tmp/中来控制（在某些假设下）。图2中的正则一元逻辑程序安全名称定义了一个reg-这样它的所有值都满足这个非常简单的安全概念E. Albert等人理论计算机科学电子笔记132（2005）113119预预预预下面的抽象属性由抽象替换{X<$→safename}组成，表示X被绑定到一个以前缀“/tmp/“开头，后跟字母数字字符列表的字符在下文中，我们简单地写安全名（X）来表示前面的抽象替换。regtype声明用于在CiaoPP中定义新的常规类型。事实上，用于定义常规类型的辅助谓词，如numanum代码，alpha代码或num代码也必须使用regtype声明。构造成员（C，“0123456789”）是一个快捷方式，用于表示C可以对应于列表中从字符0到9的任何代码。2.3安全政策CiaoPP中可用的原始断言语言[15]由几个断言方案组成其中，为了本文的目的，我们简单地考虑以下两个方案，它们直观地对应于传统的过程的前置和后置条件调用（B，{λ1;......的人。;λn}）：它们表示应该在任何调用一个给定的谓词，类似于传统的前提条件。B是谓词描述符，即，它有一个谓词符号作为主函子，参数是不同的自由变量，λi，i = 1，. n是抽象的关于执行状态的属性由此产生的断言应该是跨-表示为应保持在国家的召唤”。success（B，[λPre，]λPost）：这个断言模式用于描述一个后置条件，它必须保持给定谓词的所有成功状态。 在断言中，B是谓词描述符，λPre和λPost是关于执行状态的抽象属性。λPre是可选的，必须进行评估w.r.t.将调用状态下的存储转换为谓词。然而，条件λPost必须相对于. r.t.在谓词的成功状态下的存储。如果存在可选的λPre，则λPost仅需要保持在与满足λPre的呼叫状态相对应的那些成功状态中。注意，可以给出具有不同λPre因此，断言中的抽象属性λPre和λPost允许我们用抽象域来表达程序执行必须满足的条件。每个条件都是一个抽象的替换，对应于某个原子中的变量。一般来说，编译器设计者的任务是定义与系统相关的安全策略。在CiaoPP预编译器中，上述断言语言允许我们在存在外部函数、内置函数等的情况下定义运行时系统的安全策略。120E. Albert等人理论计算机科学电子笔记132（2005）113calls（number codes（X，Y），{（num（X）;list（Y，numcodes））}）调用（原子代码（X，Y），{（常量（X）;字符串（Y））}）calls（open（X，Y，Z），{constant（X），io mode（Y）}）调用（安全打开（Fname，，），{安全名称（Fname）}）success（number codes（X，Y），T，{num（X），list（Y，numcodes）}）success（原子码（X，Y），T，{常量（X），字符串（Y）}）success（open（X，Y，Z），T，{constant（X），iomode（Y），stream（Z）}）图三. 示例的断言示例2.3图3显示了与我们运行的示例中的程序相关的断言前四行对应于调用断言，而最后三行是成功断言。在这四个调用中，前三个调用在系统中预先定义。predicatesafeopen的最后一个用户定义断言提供了一种简单的方法来保证所有对open的调用都是安全的。它可以被理解为让我们注意到，CiaoPP系统中的实际实现还包括程序点断言[15]，这避免了使用诸如此类的辅助谓词。为了简单起见，这里我们不讨论程序点断言。在我们的例子中，安全策略对应于保证程序满足图中的所有七个断言。CiaoPP[7]中不同域的共存允许使用断言语言表达它们包括模式、类型、不失效、终止、确定性、不中止、不中断和成本界限及其组合。这个想法与以下概念有关：模型承载代码（MCC）[18]的工作中提到的模型，以捕获代码的安全相关属性。MCC使代码使用者能够尝试感兴趣的不同安全策略，并选择一个可以静态证明与不受信任代码关联的模型一致的策略。在我们的框架中，不同领域的共存使人想起MCC中各种模型的存在。然而，模型的目的是描述低级别的属性和他们的组合还没有接近，这与我们的想法相结合（高级别）抽象域。与其他方法不同，断言不是每个谓词都必须的。这一点很重要，因为断言必须手动提供。因此，用户可以决定在编写断言时投入多少时间：断言越多，程序的部分正确性就越完整，检测问题的可能性就越大。然而，前置条件和后置条件通常由程序员提供，因为它们通常易于编写，并且对于生成程序文档非常有用E. Albert等人理论计算机科学电子笔记132（2005）113121此外，断言是有用的，但实际上并不需要为了获得有关程序的信息：分析算法能够获得安全的近似程序的行为，即使没有断言。这在其他方法中并不总是如此，例如经典的程序验证，其中实际上需要循环不变式这种不变量很难找到，现有的自动化技术通常不足以推断它们，因此通常必须手动提供3通过静态分析验证程序本节介绍认证过程，即，生成证书以证明程序遵守安全政策。整个认证方法基于以下思想：通过基于抽象解释的定点算法计算的分析结果的特定切片可以起到证明程序安全性的认证作用。直观地说，我们的认证过程执行以下步骤。我们从一组AS断言开始，它在抽象域Dα的上下文中建立了与程序P相关联的安全策略，如第2节所定义的。首先，运行一个标准程序分析器，该分析器返回一个应答表AT，它对P的执行相关信息进行了编码其次，从AS和AT生成验证条件V C（AS，AT），以证明P符合安全策略。条件V C（AS，AT）被发送到自动验证器，自动验证器试图验证它。如果成功，AT构成证书，并可以与程序P一起发送给消费者。第3.1节和第3.2节分别给出了元素AT和V C（AS，AT）3.1将分析结果作为证明我们认证过程的一个主要思想是，证书是由基于fixpoint抽象解释的分析器自动生成的。特别是，我们依赖于目标依赖（a.k.a. [8]的目标导向）分析器，这是在CiaoPP系统中实现的分析器。这个分析算法（下面我们简称为Analysis）除了程序P之外，还接收一组调用模式作为输入。 调用模式是对调用模式（或条目）进入程序。特别地，对于抽象域Dα，调用模式集合Q由以下形式其中，A是谓词描述符，CP是抽象子类（即，A的运行时绑定的条件）表示为CP∈Dα。 原则上，只有导出的谓词才需要调用模式。分析算法能够自动生成它们，122E. Albert等人理论计算机科学电子笔记132（2005）113内部谓词。然而，它们仍然可以通过假设T为抽象替换来自动生成（即，未给出初始信息）。虽然这个想法是通过最初的呼叫模式来改善这一为了计算分析（P，Q，Dα），传统的（C）LP程序的（目标相关的）抽象解释器构造一个图有两种节点：或-节点对应文字，而和-节点对应规则。两种节点的连接方式如下。或-节点具有到那些和-节点的弧，这些弧对应于其头部与文字相统一的规则。用于规则H：-B1，.，Bn有n条弧到对应于规则体中文字的或节点。由于篇幅的限制，并且考虑到现在已经很好地理解了，我们在这里不描述如何计算更多细节可参见，例如，[2、8、16]。由CiaoPP以下定义引入了分析的概念sis表（可以找到类似的定义，例如，在[2，8，16]中）。非正式地说，它的尝试形式为：CP→AP，这应该被解释为“满足先决条件（或呼叫替换）的定义3.1[解析答案表]设P是一个程序。设Q是表示在抽象域Dα中的一组调用模式。 我们定义一个分析答案T表，AT，因为ntriesAj：CPj→APj，j=1.由Analysis（P，Q，D α）[8]计算，其中，在每个条目中，A j是原子，CP j和AP j分别是抽象调用和成功替换。直观地，回答表包含图的或节点中的所有文字的回答模式，而弧依赖表保持关于图中的或节点之间的依赖关系的详细信息。这项工作的一个中心思想是，为了证明程序的安全性，它需要发送存储在分析答案表中的信息，因为与原始的通用算法[8]相比，可以设计一个简单的分析检查器来验证答案表，而根本不需要使用弧依赖表（如我们在第4节中所示）。抽象解释的理论保证了答案表是运行时行为的安全近似（详见[2，8，16]）。例3.2重新考虑例2.1的程序和抽象的代码。E. Albert等人理论计算机科学电子笔记132（2005）113123使用Ex-a mple 2.2的常规类型声明安全名称增 强 了 main eterm 。T akethecallingp attern createstreams（X，Y），{list（X，num）}，这表明创建流的初始调用是在第一个参数中使用数字列表执行的。CiaoPP为它计算这个答案表谓词呼叫模式成功模式创建流（A，B）List（A，num）list（A，num）， list（B，stream）数字代码（A，B）num（A）num（A），list（B，numcodes）generate（A，B）list（A，numcodes）list（A，numcodes），sf（B）app（A，B，C）A="/tmp/"，list（B，numcodes）A="/tmp/"，list（B，numcodes），sf（C）安全打开（A、B、C）sf（A），B=写sf（A），B=写，流（B）原子码（A，B）sf（B）常数（A），sf（B）打开（A、B、C）常数（A），B=写常数（A），B=写入，流（C）例如，第一个条目应该被解释为：所有对谓词创建流的调用都在第一个参数中提供一个数字列表作为输入，并且在成功时，它们分别在其两个参数中的每一个中产生数字和流的列表。 值得注意的是，CiaoPP生成辅助类型sf（ “/tmp/” ） 。 ||A ） ： -list （ A ， numcodes ） . 表 示 以 前 缀“/tmp/”开头的数字列表。显然，SF±安全的名称。这将允许CiaoPP推断在该程序中执行的打开调用满足Ex.2.2. 此外，我们使用符号var = constant表示系统生成一个新类型，它的唯一元素是这个常量，因为它发生了：对于write，在safe open和open的条目中，对于“/tmp/”，在app的条目中。为了提高准确性，分析器通常在调用时是多变量的（参见，例如，[8]）。实际上，尽管在该示例中不可见，但CiaoPP并入是多变量分析，即，一个以上的三元组A：CP1<$$>→AP1<$，. . . 、124E. Albert等人理论计算机科学电子笔记132（2005）113对于相同的谓词描述符A，可以计算C P i / = A P i的情况下的A：CPn<$→APn<$n>1。E. Albert等人理论计算机科学电子笔记132（2005）113125PrecPrecPrecPrec3.2验证条件在下一步中，代码供应商提取验证条件（VC），只有当代码的执行不违反安全策略时才能证明。对于一组初始断言，我们定义VC如下。定义3.3【验证条件】设P是一个程序，Q是抽象域Dα中的一组调用模式，AT是它的分析答案表。 假设S是一个断言。然后，验证条件，V C（S，AT），对于Sw.r.t. 在定义如下：⎪⎪（ρ（CP）± λ1）（CP）±λn）A：CP›→AP⎪⎪⎨如果S=calls（B，{λ1;......的人。 ; λ n}）V C（S）：：=⎪⎪⎪A：CP›→AP⎪⎩ρ（CP）HλPrec=λ Pρ（AP）±λPost如果S=成功（B，λPrec，λPost）其中ρ是A的变量重命名替换w.r.t. B.如果AS是一个有限的断言集合，那么它的验证条件V（AS，AT）是AS元素的验证条件的合取。粗略地说，根据定义3.3生成的VC是布尔表达式（可能包含析取）的组合，其有效性确保了一组断言w.r.t.的一致性由分析计算的答案表。它根据断言的类型区分了两种不同的情况。对于调用断言，VC要求至少有一个先决条件我Prec 类的所有现有抽象调用模式的安全近似原子湾在成功断言的情况下，有两种情况可以让它们成立。第一个表示前提条件永远不会满足，因此断言平凡地成立（并且不需要测试后置条件）。第二种对应于这样的情况，其中通过对谓词的分析计算出的成功替换比断言所需的替换更具体。让我们通过一个例子来说明这个定义例3.4考虑例3.2中生成的答案表，图3的调用和成功断言。 根据定义3.3，VC为：λ126E. Albert等人理论计算机科学电子笔记132（2005）113（num（X）±（num（X）;list（Y，numcodes））sf（Y）±（constant（X）;string（Y））constant（X），Y=write±constant（X），iomode（Y）sf（X）±安全名称（X）num（X），list（Y，numcodes）±num（X），list（Y，numcodes）常量（X），sf（Y）±常量（X），string（Y）常量（X），Y=写入，流（Z）±常量（X），io模式（Y），流（Z））每个合取词对应于图3中的一个断言，它们出现的顺序与图3中的断言相同。因此，前四个合取词用于调用断言，后三个合取词用于成功断言。整个合取的有效性可以很容易地通过考虑域中元素之间的以下（平凡）关系来证明：sf（X）±string（X）X=write±iomode（X）注意，前两个合取式在正确的条件下包含一个析取在第二个例子中，条件sf（Y）±（constant（X）; string（Y））成立，因为sf（Y）± string（Y）。因此，在创建答案表和生成VC时，通过单独解析每个合取来检查整个布尔条件的有效性。请注意，每个合取都由抽象替换对的比较组成，它们只是返回true或false，但不计算任何替换。该验证可能产生三种不同的可能状态：i）VC确实被检查过，就像上面的例子中发生的那样; ii）它被证明是错误的，因此证书是无效的，代码运行起来肯定是不安全的（我们显然应该在继续这个过程之前纠正程序）; iii）它不能被证明也不能被证明是错误的，这可能是由于几种情况。例如，分析可能无法推断出足够精确的信息来验证条件。然后，用户可以提供对初始呼叫模式的更精细的描述，或者选择不同的、更细粒度的域。在ii）和iii）两种情况下，认证过程都需要重新启动，直到获得符合i）的VC。E. Albert等人理论计算机科学电子笔记132（2005）1131274检查消费者在证明代码的安全性后，供应商将程序连同证书一起发送为了保持安全保证，消费者既不能信任代码，也不能信任证书。因此，在验证过程中，代码消费者不仅检查证书w.r.t.程序，但它也（重新）生成一个值得信赖的VC。本节仅描述验证过程的前一部分，因为后一部分与前一节中已经讨论过的部分相同。至少有三个原因要求验证过程是有效的，并由一个简单的算法驱动。首先，检查算法的实现是安全关键基础设施的一部分，我们希望将其最小化;其次，本地主机可能是一个小型嵌入式系统，缺乏运行大型复杂程序的计算资源。第三，检查将由每个消费者执行（而证书生成仅由供应商完成一次如前所述，分析在我们的方法中扮演着证书生成器的角色。 尽管全球分析现在被常规用作实用工具，但运行整个分析来验证证书仍然是不可接受的，因为它仍然涉及相当大的成本。其中一个主要原因是定点算法是一个迭代过程，由于进一步计算可能会引入最新数据，因此经常会（重复地）重新计算同一调用的答案。在每次迭代中，算法必须处理相当复杂的数据结构，包括执行更新、查找等。直到到达终点。整个验证过程围绕着以下观察：检查算法可以定义为一个非常简单的直观地说，定点算法的计算，如分析，可以理解为：分析=定点（分析步骤）。我们将不动点显式地写为高光，即分析可以被视为迭代过程，其重复地执行分析图的遍历（由分析步骤表示），直到计算的信息不改变，即，它到达一个固定点。这个想法是，简单的，非迭代的，分析步骤的过程可以发挥的作用，基于解释的检查。 换句话说，检查分析步骤。这是因为假设认证过程已经完成，以证书的形式显示定点结果。因此，只要答案表是有效的，附加的分析通过它-或等效的分析步骤的一个单一的执行-不能改变结果。在嵌入式系统的上下文中，Java字节码[11，10正如在PCC中所做的那样，[17]中的工作提出了KVM的分割字节码验证（KVM的嵌入式变体）。128E. Albert等人理论计算机科学电子笔记132（2005）113JVM）分为两个阶段：1）生产者通过基于类型的数据流分析器计算证书，2）然后消费者简单地检查代码证书中提供的类型是否有效。在我们的例子中，第二个阶段可以在字节码上进行一次线性传递5讨论使用抽象解释的结果进行程序验证和调试的想法例如，应用于Java虚拟机的类型级别抽象解释的数据流分析是所有现有字节码验证器的基础[11，10]。分析结果证明了程序的正确性。非平凡正确性条件CiaoPP也是如此，它将抽象的解释与灵活的解释相断言语言为抽象解释的许多用途打开了大门，程序开发。在本文中，我们介绍了一种新的方法来移动代码安全，它遵循PCC和相关技术提出的将安全证书与程序相关联的标准策略，但它完全基于抽象解释的使用。 具体而言，它在以下方面不同于PCC。在我们的例子中，通过用一个简单的基于一次遍历的抽象解释的检查器代替分析阶段，减少了消费者端的负担。证书采用抽象解释器生成的分析结果的特定切片的形式。消费者端的认证检查器本身实际上是一个非常简单和高效的专用抽象解释器。我们对检查器的定义的重要性来自于这样一个事实，即虽然抽象解释是一种强大的技术，但作为回报，它并非没有代价：它提供的结果保证是正确的，并且为了有用，通常是足够精确的，但获得分析结果是一项昂贵的任务，主要是由于必须达到分析定点的事实。另一方面，我们提出的检查器大大降低了接收方的成本。另一个值得注意的区别是，我们的方案完全在源代码级别定义，而在PCC和相关方法中，代码供应商通常将证书与不受信任的目标代码而不是源代码打包。从我们的角度来看，这两种方法都是有意义的。在许多情况下，消费者根本无法获得源代码即使在对象和源代码之间有选择，使用对象代码也有明显的优势，因为不需要编译器，所以减少了消费者的可信计算基础。 然而，开源代码 现在变得越来越重要因此，现在现实的情况是，E. Albert等人理论计算机科学电子笔记132（2005）113129预期相对大量的不可信源代码可用于消费者。我们对开源的兴趣部分是因为Ciao本身就是一个GNU许可的Prolog系统，基于源代码的可用性，可以对其进行审查和修改。开源的优势就安全性而言是重要的，因为它允许检查代码并应用强大的技术来进行程序分析和验证，这允许推断可能难以在低级编译代码处观察到的信息。这使得能够处理更多涉及的属性，从而允许更多表达性的安全策略。因此，我们与PCC分享减少消费者负载的想法，但我们的方法以不同的方式应用。致谢这项工作部分由ASAP（欧盟IST FET计划项目编号IST-2001-38059）和CUBICO（MCYT TIC 2002-0055）项目资助。部分本工作是在ElviraAlbert和Germa'nPueblatUNMsuppportedbyyrespectivegrantsfortheSecretar'aucadeEstadodeEducaci'onyUnivererrsidad es 的 一 次 调 查 期 间 进 行 的 。 ManuelHermechildoisalsosupportedbythePrince of Asturias Chair in Information Science and Technology at UNM.引用[1] A.伯纳德和P.李。证明携带代码的时间逻辑。在CADE'02的Proc.Springer LNCS，2002年。[2] M. 布鲁努格 逻辑程序抽象解释的实用框架Journal of Logic Programming，10：91[3] P. Cousot和R.库索抽象解释：通过构造或逼近不动点进行程序静态分析的统一格模型。在1977年出版的《人民出版物公报》[4] P.W.达特和J·佐贝尔逻辑程序的正则类型语言。《逻辑程序设计中的类型》，第157-187页。麻省理工学院出版社，1992年。[5] T. Fruwirth，E. 好的，先生。Y. Var d i和E. 你好，我也是。逻辑编程是逻辑编程的一种类型。在Proc. LICS[6] John P. Gallagher和Julio C.佩拉尔塔正则树语言作为程序专门化中的抽象域。高阶与符号计算，14（2，3）：143[7] M. 他是一个伟大的人，G。 Puebla，F. 布埃诺，和P。 我的天啊。 使用抽象解释（和Ciao系统预处理器）的程序开发.在SAS'03的Proc.152. Springer LNCS 2694，2003年。[8] M. Hermenegildo，G.普埃布拉湾Marriott和P. Stuckey。约束逻辑程序的增量分析。ACMTransactions on Programming Languages and Systems，22（2）：187130E. Albert等人理论计算机科学电子笔记132（2005）113[9] J. 贾巴 和M.J. 马赫约束逻辑程序设计：综述。Journal of Logic Programming，19/20：503[10] 泽维尔·勒罗伊Java字节码验证：算法和形式化。Journal of Automated Reasoning，30（3-4）：235[11] T. Lindholm和F.耶琳 Java虚拟机规范 Addison-Wesley，1997年。[12] G. Morrisett，D.沃克，K. Crary和N. Glew. 从系统F到类型化汇编语言。ACM Transactions on Programming Languages and Systems，21（3）：527[13] G. Necula 携带证明代码。 在POPL'97的Proc.ACM Press，1997.[14] G. Necula和P. Lee。一个认证服务器的设计与实现。在PLDI'98的程序中ACM Press，1998.[15] G.普埃布拉湾Mr.赫梅尼吉尔多一种用于约束逻辑程序的断言语言。约束编程的分析和可视化工具，第23-61页。Springer LNCS 1870，2000年。[16] G. Puebla和M.赫梅尼吉尔多逻辑程序增量分析的优化算法。在Proc. of SASSpringer LNCS 1145，1996年。[17] K.罗斯，E.玫瑰轻量级字节码验证。OOPSALA关于Java正式基础的研讨会，1998年。[18] R. Sekar，V.N.Venkatakrishnan，S.巴苏河，巴西-地Bhatkar和D.杜瓦尼模型承载代码：安全执行不受信任应用程序的实用方法。在SOSP'03的Proc.ACM，2003年。[19] C. Vaucheret和F.你好逻辑程序的更精确而有效的类型推理在Proc. of SAS Springer LNCS 2477，2002年。