面向Armv8-a汇编代码的形式化验证方法

本发明公开了一种面向Armv8‑a汇编代码的形式化验证方法，对Armv8‑a的处理器架构和指令集系统进行分析，提取出需要建模的各个模块构件，包括异常级别、执行状态、数据值、寄存器组、内存、指令集、汇编代码，对各个模块构件进行建模；根据汇编代码中每个汇编指令的功能和安全规范确定对应汇编指令的非形式化要求，然后结合定义的模型生成每个汇编指令的形式化逻辑表达式，从而得到形式化规约；最后采用定理证明器进行形式化验证。本发明对物理机器的各个模块构件进行建模，然后基于构建的模型生成汇编代码中每个汇编指令的形式化逻辑表达式，使用定理证明器完成Armv8‑a汇编代码的形式化验证。