硬核国产代码审计工具Pinpoint介绍
简介
Pinpoint是由国内源伞科技所研制的一款静态代码审计工具，源伞科技公司是香港科技大学安全实验室的众多博士创建的，产品集成了实验室多年的研究成果，在众多国际*学术会议上都发表了成果论文，在学术界有很大的影响。近几年源伞科技将静态代码检测产品Pinpoint成功商业化，目前产品已经比较成熟，能够方便的集成各种安全开发流程，操作界面流畅。能够直接扫描JAVA的二进制文件，在Java和c/c++两种语言上的分析能力十分强大，扫描速度普遍快于市面上现有的产品，且拥有众多国内一线互联网以及金融公司的安全开发实例经验，不仅能够输出工具产品，也能够提供安全开发的解决方案，在国内静态代码分析领域处于领先地位。
高精度高性能的定理证明分析器
众所周知，传统的静态代码扫描技术中，主要有以下四种分析和检查原理
-
缺陷模式匹配
事先从代码分析经验中收集足够多的共性缺陷模式，将待分析代码与已有的共性缺陷模式进行匹配，从而完成软件安全分析。优点：简单方便；缺点：需要内置足够多的缺陷模式，容易产生误报。 -
类型推断/类型推断
类型推断技术是指通过对代码中运算对象类型进行推理，从而保证代码中每条语句都针对正确的类型执行。 -
模型检查
建立于有限状态自动机的概念基础上。将每条语句产生的影响抽象为有限状态自动机的一个状态，再通过分析有限状态机达到分析代码目的。校验程序并发等时序特性。 -
数据流分析
从程序代码中收集程序语义信息，抽象成控制流图，可以通过控制流图，不必真实的运行程序，可以分析发现程序运行时的行为。
而Pinpoint在这些基础上进行了科研创新，研发出了新一代的定理证明技术，该技术在众多的国际*学术会议上都发表了论文并且得到了国内外该领域专家的一致认可和好评。
那么什么是定理证明技术呢？我们可以举一个例子来说明。
以上这段程序，如果我们想检测其中是否存在空指针引用的情况，我们将采用一定方法对其进行分析。
传统的方法主要有几种：
- 将所有的分支结果枚举一遍，如果结果中存在空指针引用的情况，那么判断该段代码存在空指针引用的问题，该方法需要读取代码的所有内容，因此效率极差。
- 仅判断a指针是否可能为空，若可能的情况下，在引用前未加判断则直接判断该段代码存在空指针引用的问题，该方法无需花费太多时间，但准确性极低，误报较高。
而Pinpoint采用了自主研发的稀疏定理证明技术，可以同时做到准确且高效。
- 首先判断空指针引用的条件为：flag=true且a为空
- 接着向上搜索所有存在flag以及a的地方
- 发现若flag=true，那么x必须满足为true；a=null那么x必须满足为false
- 所以两个成立条件是互相矛盾的，因此该段程序并没有空指针引用的问题存在
这样的定理证明技术做到了在判断问题时不仅高效且十分的准确。
Java系语言的二进制扫描
当前许多的静态分析工具还无法对java系语言的二进制文件进行扫描分析，而仅仅分析源代码会造成十分庞大数量的误报，对于开发以及质量监管人员来说都是一个十分头疼的问题。对编译后的二进制文件分析，得出的结果往往更加准确，相当于直接理解了代码在做什么样的行为，那么这些行为所产生的后果也就能够推理分析出来。Pinpoint很早便自主研发出了java、android的二进制扫描分析，在该类语言的扫描结果上，准确率以及效率普遍高于其他同类产品。
在使用Pinpoint的过程中，将源码以及编译后的结果一起上传分析，程序将会首先分析二进制的结果文件，再结合源码，准确的将出错的位置标注并且展示，让使用者一目了然，同时，Pinpoint支持跨多编译单元追踪多级函数调用链，拥有自动学习函数库，能够建立应用安全分析所需模型。
针对企业的高并发CI/CD场景定制高可用部署方案
我们都知道，在安全开发建设的过程中，其实工具并不是一个特别让管理者头疼的点，最头疼的是一个合适自己企业开发场景的高可用部署方案，有了一个完整的、适用的、高效安全的方案，下面的建设就不再是无的放矢。源伞Pinpoint这款静态代码扫描工具，作为国内该领域的先行者，在为大大小小的企业进行服务的同时，也不断的学习和思考，形成了有着自己特色的针对不同企业的不同的高可用部署方案。在提供技术工具的同时，也能够输出这样的经验和解决方案，能够解决大部分企业所面临的安全开发建设方面的问题！