Program verification is vital as more and more users are creating, downloading and executing foreign computer programs. Software verification tools provide a means for determining if a program adheres to a user’s security requirements, or security policy. There are many verification tools that exist for checking different types of policies on different types of programs. Currently however, there is no verification tool capable of determining if all types of programs satisfy all types of policies. This thesis describes a framework for supporting multiple verification 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 configurations, a user’s security requirements are transformed from the abstract level to the tool level, possibly for multiple verification tools. Using a number of case studies, the validity of the framework is shown.
| Identifer | oai:union.ndltd.org:ADTP/238599 |
| Creators | Larkin, James |
| Publisher | ePublications@bond |
| Source Sets | Australiasian Digital Theses Program |
| Detected Language | English |
| Source | Theses |
Page generated in 0.002 seconds