C程序验证的类型化对象模型的健全性和完整性

理论计算机科学电子笔记254（2009）85-103www.elsevier.com/locate/entcs一个精确而高效的CErnie Cohena，1 Micha-l Moskalb，2 Stephan Tobiesb，3Wolfram Schultea，4a微软公司，关闭WA，USAb欧洲微软创新中心，德国摘要OO程序的验证通常从强类型对象模型开始，其中不同的对象/字段保证不重叠。 该模型通过消除所有不幸的是，这种模型对于像C这样的语言来说是不健全和不完整的，在这些语言中，“对象”几乎可以任意重叠。因此，对C的正确验证通常从无类型内存模型开始，其中内存只是一个字节数组然而，非类型化模型增加了大量的注释负担，并且在非类型化模型中的推理在计算上是昂贵的。我们提出了一个健全的，类型化语义的C语言，提供了注释和计算的优势，类型化对象模型，同时保持健全和完整的C语言。我们维护一个谓词来标识“有效”对象的位置，并引入不变量和证明义务，以保证有效对象被适当地反锯齿化，并且（几乎）所有对象都出现-在程序中是有效的。我们描述了这种方法在VCC中的实现（用于验证Microsoft Hypervisor的C的可靠验证器）以及由此产生的性能提升。关键词：演绎程序验证，C编程语言，内存模型。1引言在为命令式语言编写程序验证器时，一个基本的设计决策是如何对程序状态进行建模在Java和C#这样的类型安全语言中，状态由一个对象集合组成，每个对象都有自己的字段，1 电子邮件：ernie. microsoft.com2 电子邮件：michal. microsoft.com3 电子邮件：stephan. microsoft.com4 电子邮件地址：schulte@microsoft.com1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.09.06186E. Cohen等人/理论计算机科学电子笔记254（2009）85⟨⟩voidfoo（int*p，int*q）{*p = 12;*q = 42;return（*p == 12）;}intn（intp，intq）需要（p！=（q）{*p = 12;*q = 42;return（*p == 12）;}Fig. 1. 原语指针其中一些可能是指向对象的指针。因此，只有当两个指针（相同类型的）指向同一个对象时，才会出现别名。这允许状态的方便的逻辑表示，例如，作为从对象、场对到值的映射，以及容易机械化的框架公理，其中对对象的场的写入使映射在所有其他点处保持不变C从根本上背离了这种国家观首先，C没有真正的因此，在C中，对象可以任意重叠（在对象对齐的限制内）。第二，在C中，对象和场之间没有区别。一个结构可以包含另一个结构作为成员，指针可以指向结构的成员。由于这些困难，我们不能正确地将类型化（对象）表示直接用于C程序。例如，图1中的断言都不是有效的5-在每种情况下，参数可能指向重叠的存储器块。在函数bar的情况下，即使我们明确排除了指针相等的可能性，因为int类型的大小大于1，p和q指向的内存块可能部分重叠高级对象模型的另一种选择是每个类型的大小，以及结构中成员的操作集，由应用程序二进制接口给出，因此访问地址和宽度可以从类型定义中计算出来;如果两个对象占用不相交的内存范围，则它们是不相交的。然而，这种模式有几个缺点。首先，对象的不相交性更复杂：在对象模型中，两个对象别名如果它们的地址相同，而在C模型中，我们有一个更复杂的条件，取决于它们的地址和大小。其次，它大大增加了代码的注释负担。例如，在上面的示例中，我们必须添加额外的断言，以保证p和q虽然大多数现代架构都强制对齐，但流行的x86/x64并没有，因此我们在通用验证工具中没有利用对齐[15] C标准中描述的内存模型实际上是字节序列的集合，只允许在单个序列中使用指针运算这种区别与我们的目的无关。E. Cohen等人/理论计算机科学电子笔记254（2009）8587structA {shortx，y; };struct B{shortz，*pz; };struct C1 { Aa1;short w1; };struct C2{shortw2; A a2; };void baz（A*a，B* b）{a->x = 1; a->y = 2;b->z = 3;assert（a->y == 2）&&b->z == 3）;}public int findDuplicate（intfindDuplicate，intfindDuplicate）{c1->a1.x = 1; c2->a2.x = 2assert（c1->a1.x == 1）&&c2->a1.x == 2）;}voidshould_fail（C1* c1，A* a）{c1->a1.x = 1; a->x = 2;return（c1->a1.x == 1）;}图二、在类型良好的C程序中不可能重叠，除非类型允许别名是不相交的此外，这样做会导致不相交性断言的数量与对象的数量成二次方增长的情况拯救类型化内存模型的关键在于一句口号：我们维持在ghost程序状态中，一组指向“真实”国家的对象。我们的C内存模型确实保留了与对象模型的一个区别，这是因为C不区分对象和字段：如果状态包含一个类型为结构体的有效对象，那么结构体的成员也是有效对象8因此，我们的别名不变量稍微弱一些：如果两个有效对象重叠，那么其中一个是另一个的结构图1和图2中的示例在所有涉及的指针都有效的假设下进行验证。在VCC中，这种有效性是从讨论这些内存位置的所有权的前提条件中得出的（在这种情况下，所有者需要是当前执行的线程VCC的所有权系统不是本文的主题（但在其他地方有描述[6]），因此我们没有进入这些例子中所需的精确前提条件无论如何，所涉及的指针的有效性产生了所需的抗锯齿属性。例如，函数foo进行验证，因为p和q不能别名化，因为它们具有不同的类型，并且两者都不能是另一个的结构后代（因为它们都是基本类型）。函数bar验证，因为两个相同类型的对象只有在它们相同时才能别名。函数baz（图2）验证，因为a和b不能重叠（因为类型A和B在类型包含层次结构中是不相关的）。类似地，函数qux验证，因为c1和c2不能重叠（因此&c1->a1和&c2->a2不能重叠）。最后，在函数should_fail中，指针a确实可以等于&c1->a1，所以断言的验证失败。7.“（Tony Hoare）[8]这不包括比特场，见第6.3节。88E. Cohen等人/理论计算机科学电子笔记254（2009）85∗⊗⊕⊕1.1贡献我们为C引入了一个类型化的内存模型，其中指向结构的指针被解释为隐式不重叠的对象，这些对象具有隐式不相交的字段（Sect.4）。这个模型是健全的（节。5.1）和完整（第五节）。5.2）相对于无类型（C）内存模型，但对程序员和定理证明者的负担明显较低（Sect.7）。我们还展示了其他C类型（如联合，数组和位字段）是如何被合并到类型化模型中的。6.4）以及我们如何处理性能问题，如位向量推理，这通常太慢而无法验证。除了使验证更加方便和有效之外，这项工作还为将面向对象的验证技术（例如所有权和类型不变量）应用于C程序奠定了基础，如在配套出版物[6]中所述第二章玩具语言图3列出了一种玩具编程语言的结构，支持指针算术和在内存中任意位置的更新（但不包括条件，迭代或过程抽象，可以使用标准技术添加的扩展[11]）。该语言支持整数（TI）、指针（即，t是指向t的指针）和结构类型（TS，范围为S）。指针类型和指针类型统称为基元类型（TP）。 表达式（E）是无侧射的，由二进制表达式e1e2（其中是任何C二进制整数运算符），字段地址计算e ~f（在C中它将被写为&e->f），类型转换（允许指针和整数之间的转换，从而允许任意指针算术），变量引用和literal-als组成。 常量和变量被限制为无符号的64位整数（但可以用于保存具有适当类型转换的指针）。公式（Formulas）由应用于表达式的二元关系（binaryrelationships）组成。 语句（S）由断言、假设、内存写入、内存读取和类型重解释组成操作拆分和连接;程序（S）是语句的序列结构类型被定义为程序环境的一部分。我们使用struct S {f1：t1;. ;fn：tn}作为谓词，这意味着结构S是程序环境的一部分，并且包含字段f1，.，fn类型为t1，...，tn.和C一样，结构类型是非循环的，即，一个结构体S不能在任何嵌套层次包含一个类型为S的字段（但它可以包含类型为S的字段）。类型化程序S_tp（e）是这样的程序，其中在程序中发生的每个表达式e都有一个定义的类型tp（e），见图1。三是对TP的定义。语句也必须是类型化的：对于e1：=e2，我们要求tp（e1）=tp（e2）n，对于v：=e，我们要求tp（e）=tn，对于某些t∈TP，以及对于拆分e和连接e，tp（e）=tnE. Cohen等人/理论计算机科学电子笔记254（2009）8589| ·|→Σ Σ| |||由给定的字节序列;函数·nT I：：= i8|u8|I16|......这是什么？ | u64T P：：= T I|TS ∈ T S：：= S 1|......这是什么？ | Snt∈ T：：= T P|T Sf∈ F：：= f1|......这是什么？ | fme∈ E：：= E <$E |E ~ F|（T）E |V |Nψ∈Ψ * =E Es∈ S：：= assert|假设|E：= E |V：= 1000|分裂E|加入Ess∈S ：：= S; S|ϵtp（e1）= tp（e1）其中tp（e1）= tp（e2） tp（e1）∈TItp（e1~f）= t其中tp（e1）= S structS{... f：t;.. . }tp（（t）e1）tp（c）tp（v）=t=u64=u64其中t∈TP<$tp（e1）∈TP图三. 语言对于一些T。3无类型语义接下来，我们定义了我们语言的一个小步语义，其中内存被建模为字节序列（如C的传统语义）。字体的大小 ：TN是类型表示在内存中占用 我们假设原始类型的大小是已知的，例如。|u8| = 1，u64是最大的原始类型，对于每个类型t，|t|为|u64|.给定一个结构体S{f1：t1;. ;fn：tn}，我们定义S=i≤nti，即我们假设所有填充都是显式的。因为结构体是非循环的，所以大小是定义明确的设B = 0，1，...，255是字节的集合，并且B是字节序列的集合。函数·N：：N→ Bn，其中n≥0定义90E. Cohen等人/理论计算机科学电子笔记254（2009）85BB→ N返回表示E. Cohen等人/理论计算机科学电子笔记254（2009）8591<$c）=cE（）（）（）<$（t）e）=cast（<$e），t）11E E（Ⅲ）（Ⅲ）（E，B，（E）：=e;ss） （E，写e（B，PEe），）），ssi=0B<$·）→<$·）^^⊕E Br+^o=rE → B→+o|u64|.NBe1e2E=e1Ee2E1~f）E=e1）E +b+ b + t（f）（v）E=E（v）（1）E=（1）E（2）E（ E ， B ， （ assert;ss ） <$ifEthen （ E ， B ，（assume;ss） <$<$if Ethen（E，B，sselseT（E，B， （ v：=e1;ss ） <$<$ （ E[v：=read（B ， <$e1 ）P）]，B，ss）1 2 1Ee2E（E，B，（splite1;ss）（E，B，ss）（E， B，（joine1;ss）连接;连接哪里 其中tp（e）=teP=（t，e（Ⅱ）E见图4。 非类型语义学（Ⅱ）E对自然数的最低8n位进行编码的字节序列这些功能定义如下：b0，b1，.，bnN =nbi·28i阿格尔木=k对于k28n指针是一对类型和内存地址，即指针集P = T×B|u64|.一个原始指针是一个原始类型：P P= T P×B|u64|.函数o_set：F → N计算字段f与包含f的结构体的开头的距离（以字节为单位）;函数·~·：P × F → P计算结构体中字段的地址。给定结构体S{f1：t1;. ;fn：tn}，我们定义一个集合（fi）=j，则E，B，T1，ss<$D <$<$.5.2完整性完整性表明，如果非类型化内存模型中的计算终止，则类型化语义中的计算终止于相应的内存。Let[]1：S在内存访问周围添加联接/拆分并移除显式联接/拆分的转换，即：[s;ss]1=[ss]1其中s∈{joine1，splite1}[ss]1否则[1]1=1定理5.4若E，B，ss<$D<$E J，BJ，ssJ <$D，则E，B，T1，[ss] 1 <$E，B，T 1，[ ss ]1<$EE J，BJ，T 1，[ssJ]196E. Cohen等人/理论计算机科学电子笔记254（2009）85·−- -是的。 如果[ss]1d没有被卡住或出错，我们有引理5.1的对应关系。否则，ss和[ss]1之间的唯一区别是存储器访问的附加条件然而，它们总是OK的，因为对于任何新引入的连接e1，T=T1，并且对于所有其他操作，都有一个先前的连接e1。Q当在程序上使用[]1时，它消除了使用类型化推理的一个优点，它表明，当需要精度时，可以将类型化模型强制转换为非类型化模型，从而允许混合的非类型化和类型推理。6扩展在本节中，我们将讨论如何扩展我们的核心语言以捕获其他C类型和对象。但在此之前，我们调查如何序列的字节，代表原始值，映射到对象从一个自动定理证明理解的理论。一个自然的候选者将是使用固定大小的位向量作为基础理论。虽然这是非常精确的（所有的机器算术运算都是以位级精度建模的），但最终的性能并不令人满意。因此，我们决定用一种弱得多但也快得多的理论--线性整数运算来表示原始值及其相应的运算。我们映射字节se-长度为n的序列转换为28n-1到28n-1 1之间或0到28n 1之间的整数，这取决于类型是有符号的还是无符号的。我们引入函数每个整数类型t上的每个C运算符的符号。然后我们公理化所有的操作。无符号64位整数加法例如公理化如下：1996年， 0 ≤ x + y ≤ 264− 1加上u64（x，y）= x + y1996年， 0 ≤ addu64（x，y）≤ 264− 1这种公理化虽然不完整，但在大多数情况下似乎是足够的我们使用类似的技巧来公理化类型转换，只有当给定的值落在强制转换由于许多程序员错过了所有的数据流，我们在每个算术运算之前默认生成额外的断言，要求计算的值将适合目标范围。事实上，如果值符合u64的范围，那么加上u64与线性算术运算符+一致，所以所有常见的算术定律都成立。在用户想要推理超过流程的情况下，可以抑制这些断言的生成。E. Cohen等人/理论计算机科学电子笔记254（2009）8597--（1））^）×→6.1阵列我们扩展了我们的核心语言，允许在结构内部嵌入数组，就像在结构S中一 样 。f：t [n].. . . 我们将把f视为n个独立的场f[0]：t... f[n-1]：t. 因此，我们将域和表达式的集合扩展如下：F：：=. |F [N]E：：=. | E[E]tp（e1[e2]）=t其中tp（e1）=t∈ T，tp（e2）∈TIe1[e2]E=e1E+（e2EN·|tp（e1[e2]）|）嵌入和索引计算之间的关系类似于正常的字段地址计算：pq i f p∈ T<$$>q=p~f [i]<$0 ≤i ≤n <$p∈T嵌入（T，q）=p路径（T，q）=f[i]对于数组在结构体外部分配的情况，我们引入了一个参数数组类型数组：TN T，并将具有n个元素的类型t的数组视为array（t，n）的嵌入数组6.2工会对于联合，我们有额外的复杂性，在任何给定的点上只有一个字段应该被认为是类型化的。因此，对于U与场f1，...，如果我们引入n个结构类型U1，...，使用重新解释操作join和split在它们之间切换。请注意，只有在区分并的意义上使用并时才需要这样做。另一联合在C代码中的常见用法（实际上在OS代码中也相当常见）是将几个整数类型的字段（特别是位字段）解释为一个整数类型。这一点在下面介绍。6.3比特场C允许在结构化类型中定义位域，这些位域被解释为具有相应位数的有符号或无符号整数类型。由于大多数体系结构不允许直接访问内存中的任意位范围，C编译器通常将一个或多个连续的位域合并为一个无符号整数类型的底层域。对特定位域的访问将被转换为对底层域的位操作这就是为什么C不允许取位域的地址.我们扩展我们98E. Cohen等人/理论计算机科学电子笔记254（2009）85⟨⟩E其中，<$e）=<$$>e）E<$NEEB12E1 E2E1 EB±bstructX64VirtualAddress {i64PageOffset：12;//0：11>u64PtOffset：9;//12：20>u64PdOffset：9;//21：29>u64PdptOffset：9;//30：38>u64Pml4Offset：9;//39：47>u64SignExtend：16;//48：64>};unionX64VirtualAddressU{ X64VirtualAddressAddress;u64 AsUINT 64;};联合寄存器{struct{u8l，h; } a;u16ax;};图第七章一种带位域的结构、使用它的并集和几乎位域并集表达式语言，以适应额外的位操作：E：：=. | E [N：N：= E]|e 1 ± N |e1±Ntp（e1<$a：b<$）=u64其中a≤b，tp（e1）=u64tp（e1[ba：bb b：=e2]）=u64其中a≤b，tp（e1）=tp（e2）=u64tp（e1±b）=i64，其中b >0，tp（e1）=u64其中为了简单起见，我们假设仅64位基础字段。操作e1a：b从e1中提取a和b之间的位（包括a和b）;操作e1[a：b：=e2]用e2替换e1中a和b之间的位b;操作e1±b执行从b到64位的符号扩展。形式上：e=（e）Ndiv2a）mod2b−a+18=ifNb−1BE（e ）E（e）2然后（e）PdOffset;tmp：=p~bf0;q：=tmp 21：29p->PdOffset = x;tmp：=p~bf0;p~bf0：=tmp[21：29：=x]*q = p->PageOffset; tmp：=p~bf0;q：=tmp0：11±12p->PageOffset = x;tmp：=p~bf0;p~bf0：=tmp[0： 11： =（u64）x]为了释放涉及位域的公式，我们一直在使用固定大小位向量算术的决策过程。但事实证明，这种方法给SMT求解器带来了很大的负担，甚至对于中等复杂度的问题也会导致不可接受的性能。EE. Cohen等人/理论计算机科学电子笔记254（2009）8599ΣΣ为了拯救我们，事实证明，位域通常只用于相关信息的紧凑存储或精确映射硬件数据结构。因此，位域和算术之间的相互作用相当罕见。(What是页表条目的总结点因此，我们公理化了位选择和级联：0≤n2b−ava：b：=na：b=n−2c−b≤k2c−b<$（v[b：c<$：=（u64）k]b：c<$）±c−b+1=kbJ

下载后可阅读完整内容，剩余1页未读，立即下载