A Module Level Security Evaluation Method Based on Model Checking

Processors are an important component of computer systems, but resource sharing in space and time, as well as performance first design concepts, result in a series of security issues for processors. On the one hand, processor security evaluation can systematically analyze and verify the security of the processor, deduce the key reasons for security risks, and on the other hand, it can assist in processor design, verifying processor security at a lower cost at the beginning of the design, compared to later software and hardware protection.This paper proposes a module level security evaluation method based on model checking, modeling the module as a mealy finite state machine to analyze the relationship between its outputs, inputs and states. Computational Logic Tree (CTL) is used to represent possible execution paths, and all paths are traversed to derive counterexample paths to represent possible attack paths and information leakage processes. We use the Common Vulnerability Scoring System(CVSS) to score each counterexample path. Based on these counterexample paths and CVSS scores, we ultimately obtained a total risk score to represent the security of the module. We conduct a case study on Cache to verify the effectiveness of our proposed method.