是否可以使用 Frama-C 来验证执行流程或内存访问是否依赖于特定变量？
背景:
曾经有选项 -experimental-path-deps and -experimental-mem-deps , 但这些是 removed在硅
发布。
为了防止旁道攻击，我想确保程序的执行流程不依赖于 secret 数据，使其容易受到定时攻击。
对于内存访问，我们可以对每个索引进行数据流分析，但是这样比较容易出错，而且每次访问数组都必须手动进行。对于 -experimental-path-deps，没有明显的解决方法。
Frama-C 的其他地方是否存在等效功能，或者是简单地恢复到旧版本的最佳选择？
最佳答案
-experiment-{path,mem}-deps 大部分是现有依赖分析的重复，而且从未移植为完全调用敏感(选项 -calldeps).如果您愿意编写一些 OCaml 代码，修改现有的调用感知依赖分析很容易。这将比恢复到 pre-Silicon 版本更精确。如果您有兴趣，我可以扩展此答案以将您指向要修改的函数。
关于frama-c - 执行路径数据流分析，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/48404139/