java - 对源代码、字节代码、机器代码等执行静态分析的权衡是什么？

Question

在不同级别的代码上执行静态分析的各种权衡是什么？例如对于 Java，为什么有人会对 Java 源代码执行静态分析而不是 Jasmin代码与 Java 字节码？选择是否限制或扩展了能够进行的各种类型的分析？选择会影响分析的正确性吗？谢谢。

Answer 1

What are the various tradeoffs for performing static analysis on various levels of code? For instance for Java, why would someone perform static analysis on Java source code vs. Java bytecode?

从用户的角度来看，我会说，除非您有非常具体、易于形式化的属性来分析(例如纯安全属性)，否则请使用支持 Java 源代码的工具.

从工具开发人员的角度来看，使用一个级别或另一个级别可能更容易。我在这里提出我想到的差异。 (请注意，对于编译器和/或像样的反编译器，工具例如在一层上运行并在另一层上显示结果。)

Java 源代码的优点:

• Structured language ，即循环等，而不是任意跳跃。 (例如，这使得创建 weakest precondition 演算变得容易得多。)
• 你可以在代码中做更多的假设(字节码程序更具表现力)。

字节码的优点:

• 语言规范(字节码指令的语义)要简单很多。
• 更“固定”的机器(VM)规范
• 您可以将分析扩展到遗留代码和库。
• 分析允许针对 JVM 的其他语言(Closure、Scala、JRuby...)
• 不需要可能很复杂的解析器

机器码的优点:

• 您验证您实际为 CPU 提供的是什么。 (如果您想要一个完全验证的链，则无需使用经过验证的编译器或经过验证的 VM。)

最先进的工具，例如 Spec#等(C# 的形式方法方言)通常通过专门为形式分析设计的中间语言(在 Spec# 案例中是 BoogiePL(更接近 MSIL 或 C#))。

Does the choice restrict or expand the various types of analyses able to be done?

最后……不，不是真的。无论您选择分析哪种 (Turing complete) 语言，您都会面临相同的基本问题。根据您分析的属性，YMMV。

如果您热衷于形式化方法并考虑自己实现分析，我想您会找到更好的字节码工具支持。如果您是用户 或开发人员 并且想要对您自己的代码库执行分析，我怀疑您将从在 Java 源代码级别运行的工具中获益更多.

Does the choice influence the correctness of the analyses?

取决于你所说的正确性。静态分析通常是“防御性”的，因为您不会假设任何您不知道的事情都是真实的。如果您将注意力限制在 sound验证系统，所有这些都将“同样正确”。