To protect computer systems from running untrusted software programs, various methods have been proposed in software domain to validate the trustworthiness and genuineness of the delivered software code. Most of these methods lay burden on users to verify the code while a new mechanism, proof-carrying code, switches workload purely to software providers and provides a unique way to determine whether code from potentially untrusted sources is safe to execute.
The design of the security properties will depend on the feature of the attack and the structure of the microprocessor. Our current properties can be classified to the functional properties (whether the output is correct) and storage properties (whether the proper registers have been updated).
We use the encapsulation to deal with our proof, and the encapsulated lemmas can be reused for different instructions when proving their security properties. And then we can find that there is a hierarchical system after the encapsulating.