SMT理论驱动的Lustre程序安全性验证法

本文主要探讨了在确保Lustre程序安全性方面的一种新颖方法，即利用可满足性模理论（SMT）。Lustre是一种重要的编程语言，特别是在实时系统和并发计算领域，其安全性验证面临着严峻挑战。传统的验证方法，如NBAC使用的抽象解释和Luke采用的SAT求解器，都存在局限性，容易受到攻击。 SMT作为一种扩展的命题逻辑满足性检查技术，允许在特定理论，如整数或实数上的线性算术，对逻辑公式进行判断。它通过增强标准的SAT求解器，使其能够处理这些理论中的约束条件，如在CVCLITE、DPLL(T)、haRVey和MATHSAT等系统中所见。一些系统，如ARIO，采用了伪布尔SAT求解器，但仍遵循相似原理。 本文作者提出了一种创新的策略，即构建一个基于SMT的增量式判定过程，用于Lustre程序的验证。这个过程通过简单的方式实现，旨在提高验证效率并提供竞争性的性能。与现有工具相比，特别是在处理复杂情况时，这种方法显示出优越性。作者关注的理论框架限于无量化的一阶公式，具体涉及整数变量之间的线性关系，如iaixi=b，其中a和b是整数常数。 通过SMT技术，可以验证Lustre程序在执行过程中是否满足这些线性约束，从而确保程序行为符合预期，降低潜在的安全漏洞。这种方法不仅提升了验证的精确性和效率，也为Lustre程序的严谨性和安全性提供了强有力的支持。因此，本文的工作对于推动形式验证在Lustre这类关键领域的应用具有重要意义。