咨询：能否用Frama-C验证执行流或内存访问对特定变量的依赖及替代方案

Great question—side channel resistance (especially against timing attacks) is such a critical concern, and it’s totally frustrating when experimental features you rely on get removed. Let’s break down your options for modern Frama-C versions, plus weigh whether rolling back is the right move.

1. Use the WP (Weakest Precondition) Plugin for Path Dependency Proofs #

The WP plugin is your best bet for formally proving that execution flow doesn’t depend on secret data. Here’s how to approach it:

• For branch conditions that shouldn’t rely on secrets, write assertions that the condition’s outcome is identical regardless of the secret variable’s value. For example:

  /*@ 
    requires \valid(secret);
    ensures (\result == 1) == (\result == 1[secret := 0]);
  */
  int sensitive_branch(int secret) {
    if (secret > 5) return 1;
    else return 0;
  }
  

• Run WP with frama-c -wp -wp-rte your_program.c to verify these assertions. If WP can prove the assertion holds, it confirms the branch outcome doesn’t depend on secret.
• For memory accesses, you can use similar assertions to prove array indices don’t rely on secrets—e.g., ensuring the index value is the same even if the secret is replaced with a constant.

2. Leverage the -deps Option with Value Analysis #

While not a direct replacement for -experimental-path-deps, the built-in -deps option (used with Value Analysis) can help track data dependencies:

• Run frama-c -eva -deps your_program.c to generate a report of which variables depend on others.
• Check if your secret variable appears in the dependency chain of branch conditions or array indices. This won’t capture full path dependencies, but it’s a useful lightweight check to catch obvious leaks.
• Pair this with -slevel N (where N is a higher number) to increase Value Analysis’s context sensitivity, making dependency tracking more accurate for complex control flow.

3. Build a Custom Analysis with Frama-C’s OCaml API #

If you need functionality exactly like the old -experimental-path-deps, you can build a custom plugin using Frama-C’s OCaml API:

• Tap into the Control Flow Graph (CFG) generated by Frama-C’s frontend.
• Traverse each branch node and use Value Analysis’s results to check if the branch condition’s evaluation depends on your secret variable.
• This requires some OCaml knowledge, but it gives you full control over the analysis logic—perfect for replicating the old experimental feature’s behavior in modern Frama-C.

4. Should You Roll Back to an Older Frama-C Version? #

Rolling back to a version that still supports -experimental-path-deps and -experimental-mem-deps is technically feasible, but consider these tradeoffs:

• Pros: You get the exact functionality you’re used to without needing to rewrite your analysis workflow.
• Cons: Older versions lack critical bug fixes, security patches, and new features from recent Frama-C releases (like improved WP tactics or better Value Analysis precision). The experimental features were also never officially supported, so they might have unaddressed bugs that won’t be fixed.

Final Recommendation #

If you’re working on a long-term project, prioritize migrating to WP + -deps or a custom plugin—these are supported, maintainable approaches. If you need a quick fix for a short-term task and don’t rely on modern Frama-C features, rolling back can work as a temporary solution.

内容的提问来源于stack exchange，提问作者Lll