Formal methods for secure software construction
Ben Goodspeed · Saint Mary's University Institutional Repository (Saint Mary's University) · 2016
Formal Methods for Secure Software Construction by Ben GoodspeedThe objective of this thesis is to evaluate the state of the art in formal methods usage in secure computing.From this evaluation, we analyze the common components and search for weaknesses within the common workflows of secure software construction.An improved workflow is proposed and appropriate system requirements are discussed.The systems are evaluated and further tools in the form of libraries of functions, data types and proofs are provided to simplify work in the selected system.Future directions include improved program and proof guidance via compiler error messages, and targeted proof steps. April 8, 2016"There is no such thing as perfect security, only varying levels of insecurity."