Runtime Verification精读记录

论文地址：Runtime Verification of Crypto APIs: An Empirical Study | IEEE Journals & Magazine | IEEE Xplore

2023 TSE CCF-A

总结：RVsec利用CrySl转化为JavaMOP规则实现RV（运行时验证）；三类方法四个工具对五个基准进行测评，详细描述了FN、FP的原因，在三类和五个分别进行展开描述（感觉重复内容有点多）

背景和实验设置

出现加密API误用原因：1.开发人员不清楚；2.现有分析工具挺好的，但还不够

RV的优势：1.加强发现错误的能力；2.补充静态分析工具，减少误报；3.平衡规则编写的付出和运行开销

本文RV方法：22条CrySl规则（CryLogger工具的规则）-——>JavaMOP规则；不使用RV加速技术；

基准：MASCBench、SmallCryptoAPIBench、OWASPBench、JulietBench、ApacheCryptoAPIBench（不全）

指标：P（准确率）、R（召回率）、

TP：正确预测的正例；FP：错误预测的正例（误报）；FN：错误预测的负例（漏报）

P：避免将负例误判为正例；R：覆盖真实正例的能力，避免漏判正例

实验目标：1.RVsec的有效性；2.误报漏报的原因

贡献总结：1.和现有工具进行了比较；2.发现和现有工具的互补作用；3.形成了22条JavaMOP规则；4.补充了不全基准的真实标签

RV是什么

静态分析存在误报（有滥用API代码，但实际没调用）和漏报（没检测到哈希功能滥用的API）问题

RVsec作为动态分析的方法，和其他动态分析的工具做比较

JavaMOP规范：1.事件定义（确定你要报告出什么问题）；2.属性（也就是事件的逻辑公式，使用ERE拓展正则描述，偶尔使用FSM有限状态机）；3.处理程序（ERE匹配成功触发执行程序，reset）

准确率描述

MASCBench：静态误报（Cipher.getInstance(keyGenerator.getInstance())，动态漏报（固定值初始化）

SmallCryptoAPIBench：Rcsec7个漏报（硬编码生成密钥，RV运行无法验证硬编码问题），CryLogger误报（规则过于严格）漏报（可预测的种子或凭证）

OWASPBench：CogniCrypt误报（控制流问题，不全部执行），CryptoGuard误报（配置文件问题），CryLogger误报（规则过于严格）

配置文件	代码信息	CryptoGuard
✅	❌	❌误报
❌	✅	✅漏报

JulietBench：RVsec漏报（哈希算法的不确定性，一个安全一个不安全），CryptoGuard漏报（缺少所需的加密步骤）
ApacheCryptoAPIBench（该基准没有标准的真实标签，研究人员手动标记）

Summary: Results shows that RVSec is very accurate (F1=0.95), compared to CryLogger (F1=0.85), CogniCrypt (F1=0.83), and CryptoGuard (F1=0.78).

原因描述

RVsec：

8FP（过于严格的规则），22FN（10个输入测试样例缺乏、12个动态分析固有局限）

加密API的使用仅限于一些由测试样例进行的覆盖类；检查初始化使用硬编码的规则编写困难
静态分析（CryptoGuard、CogniCrypt）：

漏报（多次方法调用初始化Cipher类、路径敏感问题、条件判断、加密算法完整代码识别）

误报漏报都有（配置文件问题，具体可见上文的表格，这里给一张图描述，fig15误报、fig16漏报）
动态分析（CryLogger）：

误报（安全算法被认为不安全、不确定性问题）

漏报（缺乏算法的完整步骤，随机数问题）

对大项目扫描效果不佳，输出不合适

讨论和未来工作

RV开销：

新技术evolution-aware可以减少RV的开销（10x，平均5x）

未来工作：

动静态分析的互补性
更好的在检测中使用RV
现有基准的问题

开源仓库具体展示

项目地址 GitHub - PAMunb/rvsec

KeyGeneratorSpec-JavaMOP规范说明：rvsec/rvsec/rvsec-agent/src/main/mop/KeyGeneratorSpec.mop at master · PAMunb/rvsec · GitHub

package mop;

import javax.crypto.KeyGenerator;
import javax.crypto.SecretKey;
import java.security.SecureRandom;
import java.security.spec.AlgorithmParameterSpec;

import br.unb.cic.mop.eh.*;
import br.unb.cic.mop.ExecutionContext;

/**
 * KeyGeneratorSpec
 *
 * A JavaMOP specification of the correct usage of the
 * javax.crypto.KeyGenerator class.
 *
 * https://github.com/CROSSINGTUD/Crypto-API-Rules/blob/master/JavaCryptographicArchitecture/src/KeyGenerator.crysl
 */
KeyGeneratorSpec(KeyGenerator k) {

    List<String> safeAlgorithms = Arrays.asList("AES", "HmacSHA256", "HmacSHA384", "HmacSHA512");
    String currentAlgorithmInstance = "";
    KeyGenerator keyGenerator = null;

    Key generatedKey;

    event g1 after(String alg) returning(KeyGenerator k):
      call(public static KeyGenerator KeyGenerator.getInstance(String))
      && args(alg)
      && condition(safeAlgorithms.contains(alg)) {
        keyGenerator = k;
        currentAlgorithmInstance = alg;
    }

    event g2 after(String alg, Object provider) returning(KeyGenerator k):
      call(public static KeyGenerator KeyGenerator.getInstance(String, Object+))
      && args(alg, provider)
      && condition(safeAlgorithms.contains(alg)) {
        keyGenerator = k;
        currentAlgorithmInstance = alg;
    }

    event g3 after(String alg) returning(KeyGenerator k):
      call(public static KeyGenerator KeyGenerator.getInstance(String))
      && args(alg)
      && condition(!safeAlgorithms.contains(currentAlgorithmInstance))  {
        currentAlgorithmInstance = alg;
    }

    event init before(KeyGenerator k):
       ( call(public void KeyGenerator.init(int)) ||
         call(public void KeyGenerator.init(int, SecureRandom)) ||
         call(public void KeyGenerator.init(AlgorithmParameterSpec)) ||
         call(public void KeyGenerator.init(AlgorithmParameterSpec, SecureRandom)) ||
         call(public void KeyGenerator.init(SecureRandom))
       ) && target(k) {  }

    event gk1 after(KeyGenerator k) returning(SecretKey key):
      call(public SecretKey KeyGenerator.generateKey())
      && target(k) {
        if (!safeAlgorithms.contains(currentAlgorithmInstance)) {
            ErrorCollector.instance().addError(new ErrorDescription(ErrorType.UnsafeAlgorithm, "KeyGeneratorSpec", "" + __LOC,
        "expecting one of" + String.join(",", safeAlgorithms) + " but found " + currentAlgorithmInstance + "."));
        }
        generatedKey = key;
        ExecutionContext.instance().setProperty(ExecutionContext.Property.GENERATED_KEY, generatedKey);
    }

    ere : (g3* g1+ | g3* g2+) ((init gk1) | gk1)

    @fail {
        ErrorCollector.instance().addError(new ErrorDescription(ErrorType.InvalidSequenceOfMethodCalls, "KeyGeneratorSpec", "" + __LOC));
        ExecutionContext.instance().unsetObjectAsInAcceptingState(keyGenerator);
        ExecutionContext.instance().remove(ExecutionContext.Property.GENERATED_KEY, generatedKey);

        __RESET;
    }

    @match {
       ExecutionContext.instance().setObjectAsInAcceptingState(keyGenerator);
    }
}

分析说明：

这段代码是一个 JavaMOP (Java Monitoring and Pluggable) 的规范，用于监控和验证 javax.crypto.KeyGenerator 类的正确使用情况。它的目的是确保在使用 KeyGenerator 类时，仅允许特定的安全算法，并且遵循一定的调用顺序。JavaMOP 是一种用于 Java 程序运行时监控的工具，通常用于验证代码中某些条件是否被满足。

下面是对代码的逐步分析：

定义和目标

该规范的目标是监控 KeyGenerator 的使用，确保以下条件：

使用的是一个安全的算法（如：AES、HmacSHA256、HmacSHA384、HmacSHA512）。
KeyGenerator 的方法调用顺序正确。

变量声明

List<String> safeAlgorithms = Arrays.asList("AES", "HmacSHA256", "HmacSHA384", "HmacSHA512");
String currentAlgorithmInstance = "";
KeyGenerator keyGenerator = null;
Key generatedKey;

safeAlgorithms 列出了允许的安全算法。
currentAlgorithmInstance 用于追踪当前实例化的 KeyGenerator 使用的算法。
keyGenerator 和 generatedKey 用于追踪 KeyGenerator 实例和生成的密钥。

事件 g1、g2、g3：

这些事件分别在 KeyGenerator.getInstance() 方法调用后触发，用于记录 KeyGenerator 的实例化。

g1：在 KeyGenerator.getInstance(String) 被调用时，如果算法在安全算法列表中，记录当前使用的算法。
g2：在 KeyGenerator.getInstance(String, Object) 被调用时，也类似地记录当前使用的算法。
g3：在其他情况下（例如，算法不在安全算法列表中），更新 currentAlgorithmInstance，但不做其他操作。

事件 init：

event init before(KeyGenerator k):
    ( call(public void KeyGenerator.init(int)) ||
      call(public void KeyGenerator.init(int, SecureRandom)) ||
      call(public void KeyGenerator.init(AlgorithmParameterSpec)) ||
      call(public void KeyGenerator.init(AlgorithmParameterSpec, SecureRandom)) ||
      call(public void KeyGenerator.init(SecureRandom))
    ) && target(k) {  }

这个事件在 KeyGenerator 的初始化方法（init()）调用之前触发，确保 KeyGenerator 被正确初始化。它监控了多个重载版本的 init() 方法。

事件 gk1：

event gk1 after(KeyGenerator k) returning(SecretKey key):
    call(public SecretKey KeyGenerator.generateKey())
    && target(k) {
        if (!safeAlgorithms.contains(currentAlgorithmInstance)) {
            ErrorCollector.instance().addError(new ErrorDescription(ErrorType.UnsafeAlgorithm, "KeyGeneratorSpec", "" + __LOC,
            "expecting one of" + String.join(",", safeAlgorithms) + " but found " + currentAlgorithmInstance + "."));
        }
        generatedKey = key;
        ExecutionContext.instance().setProperty(ExecutionContext.Property.GENERATED_KEY, generatedKey);
    }

gk1 事件会在 generateKey() 方法被调用后触发。它检查当前算法是否在安全算法列表中。如果不在列表中，则会触发错误。
generatedKey 被保存并通过 ExecutionContext 设置。

ere：

1	ere : (g3* g1+ \| g3* g2+) ((init gk1) \| gk1)

这是一个事件规则，描述了事件之间的合法调用顺序：

允许 g3（不安全算法）事件多次出现，但至少跟随一个 g1 或 g2 事件（这些是安全算法实例化的事件）。
init 和 gk1 事件可以在一起或者单独出现，但必须按顺序。

@fail 语句：

@fail {
    ErrorCollector.instance().addError(new ErrorDescription(ErrorType.InvalidSequenceOfMethodCalls, "KeyGeneratorSpec", "" + __LOC));
    ExecutionContext.instance().unsetObjectAsInAcceptingState(keyGenerator);
    ExecutionContext.instance().remove(ExecutionContext.Property.GENERATED_KEY, generatedKey);

    __RESET;
}

如果事件顺序不正确或发生错误，这段代码会触发。
它会记录错误、清除执行上下文中的相关信息，并重置状态。

@match 语句：

1
2
3

@match {
    ExecutionContext.instance().setObjectAsInAcceptingState(keyGenerator);
}

这段代码用于当事件顺序正确时，设置 keyGenerator 为接受状态，表示其处于一个有效的状态。

总结：

这个 JavaMOP 规范旨在监控 KeyGenerator 类的使用，确保以下两个方面：

使用的算法是安全的，符合 safeAlgorithms 列表的规定。
KeyGenerator 的方法调用顺序是正确的。

当不符合这些规则时，代码会触发错误并清理执行上下文。如果符合规则，则会将 KeyGenerator 设为有效状态。

JAVAPOM

JavaMOP（Java Monitoring-Oriented Programming）是一个基于运行时验证（Runtime Verification，RV）的方法，旨在动态监控Java程序的执行，并验证程序在运行时是否遵循给定的正式规格。JavaMOP是用来检查程序是否满足一定的行为约束的一种工具，通常用于检测程序中潜在的错误或不符合预期的行为。

开源仓库runtimeverification/javamop: Runtime verification system for Java, using AspectJ for instrumentation. (github.com)

JavaMOP的特点：

运行时验证：
- JavaMOP通过将正式的规格（例如，逻辑约束或事件序列）嵌入到Java程序中，在程序运行时检查这些规格是否被满足。如果某个规格没有被满足，它会触发一个警告或错误报告。
监控事件：
- JavaMOP关注事件驱动的编程模型。它通过在程序运行时监控特定的事件（如方法调用、字段访问等）来检查程序是否遵循了定义的行为。
- 可以定义复杂的事件序列（例如方法调用的顺序）来验证程序的行为。
规格语言：
- JavaMOP允许用户使用各种规格语言来定义监控规则。常用的语言包括：
  - 扩展正则表达式（ERE）：用于描述方法调用的序列。
  - **上下文无关语法（CFG）、有限状态机（FSM）、线性时序逻辑（LTL）**等，适用于更复杂的约束。
在仓库javamop/examples at master · runtimeverification/javamop (github.com)的例子中，包含多种规格语言的例子。
错误检测和报告：
- 当程序在运行时违反了定义的规则时，JavaMOP会记录违规信息，并通过日志或警报向开发者报告错误。这使得开发者能够在早期阶段识别潜在的问题，并进行修复。
灵活性与可扩展性：
- JavaMOP支持与其他工具和框架的集成，可以与现有的Java应用程序一起使用，而无需对源代码进行大量修改。
- JavaMOP还支持动态监控，可以与现有的测试用例一起使用，以提高测试的覆盖率。

JavaMOP的工作原理：

规格编写：用户使用JavaMOP的规格语言（如ERE、FSM）编写正式规格，定义程序应遵循的行为。
代码插桩：JavaMOP通过插桩技术在程序的执行过程中添加监控代码，这些代码在程序运行时触发并监控相关的事件。
执行监控：程序按照规格运行，JavaMOP实时监控并检查程序是否违反了任何规格。如果发现违规，它会记录并报告。

应用场景：

软件测试：在单元测试、集成测试过程中，使用JavaMOP动态监控程序的执行，以验证程序是否符合规范。
安全验证：用于检查程序是否遵循安全协议，例如确保加密API按照规定的顺序和规则进行调用。
程序行为分析：在复杂系统中，动态监控特定的行为或状态，以确保系统按照预期运行。

优点：

实时性：能够在程序运行时即时发现错误，避免了静态分析可能遗漏的动态行为问题。
高精度：可以精确地监控程序的每个方法调用或事件，减少误报。
易于集成：可以在现有的Java项目中轻松集成，无需大规模修改代码。

缺点：

运行时开销：插桩和动态监控可能会导致一定的性能开销，尤其是在大规模程序中。
规格编写困难：编写精确的正式规格可能需要深厚的领域知识和对程序行为的深入理解。
覆盖限制：如果测试用例不足或覆盖范围不广，动态分析可能无法发现所有的潜在问题。

总结：

JavaMOP是一个强大的工具，特别适用于动态监控Java程序的执行，并检查是否符合预定的行为规范。它的灵活性和高精度使其在软件工程中具有广泛的应用价值，尤其是在复杂系统和高安全性要求的场景下。

JavaMOP（Java Monitoring Oriented Programming）是一个基于监控导向编程（Monitoring Oriented Programming）的工具，主要用于在Java程序中动态监控和检测程序行为。它允许开发者定义监控逻辑，并将这些逻辑与应用程序运行时状态相结合，从而捕捉到运行时的特定事件。

JAVAMOP一个简单的应用实例：

假设我们有一个简单的Java应用程序，其中包含了一个账户类（Account），该类允许存款和取款操作。我们希望监控每次取款操作时账户余额是否足够，如果余额不足，打印错误日志。

定义监控规范（Monitor）

首先，我们需要定义监控规范，这个规范将在JavaMOP中进行编译。这里我们编写一个简单的监控规则：当调用Account.withdraw()方法时，如果余额不足，监控到的结果将触发一条错误信息。

// Account.mop
monitor AccountMonitor {
    // 绑定到Account类的withdraw方法
    event withdraw(Account a, int amount) after (a.withdraw(amount)) {
        if (a.getBalance() < 0) {  // 检查余额是否不足
            System.out.println("ERROR: Insufficient funds for withdrawal of " + amount);
        }
    }
}

编译监控规范

使用JavaMOP编译器来编译这个监控规范文件。编译后的代码将作为工具的一部分插入到我们的Java项目中。

1	java -jar JavaMOP.jar -m Account.mop

编译后的代码将生成与Account类相关的监控类，用于插入到应用程序中。

集成监控代码

然后，我们将监控代码集成到我们的应用程序中。我们假设有一个简单的Account类，其中包括存款和取款操作。

// Account.java
public class Account {
    private int balance;

    public Account(int balance) {
        this.balance = balance;
    }

    public void deposit(int amount) {
        balance += amount;
    }

    public void withdraw(int amount) {
    if (amount > balance) {
        throw new IllegalArgumentException("余额不足");
    }
    balance -= amount;
}

    public int getBalance() {
        return balance;
    }
}

运行监控

现在我们运行程序，并监控每次取款操作。如果余额不足，监控将触发相应的错误信息输出。

// Main.java
public class Main {
    public static void main(String[] args) {
        Account account = new Account(100);
        account.withdraw(50);  // 应该正常执行
        account.withdraw(100); // 会触发错误，因为余额不足
    }
}

输出

运行程序时，我们应该看到如下输出：

1	ERROR: Insufficient funds for withdrawal of 100

在这个简单的例子中，JavaMOP通过插入监控代码，能够动态监控Account.withdraw()方法的行为，并在特定条件（余额不足）下输出错误信息。这种方式非常适合用于调试、性能监控或检测程序中的潜在错误。