本技术公开了一种面向Armv8‑a汇编代码的形式化验证方法,对Armv8‑a的处理器架构和指令集系统进行分析,提取出需要建模的各个模块构件,包括异常级别、执行状态、数据值、寄存器组、内存、指令集、汇编代码,对各个模块构件进行建模;根据汇编代码中每个汇编指令的功能和安全规范确定对应汇编指令的非形式化要求,然后结合定义的模型生成每个汇编指令的形式化逻辑表达式,从而得到形式化规约;最后采用定理证明器进行形式化验证。本发明对物理机器的各个模块构件进行建模,然后基于构建的模型生成汇编代码中每个汇编指令的形式化逻辑表达式,使用定理证明器完成Armv8‑a汇编代码的形式化验证。
背景技术
操作系统作为现代计算机应用的基础平台,支持各类软件的运行,并直接影响计算机系统的稳定性和安全性。操作系统中的小漏洞可能导致严重的系统错误或安全威胁,甚至引发生命和财产损失。因此,确保操作系统的安全性和可靠性是维护计算机软件生态健康运行的关键因素。
传统的软件测试方法在发现错误和漏洞方面存在局限,测试无法覆盖所有情况和路径,漏洞可能隐藏在边缘情况或复杂交互中。因此,虽然传统测试方法是重要的质量保障手段,但无法完全消除系统中的错误和漏洞。而随着系统功能的扩展、代码规模的增大以及内部逻辑的复杂化,确保系统的可靠性和安全性成为一项重要且富有挑战性的任务。在现有技术中,形式化方法是解决这一挑战的有效途径。
形式化方法是一种以数学和形式化语言为基础,能够提高软硬件系统的可靠性和正确性的技术。该方法的核心理念是通过精确而严格的规约和验证过程,消除软硬件设计和实现中的歧义,降低错误和漏洞的发生概率。形式化方法包括形式规约和形式验证两个主要步骤。形式规约是对系统行为和性质的详细、数学化描述,通常使用形式化语言。这样的规约消除了对系统规范的模糊理解,提供了准确且一致的描述。形式验证则通过数学分析方法,对形式规约进行验证,以确保系统满足规约中定义的性质。
近些年来,针对操作系统内核验证的工作:澳大利亚国家信息通信中心(NICTA)的seL4项目,使用了交互式定理证明器Isabelle/HOL,通过三层验证框架完成了微内核的形式化验证。耶鲁大学根据深度规约和认证抽象层开发出的CertiKOS框架,通过Coq验证了并发操作系统内核mC2。中国科学技术大学开发出了针对C语言子集的操作系统内核验证框架,验证了抢占式操作系统μC/OS-II的关键模块。
现代操作系统主要使用高级语言开发,但汇编代码在关键部分仍然发挥着不可或缺的作用。相比高级语言,汇编代码可以实现对硬件的直接访问和控制:能够直接操作CPU寄存器、执行特权指令以及与硬件设备进行高效交互,这在许多性能敏感的场景中至关重要。例如,在上下文切换和中断处理时,汇编代码可以确保最小的延迟和最高的执行效率。此外,汇编语言还允许开发者在内存管理和系统调用中实现更精细的控制,确保操作系统在资源受限的环境中运行时的可靠性和高效性。因此,汇编代码中潜在的错误或漏洞都可能导致系统崩溃或安全隐患,所以对操作系统的验证离不开汇编代码的安全性。
实现思路