LSBA Based Security Verification in MCC

This paper presents a new way to verify whether a behavior model of code satisfies a security policy in the model-carrying code(MCC) approach for safe execution of untrusted code. This new verification method based on a new kind of model called logic semantic based automata(LSBA). Logic semantic based pushdown automata(LSBPDA)is to model safety-related behaviors of codes unknown to a user and logic semantic based finite states automata (LSBFSA) is to model security policies of users. Verification is done by checking wether the language of the LSBPDA model of a policy and the language of the LSBFSA model of untrusted code intersect. This new method is formal in nature and suitable for automation of the verification step in MCC method.