Abstract
| Model checking is a method of formally verifying properties of finite state machines. By describing operating system structure and system authorization policies using finite state machines, model checking may be used to verify useful properties of policies, improving the chances of developing a secure system. The technique is demonstrated on authorization systems from an Active Network, and from a simplified UNIX-like environment. |
My senior thesis is now available here for download. The preferred format is postscript.
Needless to say, while the thesis is at this point complete, the theory and concepts behind it should be considered a work in progress. Please feel free to email me with comments, suggestions, or reports of errors, at robert@fledge.watson.org.
I am currently assembling minor corrections and editing changes for a second revision appropriate for publication; comments and suggestions relating to this would be much appreciated.
Return to my homepage.