Program veriﬁcation is vital as more and more users are creating, downloading and executing foreign computer programs. Software veriﬁcation tools provide a means for determining if a program adheres to a user’s security requirements, or security policy. There are many veriﬁcation tools that exist for checking diﬀerent types of policies on diﬀerent types of programs. Currently however, there is no veriﬁcation tool capable of determining if all types of programs satisfy all types of policies. This thesis describes a framework for supporting multiple veriﬁcation tools to determine program satisfaction. A user’s security requirements are represented at multiple levels of abstraction as Intermediate Execution Environments. Using a sequence of conﬁgurations, a user’s security requirements are transformed from the abstract level to the tool level, possibly for multiple veriﬁcation tools. Using a number of case studies, the validity of the framework is shown.
|Date of Award||6 Jun 2009|
|Supervisor||Padmanabhan Krishnan (Supervisor)|