GPU程序的静态分析与不安全类型转换的检测方案，有效降低了虚警，适用于CUDA SDK

可在www.sciencedirect.com在线获取理论计算机科学电子笔记317（2015）33-45www.elsevier.com/locate/entcsGPU程序的不安全浮点到无符号浮点转换检查1Wei-Fan Chiang2，Ganesh Gopalakrishnan，andZvonimirRa ki'c3犹他大学计算机学院关闭MT，USA摘要数值程序通常包括类型转换指令，这些指令在不同类型之间转换数据。识别不安全的类型转换对于防止导致严重问题（如安全漏洞和结果不可再现性）的未定义程序行为非常重要。虽然已经提出了许多工具来处理顺序程序，但据我们所知，还没有一个工具适合GPU。在本文中，我们提出了一个静态分析为基础的方法，指出所有潜在的不安全类型转换指令在程序中。 为了减少虚警（通常由静态分析引起），我们采用了两种技术，手动提示和预定义的函数合同，我们的经验表明，这些技术在实践中是有效的。我们使用CUDA SDK中的人工程序和样本对我们的方法进行了评估。我们的实现目前正在集成到一个GPU程序分析框架称为GKLEE。我们计划在未来的工作中集成动态不安全类型转换检查关键词：不安全铸字检查，数值程序分析，静态分析，GPU程序分析1介绍许多数值程序，包括用于物理模拟[19，17]和图像处理[19，10]的程序，都是通过支持高并行性的图形处理单元（GPU）来加速的正确性检查因此成为GPU程序开发的一个重要问题。以前的工具已经包含了在大量线程、分层内存空间和线程调度存在的情况下进行数据竞争检查的正式方法[14，15，5，7]。直接影响值完整性的一个问题是不安全的类型转换检测。然而，这方面在过去没有受到太多关注在本文中，我们将重点关注这个问题，并提供基于静态类型的简单实用的解决方案1由NSF CCF 7298529和13467562部分由美国能源部奖号10034350支持3如有任何问题或意见，请电邮至Wei-Fan Chiangwfchiang@cs.utah.eduhttp://dx.doi.org/10.1016/j.entcs.2015.10.0051571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。34W.- F. Chiang等人/理论计算机科学电子笔记317（2015）33意外的不安全强制转换可能会导致严重的问题，包括安全漏洞[3，4]或与CPU代码相关的结果差异[24]。问题的核心原因是在某些情况下，铸造结果变得不确定。例如，从一个负的浮点数（例如-1.0）转换为一个无符号整数（例如C语言中的unsigned int类型）是不安全的/未定义的，这意味着程序被允许在这个转换操作上（甚至之后）做任何事情。然而，检测不安全的类型转换是困难的，因为不安全的场景只能在特定条件下触发在上一个示例中，在浮点到无符号整数（FP2UI）操作中触发不安全场景的条件是参数值必须为负。在本文中，我们关注不安全类型转换的一个特殊情况，即不安全FP2UI转换。具体来说，我们检测到将负浮点数转换为无符号整数的情况。（检查其他不安全的类型转换场景（如overload）可以通过其他工具（如即将引入的IOC）进行辅助（见第2节） FP2UI操作广泛应用于许多GPU软件中，先前在实际GPU并行医疗软件中报告的不安全FP2UI的漏洞[24]。不幸的是，据我们所知，目前基于动态符号分析的GPU程序检查器GKLEE最初被提出用于数据竞争检测[15]。最近，它已经扩展并集成了许多技术来解决各种正确性问题，例如原子性检查[7]和对称线程识别[16]。这些扩展表明，GKLEE是一个强大的通用GPU程序正确性检查框架。本文提出了一种用于检测FP2UI不安全铸造的静态分析方法，并将该方法集成到GKLEE中实现鉴于GKLEE目前专注于处理CUDA GPU程序[20]，我们的实现目前仅限于处理CUDA。我们的静态分析方法跟踪可能的负值（整数和浮点数），并检查FP2UI转换中是否使用了任何此类值。我们的方法是保守的。 这意味着不安全FP2UI的错误警告可能复活我们采用两种技术来减少错误警报：手动提示和预定义函数契约。手动提示允许我们的方法与外部源（如用户或其他分析器）进行通信。预先定义的函数合约允许我们的方法在高级抽象中跟踪可能的负值，而不是探索源代码级别的细节。这大大提高了分析的准确性。此外，这种技术允许我们的方法来处理动态链接例程的源代码是不可用的。我们工作的贡献可归纳如下：• 我们实现了一个静态分析的不安全FP2UI铸造检测，这是适用于GPU程序和实现被集成到一个GPU程序检查框架称为GKLEE。• 我们研究了减少错误警告的技术，包括手动提示和预先定义的函数契约。我们通过CUDA SDK中的实际例子表明这些技术在实践W.- F. Chiang等人/理论计算机科学电子笔记317（2015）33352相关工作用于检测顺序程序的不安全类型转换的工具已经在许多以前的上下文中提出。这些工具可以分为三类：动态，静态和动态符号。动态工具检测程序并设置条件以在运行时检查类型转换参数。IOC [9]和BRICK[6]是动态方法的例子。这些工具不会产生假警报;但是，检测覆盖率取决于用户提供的测试输入静态分析工具执行类型推断。 IntScope [23]和我们的分析器就是这种例子。与动态方法相比，静态方法保证覆盖率，但可能会引发错误警报动态符号分析类似于白盒模糊测试[11]，由一些初始输入驱动。这些工具自动生成新的输入以增加测试覆盖率。SmartFuzz [18]属于这一类。这些工具的测试覆盖率和可扩展性可能受到底层约束（SMT）求解器的限制3方法3.1非负值的保守跟踪我们静态分析的关键思想是跟踪非负值，并检查是否有任何类型转换表达式将可能的负值作为参数。图1显示了我们的静态分析所处理的程序的核心语法。在这种语法中，我们省略了实际CUDA（或C）程序中的许多实际数据类型例如8位整数（C语言中为char）和64位浮点数（C中为double保留的程序类型（ptype）是bool，int，unsigned int和unsignedint，这些是程序员允许在程序中声明的类型为了简单起见，我们还省略了语法中的关系操作，如小于（）和大于（>）。为了跟踪非负值，我们的分析器在后台扩展程序类型（ptype）。图2显示了我们分析中使用的类型。具体来说，我们在ptype之上添加了两个额外的类型，非负int和非负int。类型非负int（或非负浮点数）用于声明为int（或浮点数）但其值为非负的整数（或浮点数）。另一方面，类型int和int oat（在图2中）用于值可能为负的变量非负值（包括非负int类型和非负整型值）由常量赋值创建。由于我们的方法是基于静态分析的，因此一些非负值可能被保守地推断为int或numeroat。我们将在3.2节中介绍一些减少保守推论的技巧。我们使用符号expr：T来表示类型为T的表达式expr。在图3中，规则1至5显示了二元运算求值的语义，规则6至36W.- F. Chiang等人/理论计算机科学电子笔记317（2015）33程序=语句statement = statement语句|variable = expression ;expression=expression bop expression|(ptype)expression|func(exp 0, 实验1，.）|(exp cond? 实验0：实验1）|variable|value◦ 表示级联二进制运算类 型 转 换 函数调用phi节点BOP=+ - * /等等二元运算符ptype=bool程序|||unsigned intint奥索特Fig. 1.基本程序type = ptype|non-negativeint|non-negativefloat图1中为非负数对于值为非负数的浮点数（一）（二）（三）（四）（五）图二.我们的不安全类型转换检查基本二进制操作所使用的扩展类型：实验0：T bop实验1：T。bop∈ {+，，/}实验相对值：T整数减法：实验0：T −实验1：T. n ∈ {unsigned int，non-negative int，int}exprel：int减涂点： 实验0：T −实验1：T. T ∈ {非负方向，方向}实验相关性：exp0：非负整数 国际收支指数1：整数二进制运算整数推断：exprel：intexp0：非负偏置 国际收支平衡表1：原油二进制运算的浮点推理：实验相关性：（六）基本Phi节点：（expcond：bool？实验0：T：实验1：T）实验相对值：T（七）Phi节点整数推断：（expcond：bool？ exp0：非负整数 ： exp1：int）exprel：int（八）Phi节点的浮动点推断：W.- F. Chiang等人/理论计算机科学电子笔记317（2015）3337（expcond：bool？ exp0：非负偏置 ： 实验1：燕麦）实验相关性：图3.第三章。GKLEE中二进制运算和Phi节点的运算语义图8显示了Phi节点求值的语义。所有的语义规则都是对称的：一个规则可以应用于交换两个操作数的类型的情况。规则4、5、7和8显示了在我们的静态分析中执行的保守类型推断图4显示了类型转换的语义。强制转换的原则是，将非负值强制转换为可能为负的类型（int或non-negative）将导致非负类型（non-negative in或non-negativenon-negative）。规则15和20中的表达式警告表示潜在的不安全类型转换。具体来说，规则20描述了我们在这项工作中关注的不安全的FP2UI场景警告38W.- F. Chiang等人/理论计算机科学电子笔记317（2015）33（九）基本型铸件：（T）expop：T实验相对值：T（十）unsigned int到int：（int）intcount：intexprel：non-negative int（十一）unsigned int到unsigningpoint：（可选）expop：unsigned int经验相对于：非负样本（十二）non-negative int到unsigned int：（unsigned int）expop：non-negativeintexprel：unsigned int（十三）非负int到int：（int）numerous intexprel：non-negative int（十四）non-negative inttonon-pointingpoint：（可选）expop：non-negativeint经验相对于：非负样本（十五）unsignedint：（unsigned int）expop：int警告（十六）int到重定向点：（可选）expop：int实验相关性：（十七）non-negativeunsigned int：（unsigned int）expop：非负整数exprel：unsigned int（十八）非负向整型：（int）expop：非负整数exprel：non-negative int（十九）非负电压转换为正电压（非负）指数：非负指数经验相对于：非负样本（二十）unsigned int（unsigned int）expop：int警告（二十一）转换为int：（int）intsumexprel：int见图4。 类型转换语义W.- F. Chiang等人/理论计算机科学电子笔记317（2015）3339如果这些规则之一被触发，我们的分析器将给出不安全类型转换的消息，并且程序可能有未定义的行为。3.2优化我们的静态分析遵循保守地推断值类型的语义（图3和图4）。在没有应用任何优化的情况下，我们的分析器往往会发出许多错误的警报：对安全类型转换发出警告。在这里，我们描述了在我们的分析器中应用的一些优化，我们将通过§4中的示例展示如何消除假警报。手动提示用户我们当前的实现为程序员提供了一个接口，可以手动声明非负表达式。40W.- F. Chiang等人/理论计算机科学电子笔记317（2015）33（二十二）（二十三）绝对值：abs（exp：T）。T ∈ {non-negativefloat，float}经验相对于：非负样本向量长度：长度（exp0：T，exp1：T，.）的。 T ∈ {非负方向，方向}经验相对于：非负样本（二十四）上限值：ceil（exp：非负对数）经验相对于：非负样本（二十五）门值：地板（exp：非负地板）经验相对于：非负样本（二十六）max（exp0：T0，exp1：T1）。取最大值：T0 =非负向振荡T1 =非负向振荡经验相对于：非负样本（二十七）取最小值：最大值（实验0：非负振荡，实验1：非负振荡）经验相对于：非负样本图五. 使用预定义函数契约的预先定义的函数合约我们目前实施类型转换检查以执行函数分析。类型信息不在函数之间传递。换句话说，为了处理任意函数调用表达式，我们只需检查函数声明中描述的返回类型。例如，让函数foo浮动→浮动。函数调用表达式foo（1. 0）将被认为可能是负面的，即使foo的实际实现可能是floatfoo（floatf）{return f;}表达式foo（1. 0）实际上是非负的。我们发现，将预先定义的函数契约（如某些数学例程的抽象公理）纳入类型转换检查的考虑可以大大减少误报。例如，许多编程框架（如CUDA）提供了函数abs，它将一个浮点值作为参数并返回绝对值。显然，abs的返回值总是非负的。图5显示了为某些函数调用表达式推断非负的非负类型的语义图5中未列出的函数调用计算仅引用函数声明。3.3当前限制在这一点上，我们只有静态分析方法的原型实现。正如我们将在第4.2节中看到的一个例子，有许多CUDA（或C语言）语法，如结构和指针数组，我们目前的实现无法处理。在我们当前的实现中也没有实现跨函数分析我们将在未来的工作中完善我们的实施工程。W.- F. Chiang等人/理论计算机科学电子笔记317（2015）3341对于处理分支语句，我们目前认为每条路径都是可行的，42W.- F. Chiang等人/理论计算机科学电子笔记317（2015）33在联接位置，根据所有传入路径保守地推断类型。用于处理分支的语义类似于规则6、7和8，它们是处理Phi节点的语义。在我们未来的工作中，我们计划调用GKLEE的识别不可行路径的功能，这将提高我们的不安全类型转换分析的准确性。对于处理循环，我们简单地执行展开。与固定点理论的整合[12]也在我们的计划中。4实验结果我们收集了一些示例来评估我们的不安全FP2UI检测。在§4.1中，我们证明了我们的方法可以成功地报告我们创建的一些人工基准测试在§4.2中，我们证明了我们的方法在实践中可以避免报告假警报第4.2节中使用的示例摘自CUDA SDK（6.0）。我们所有实验的程序（在§4.1和§4.2中）都是用Clang [1]编译的，优化了Clag-O0。GKLEE的CUDA程序到C语言的转换功能为Clang编译CUDA程序提供了支持.我们的实验是在一台装有12个Intel Xeon 2的机器上进行的。40GHz CPU和48GBRAM。4.1不安全铸型检测演示图6显示了两个人工（CUDA）函数，它们展示了不安全的FP2UI使用。在图6a中，第7行上的断言确保来自参数数组数据的所有浮点值都是非负的。这个信息（由断言描述）作为手动提示传递给我们的静态分析在我们对图6a中第8行（第9行被注释掉）的程序进行的实验这是因为（fp0 +fp 1）被认为是非负的，而（fp2−fp 3）被认为是可能为负的（根据规则3）。因此，Phi节点的评估结果（myid256？<（fp0+fp 1）：（fp2−fp 3））可能是负数（根据规则8）。如果将第8行与第9行交换，则两个传入表达式都是非负的。因此，我们的分析仪没有发出警报图6b示出了调用用户定义函数（fAdd）和数学例程（abs和ceil）的示例，其中数学例程具有如图5所示的预定义合约。 在我们对图6b中的程序进行的实验中，第8行（第8行）9注释），第10行FP2UI发出警报。原因是函数fAdd因此，fp2因此，第10行上的FP2UI可以从负值转换。如果将第8行与第9行交换，则通过调用abs（计算绝对值）触发规则22因此，fp2W.- F. Chiang等人/理论计算机科学电子笔记317（2015）3343≤1 ： 程 序 全 局FOO （ unsigned int results ） 2 ： int myid =threadIdx.x;第三节：intfp0 = data[myid * 4 + 0];第四章：返回fp 1 = data[myid * 4+ 1]; 5：fp2 = data[myid * 4 + 2];6：7：assert（0 fp0，fp1，fp2，fp3）;第八章：results[myid]=（unsigned int）（myid 256？< (fp0+fp1）：（fp2 - fp3））;9：// results[myid] =（unsigned int）（myid 256？<(fp0+ fp 1）：（fp 2 + fp3））; 10：结束过程(a) 基本二进制运算和Phi节点1：过程装置ADD（参数arg0，参数arg1）2：返回arg 0 + arg 1;第三节： 结束程序4：程序全球BAR（unsigned int results）5：intmyid = threadIdx.x;6：调用fp 0 = data[myid];7：选择fp 1 = data[myid + blockDim.x]; 8：选择fp 2 = fAdd（fp 0，fp 1）;9：//确定fp 2 = abs（fAdd（fp 0 + fp1））; 10：results[myid]=（unsigned int）ceil（fp 2）;11：结束过程(b) 函数调用见图6。 演示不安全类型转换检测4.2CUDA SDK示例研究了CUDA SDK中FP2UI强制转换的一些用法，并将实例分为两个场景：线程组大小计算和信息压缩。我们手动分析了FP2UI的所有使用情况，发现它们都是安全的。我们的分析器在CUDA SDK的所有示例中只发出了一个警报（假警报）。在许多示例中，我们观察到简单的手动提示和预先定义的合同可以帮助我们的分析器避免发出错误警报。计 算 线 程 组 大 小 图 7 显 示 了 从 程 序 simpleZeroCopy 、 FDTD3d 和cdpBezierTessellation中提取的代码 。图7a 显示了在simpleZeroCopy中使用FP2UI转换（第5行）来决定网格中线程块的数量我们的分析器声称这种用法是安全的，因为它传播了来自nelem（1048576）和block.x（256）的非负常数，并发现（根据规则1）（浮点）nelem/（浮点）block.x函数ceil的值是非负的（根据规则1）。因此，FP2UI在第5行强制转换所取的浮动点值是非负的（根据规则24）。图7b显示了在FDTD3d中使用FP2UI转换（第9行和第10行）来决定网格尺寸。函数调用checkCmd（）检查是否存在通过命令行给定的任何用户指定的块大小，函数调用getUserBS（）返回用户指定的块大小。我们的分析器成功地推断出整数userBlock- Size是非负的（第4行）。它首先决定max和min必须返回一个非负整数（根据规则26和27），然后决定第4行上的Phi节点在非负整数和常数512之间进行选择。因此，第5行和第6行的SI2UI（有符号整数到无符号整数）转换都是安全的。第1行的手动提示断言dimx和dimy都是非负的，我们的分析器声称FDTD3d44W.- F. Chiang等人/理论计算机科学电子笔记317（2015）33----≤}1：procedureMAIN（）intnelem = 1048576;3：unsigned intbytes = nelem * sizeof（int）;4：dim3块=1，1，256;5：dim 3grid = 1，1，（（unsigned int）ceil（（unsigned int）nelem /（unsigned int）block.x））; 6：结束过程(a) simpleZeroCopy1：procedureFDTDGPU（intdimx，intdmy）2：assert（0 dimx，dimy）;3：dim3dimBlock，dimGrid;4：intuserBlockSize =（checkCmd（）？ min（max（（getUserBS（）/ 1024），128）：512））;5：unsigned intdbx = 32;6：unsigned intdby =（（（userBlockSize/32）16）？<（userBlockSize/32）：16）; 7：dimBlock.x = dbx;8：dimBlock.y = dby;9：dimGrid.x =（unsigned int）ceil（（unsigned int）dimx/dbx）;10：dimGrid.y =（unsigned int）ceil（（unsignedint）dimy/dby）; 11：结束过程(b) FDTD3d1：#defineN LINES 2562：#defineBLOCK DIM 64第三节： 结构BezierLine4：燕麦2CP[3];5：顶点2 *顶点位置;6：intnVertices;第七章：MAIN（）8：BezierLine *bLines;9：//在这里初始化bLines...10：unsigned intdGrid =（unsigned int）ceil（（bLines）N LINES /（bLines）BLOCK DIM）; 11：computeBezierLinesCDP dGrid，BLOCK DIM>（bLines，NLINES）;12：结束程序1：程序全球(c) cdpBezierTessellation：main计算BEZIER直线CDP（BezierLine *bLines，intnLines）2：intlidx = threadIdx.x + blockDim.x * blockIdx.x; 3：BezierLinebl = bLines[lidx];4：曲率=长度（b1.CP [1] - 0.5 *（b1.CP [0] + b1.CP [2]））/长度（b1.CP [2] -b1.CP [0]）; 5：intnTessPoints = min（max（（int）（curvature * 16.0），4），32）;6：ifbl.vertexPos == NULLthen bLines[lidx].nVertices = nTessPoints; 7：unsigned intdGrid =（unsigned int）ceil（（unsigned int）bl.nVertices/ 32.0）; 8：computeBezierLinePositions dGrid，32>（lids，bLines，bl）;九： 结束程序(d) cdpBezierTessellation：computeBezierLinesCDP图第七章CUDA SDK示例中用于计算线程组大小的代码（摘录）是安全的程序cdpBezierTessellation中有两段代码使用FP2UI铸造。这些部分如图7c和7d所示。图7c定义了BezierLine结构和两个代码部分中使用的常量。图7c中所示的FP2UI投射的使用类似于图7a的情况（恒定传播）。对于图7 d中的用法，我们的分析器成功地推断出第4行的cur- vature必须是非负的浮点值（根据规则23），第5行的nTessPoints必须是非负整数。然而，我们的分析器目前无法推断网格大小（dGrid）必须通过从一个非负的浮点数，因为我们当前的实现在这种情况下，需 要 跟 踪 的 结 构 体 是 bLines[lidx].nVertices 。 此 外 ， 目 标 结 构 成 员（bLines[lidx].nVertices）的值在此函数的if-语句（第6行）为了解决这个问题，跨职能分析是{W.- F. Chiang等人/理论计算机科学电子笔记317（2015）3345|||1：程序装置unsigned intRGBAFLOAT TO INT（rgba）2：rgbasx= saturate（rgba.x）;3：饱和sy =饱和（rgba.y）; 4：饱和sz =饱和（rgba.z）; 5：饱和sw=饱和（rgba.w）;6：unsigned intinfow=（（unsigned int）（sw * 255.0f）24）;7：unsigned intinfoz=（（unsigned int）（sz * 255.0f）16）;8：unsigned intinfoy=（（unsigned int）（sy * 255.0f）8）;9：unsignedint infox=（（unsigned int）（sx *255.0f））;<<<<<<10：返回infow infoz infoy infox; 11：结束过程见图8。 用于信息压缩的类别基准手动分析发现不安全FP2UI发现不安全的FP2UI，无选件不安全的FP2UI发现与选择。应用优化公司简介二进制运算φ节点YYY手动提示函数调用YYY预定义合同CUDASDK简单零拷贝NYN预定义合同FDTD3dNYN预先&定义的手动提示合同cdpBezierTessellationNYN预定义合同info. 压实NYY预定义合同表1我们的实验结果手动分析发现的不安全FP2UI列指示基准是否包含任何不安全FP2UI转换。列Unsafe FP 2UI Foundwith/without Opt.指示我们的静态分析是否使用/不使用优化技术引发了不安全的FP 2UI警告。Y（N）表示找不到不安全的FP2UI。“应用的列优化”指示应用于“使用Option找到的列不安全FP2UI”中显示的结果的优化技术。.这是我们目前没有实现的。我们计划在未来的工作中修改我们的实现，以处理更多的C（或CUDA）语法，如结构和处理跨功能分析信息压缩图8显示了boxFilter和bilateralFilter程序中使用的代码，这些程序用于将存储在Data4中的颜色信息压缩为一个无符号整数。 函数saturate将浮动点值固定到范围[0。0，1。0]，可以解释为饱和（f p）= max（0. 0，min（1. 0，f p））根据规则26和27，第2行到第5行的sw、sx、sy和sz都是非负的浮点值。因此，6至9号线上的铸件都是安全的。表 1 总 结 了 我 们 所 有 的 实 验 结 果 。 列 Unsafe FP2UI Found by ManualAnalysis显示手动不安全FP2UI转换分析的结果如果基准包含（不包含）不安全的FP2UI转换，则用标签Y（N）标记基准。列Unsafe FP2UI Found without Opt.显示了我们在没有应用任何优化技术的情况下的静态分析结果。如果我们的分析器在基准测试中检测到（没有检测到）一个潜在的不安全的FP2UI转换，那么基准测试将被标记为标签Y（N）。ColumnUnsafe FP2UI Found with Opt.显示了应用了一些优化技术的静态分析结果。表1的最后一列详细说明了所应用的优化技术。列应用的优化显示了应用于46W.- F. Chiang等人/理论计算机科学电子笔记317（2015）331：过程voidFF（uint4 *td，inti，uint4 *Fr，unsigned int *data）2：unsignedt = sin（（unsigned）（i））* p;3：unsigned inttrigFunc =（unsigned int）t;4：结束过程(a) CUDPP中的潜在不安全FP2UI（rand gold.cpp）1：程序DEVICEvoidFF（uint4 * td，int i，uint4 * Fr，unsigned int * data）2：unsigned t = sin（int as unsigned（i））* p;3：unsigned inttrigFunc =Ammoat 2uint rd（t）; 4：结束程序(b) CUDPP中的安全FP2UI（rand cta.cuh）图第九章CUDPP中的潜在不安全和安全FP2UI类型转换结果显示在使用Option发现的列不安全FP2UI中。.4.3CUDPP中的潜在不安全FP2UICUDPP [2]是一个GPU计算库，它提供了许多并行算法原语，如prefix-sum [13，21]，排序[8]和随机数生成[22]。我们使用我们的静态分析来检查CUDPP的最新版本（2.2），并在其中发现了一个潜在的不安全FP2UI。潜在的不安全FP2UI已报告给CUDPP开发人员，但我们的发现尚未在本文的提交截止日期前得到确认。(Thus，我们声称我们的发现是一个潜在的不安全类型转换场景。）图9a显示了函数（FF）的提取代码，其中包含CUDPP的filerangold.cpp中潜在的不安全FP2UI转换。当变量t的值（在图9a中）为负时，第3行中的FP2UI的结果是不确定的。事实上，当t大于unsigned intvalue的最大限制时，代码可能会从另一个不安全的类型转换sce- nario中继承。(This不安全类型转换的类型不在本文的重点之列。）然而，我们在CUDPP中发现了另一个文件rand cta.cuh，它定义了与rand gold.cpp中类似的函数，包括图9a中所示的（潜在）有问题的函数。图9b显示了图9a中函数的安全类型转换版本（定义为rand cta.cuh）。在图9b中，类型转换由CUDA库例程，int as cuboat和cuboat2uint rd保护，它们使用前面的上下文中建议的安全类型转换方法[24]。4.4讨论：潜在集成与动态分析我们的静态分析仪目前已与GKLEE集成。如第3.3节所述，我们计划在未来的工作中调用更多GKLEE的设施，例如路径可行性检查，以提高检测准确性（以减少误报）。在这里，我们提出了一个与IOC [9]的潜在集成：一个动态的不安全类型转换检查器。IOC可以检查不安全的类型转换场景，例如我们目前的静态分析方法无法处理的overload。此外，IOC为每个类型转换指令插入代码，如果在运行时触发任何不安全的转换，则被检测的程序生成警告。换句话说，IOC不仅动态地检测不安全的强制转换，而且还合成不允许沉默的未定义行为的安全程序。但是，插装会导致性能开销。我们的静态分析器可以为IOC选择可能不安全的类型转换指令，W.- F. Chiang等人/理论计算机科学电子笔记317（2015）3347插入安全检查代码。与单独使用IOC相比，这种组合由于插入了较少的安全检查代码，因此可以合成性能更高的程序。5总结发言检测不安全的类型转换对于GPU程序开发非常重要。本文提出了一种基于静态分析的不安全类型转换检测方法，并实现了与GPU程序分析器的原型集成。我们的经验表明，我们的方法可以避免在实践中报告许多假警报。我们计划在未来的工作中调用符号分析来提高检测精度，并与程序合成相结合来生成低开销的安全程序引用[1] Clang：a C language family frontend for llvm，http://clang.llvm.org/.[2] CUDPP，http://cudpp.github.io/。[3] Cve-2002-0639 ： 在openssh 中的sshd 中的 重写（ 2002 ） ，http://cve.mitre.org/cgi-bin/cvename 。cgi？名称=CVE-2002-0639。[4] Cve-2010-2753：mozilla firefox、thunderbird和seamonkey中的overflow，http://cve.mitre。org/cgi-bin/cvename.cgi？名称=CVE-2010-2753（2010）。[5] Betts，A.，N. Chong，A. F. Donaldson，S. Qadeer和P. Thomson ，GPUVerify：GPU内核的验证器，在：OOPSLA，2012年。[6] 陈佩，Y. Wang， Z.辛湾，澳-地Mao和L. Xie，Brick：一个用于运行时检测和定位基于整数的漏洞的二进制工具，在：可用性，可靠性和安全性，2009年。ARES'09。国际会议，2009年，pp。208-215[7] Chiang，W.，G. Gopalakrishnan湾Li和Z. Rakamaric，Formal analysis of GPU programs with atomicsvia concilient-directed delay-bounding ， NASA Formal Methods ， 5th International Symposium ，（NFM），2013，pp. 213-228[8] Davidson，A.，D. Tarjan，M.加兰和J. D. Owens，Eachcient parallel merge sort for fixed and variablelength keys，in：Innovative Parallel Computing（InPar），2012，pp. 1-9.[9] Dietz，W.，P. Li，J.Regehr和V.Adve，Understanding integer over integer in c/c++，in：ICSE，2012。[10] 埃克隆德，A.，P. Dufort，D. Forsberg和S. M. LaConte，GPU上的医学图像处理-1073-1094年。[11] Godefroid，P.，M. Y. Levin，D. A. Molnar等人，自动白盒模糊测试。见：国家社会保障局，2008年，第100页。151-166.[12] Granas，A. Dugundji，[13] 哈 里 斯 ， M. ， S. Sengupta 和 J.D. Owens ， Parallel prefix sum （ scan ） with cuda ， GPU gems3（2007），pp. 851-876[14] Li，G.和G. Gopalakrishnan，基于SMT的GPU内核功能可扩展性验证，FSE，2010年，第100页。187-196.[15] Li，G.，P. Li，G.萨瓦亚湾戈帕拉克里希南岛Ghosh和S. P. Rajan，GKLEE：Concolic Verificationand Test Generation for GPU，PPOPP，2012，pp. 215-224.[16] Li，P.，G. Li和G. Gopalakrishnan，参数化流：cuda程序中种族符号分析的自动行为等效，在：高性能计算，网络，存储和分析，2012年，第29页。[17] 刘伟，B.Schenches，G.Voss和W.Müller-Wittig，Accelatingmoleculardynamicssimulationsusinggraphics processing units with cuda ， Computer PhysicsCommunications 179（2008），pp. 634-64148W.- F. Chiang等人/理论计算机科学电子笔记317（2015）33[18] Molnar，D.，X. C. Li和D. Wagner，Dynamic t