对区块链技术感兴趣的话，或许听说过很多进犯者利用程序代码中的缝隙而导致的大量资金被盗事情。例如，2016 年臭名昭著的 DAO 进犯事情，进犯者利用一个名叫「重入」的缝隙超量提取了他们本来所能提取的资金。另一个更近期的事情是闪电贷进犯，发生于 2022 年 4 月 17 日，形成 1.82 亿美元的资金损失。虽然一切进犯都源于底层源代码的安全缝隙，但好消息是现在已经有可以检测此类缝隙的程序剖析技术。在接下去的几篇博文中，咱们会解释程序剖析是什么，以及它怎么协助在布置前捕获安全缝隙。
程序剖析简介
程序剖析指的是一类用于检测程序中安全缝隙的技术。程序剖析有两种首要方式，动态和静态。动态程序剖析的目标是经过执行程序来检测问题，而静态程序剖析则无需运转程序自身就可以对源代码进行剖析。但是，在这些技术之中，只要静态剖析可以保证程序中不存在缝隙。相反，不同于静态剖析，动态剖析能证明问题的存在，它并不可以证明缝隙并不存在。
乍一看，静态剖析听起来好像很神秘：外表看来，静态剖析好像违反了一个被总结为莱斯定理「Rice's theorem」的基本原则，该定理声称程序的每一个非普通性质都是不可判定的。在此，语义特点是关于程序行为的特点（与语法特点不同），而非普通性质是指只要某些程序具有而其他程序没有的性质。与咱们手头论题更相关的是，安全缝隙的存在是非普通性质的一个典型比如。因而，关于「这个程序是否存在安全缝隙」这一问题，莱斯定理告诉咱们没有一个算法可以完结并精确答复这一问题。
那么，静态剖析的可行性源自哪里呢？答案藏于以下的调查：没错，没有一个算法可以精确地给出是或否，但可以有一个算法在程序有安全缝隙时总是会答复「是」，在程序没有安全缝隙时算法有时或许也会答复「是」。换句话说，只要咱们愿意容忍一些误报，咱们就可以绕过赖斯定理和不可判定性。
静态剖析原理
让咱们以高一维度的视角来看看静态剖析是怎么运作的。静态剖析的基本原理是将程序所处的状况调集进行过近似「over-approximate」。咱们将程序状况视为从变量到值的映射。一般来说，不存在一个算法可以清晰也许是执行某一程序引起的确切程序状况集。但可以近似该调集，如下图所示：
此处，蓝色的不规则形状对应在执行某些程序时或许出现的实践状况集，赤色区域对应预示过错或安全缝隙的「坏状况」。因为不可判定性，永远没有一个算法可以精确标明蓝色区域究竟是什么，但是咱们能规划一个算法以系统性的方式过近似这个蓝色区域，如上面常规绿色区域所示。只要绿色和赤色的交集为空，咱们就有依据证明程序没有做坏事。但是，如果咱们的过近似不够不精确，或许会使得赤色区域堆叠，即使蓝色和赤色区域的交集依旧为空，如下图所示：
这种状况会导致所谓的「误报」，因为剖析与真实问题不相应而陈述的虚伪过错。一般来说，静态剖析的圣杯是构造过近似，即 （1）过近似满足精确因而咱们在实践中不会取得很误报 （2）过近似的核算满足有用率，因而剖析可扩展到咱们所关心的现实世界的程序。
附带说明一下，还可以规划静态剖析算法来近似如下所示的程序行为：
在此状况下，绿色区域（经过静态剖析核算）包含在蓝色区域内（表示实践状况），和另一种方式正好相反。这种剖析是不牢靠的，意味着或许会漏掉真实的程序过错：正如咱们在上图所看到的那样，绿色和赤色的交集为空，因而即使程序真的存在缝隙，剖析也不会陈述问题。这会导致所谓的假阴性，真实的缝隙被静态剖析给遗漏了。
大体来说，如果咱们想取得可证明的安全性，咱们会想要牢靠的从来不会有误报的静态剖析器，一起还需要满足精确，在实践时不会陈述太多误报。但是，好消息是，几十年的正统研讨标明规划这样的静态剖析器有或许的。下篇博文，咱们会更具体地介绍静态剖析器具体是怎么运作的！
总结
程序剖析是一种有用的可以捕捉各种程序中安全缝隙的技术，包括区块链应用程序。此外，牢靠的静态剖析器的过近似程序行为能保证整个类别中不存在缝隙。
评论