NJU「软件分析」学习笔记：Soundness and Soundiness

Soundness and Soundiness

前面提到 static program analysis 追求的 goal 是 soundness，但是无论是在学术界还是在工业界，由于一些语言的 hard language features 的存在，对现实世界的大型 program 想要实现完全的 soundness 是（目前）做不到的。

Hard-to-analyze features: an aggressively conservative treatment to these features will likely make the analysis too imprecise to scale, rendering the analysis useless.

于是，为了避免 papers 中写 soundness 会误导读者，所以引入了 soundy 的概念：a soundy analysis typically means that the analysis is mostly sound, with well-identified unsound treatments to hard/specific language features.

Hard Language Feature: Java Reflection

java reflection 会在 run-time 将 class、method、field 等转换为 metaobject，并且用一个 string 作为它们的 identifier，如图所示。

reflection

在 run-time 对代码作出一些改变会产生一些 static analysis 无法预测的行为，这也是 static analysis 的硬伤。

why analyze reflection

• string mName 无法分析，那么 m.invoke 具体调用了哪个方法也就无法得知，于是对某些可能的 method 的忽略优化很有可能会导致我们少检测到一些 bug
• 在进行 verification optimization 时，我们可能会忽略 reflection 产生的作用等同于 a.fld = a 的语句 f.set(a, a)，那么在分析 B b = (B) a.fld 就会得到 false negative

考虑到 reflection 产生的很多不确定行为都是由于 string 具体值的未知而导致的，因此我们可以用 string constant analysis + pointer analysis¹ 来完成对 reflection 的分析。

但是实际上的很多 string 都是 statically unknown，所以这种方法仍然具有很大的局限性。

除了直接对 string 进行分析，我们还在 usage points 对可能的 reflective targets 进行推断，概括来说就是 type inference + string analysis + pointer analysis，实践上，这种方法的准确度也很高。²

infer

不仅仅是根据 usage point 时的 parameters 对 method 进行推断，对其他的 metaobject 也是有效的³。

more handlings

另外，我们也可以根据 run-time 的特性利用 dynamic analysis 辅助 static analysis⁴。具体一点说就是利用一部分程序进行 dynamic analysis 分析得到的数据进行 static analysis，但是有限的程序量很难 cover 所有可能的 data。

Hard Language Feature: Native Code

在 java 中如果想要 print，就需要与 OS 进行交互，于是就不得不调用一些底层的 C/C++ 代码，这些代码被称为 native code。

由于 java 是运行在 jvm 上的，所以 jvm 需要一个 function module 作为 interface 便于它 (jvm) 与 native code 调用的 native libraries 进行交互，也可以与 OS 进行交互、复用已有的 C/C++ 代码，这个 interface 就是 JNI。

interoperation

由于我们的 analyzer 针对的是 java 代码，而 native code 用的是 C/C++ 代码，所以我们无法进行分析。

目前对于这个问题使用最广泛的方法是 manually models critical native code，比如调用 arraycopy 方法就将其改写为 java 语言的循环赋值语句然后再进行分析。

最近的研究工作有使用 binary scanning 在 native code 中识别 java calls 的⁵。

最后，想要了解更多 soundiness，可以访问 soundiness.org.