ChiSA：轻量级Chisel验证的静态分析方法

《Proceedings of the ACM on Programming Languages》：ChiSA: Static Analysis for Lightweight Chisel Verification

本文提出基于静态分析的Chisel硬件验证工具ChiSA，通过λC形式化核心解决价值流分析问题，实现高效漏洞检测与信息泄露分析，实验表明其优于现有方法。

　　

摘要摘要

要查看此由人工智能生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

在硬件开发中，对生产力的需求不断增长，这为将编程语言（PL）技术应用于硬件描述语言（HDL）提供了新的机会。Chisel作为一种领先的敏捷HDL，通过利用现代PL特性来提高硬件设计的生产力。然而，Chisel的验证仍然是一个主要的生产力瓶颈，需要大量的时间和人工努力。为了解决这个问题，我们提倡使用静态分析技术——这种技术已被证明非常适合软件的敏捷开发工作流程——来进行轻量级的Chisel验证。

本研究为Chisel的静态分析建立了理论基础。其核心是λ_C，这是ChAIR（一种针对Chisel的中间表示形式，用于分析）的形式化核心演算。λ_C是第一个既能捕捉Chisel本质又能保持极简性的形式化体系，从而便于基于λ_C进行严格的静态分析推理。我们证明了λ_C的一些关键属性，这些属性反映了真实的硬件特性，从而为其设计提供了一种回顾性验证方式。在λ_C的基础上，我们定义并形式化了硬件价值流分析（HVFA）问题，这是我们进行关键Chisel验证任务（包括错误检测和安全分析）的静态分析的基础。然后，我们提出了一种针对HVFA问题的同步定点解决方案，该方案特别处理了时钟驱动的硬件寄存器的同步行为——这是Chisel程序的核心特征。我们进一步证明了一些关键定理，以确立我们解决方案的保证和局限性。

作为概念验证，我们开发了ChiSA（30K+ LoC）——第一个能够分析复杂硬件价值流的Chisel静态分析器，从而实现对关键Chisel验证任务（如错误检测和安全分析）的轻量级分析。为了全面评估ChiSA和未来的工作，我们提供了ChiSABench（11M+ LoC），这是一个用于Chisel静态分析的综合性基准测试工具。

我们在ChiSABench上的评估表明，ChiSA为关键Chisel验证任务提供了一种有效且显著更轻量级的解决方案，尤其是在大型和复杂的实际设计中。例如，ChiSA在不到200秒的时间内识别出了大规模Chisel设计（9.7M+ LoC）中的69个可违反的开发者插入断言——其中8个已被开发者发现并计划在未来进行修复——并且在一秒钟内检测出了著名的TrustHub基准测试（1.1M+ LoC）中的所有60个信息泄露漏洞——其性能超过了像ChiselTest的有界模型检查和ChiselFlow的安全类型系统这样的现有Chisel方法。这些结果凸显了静态分析在轻量级Chisel验证中的巨大潜力。为了鼓励持续的研究和创新，我们将完全开源ChiSA（30K+ LoC）和ChiSABench（11M+ LoC）。

摘要

要查看此由人工智能生成的纯文本摘要，您必须具有高级访问权限。