Research on Remote Attestation Technology Based on Formal Software Behavior Measurement

The traditional static measurement method based on data integrity measurement can only prove that the software has not been tampered with, and cannot describe the software behavior status. Dynamic measurement can measure the software behavior in real time, but there is no doubt that it requires a lot of computing resources. In this paper, we propose static measurement architecture PMA, which using formal method to abstract and verify software behavior. In PMA, formal language abstracts software behavior, formal specification describes security policy, and software behavior measurement problem is transformed into formal proof. We also have implemented the corresponding code according to the PMA design principle. The experimental test verifies the feasibility of the PMA architecture.