Computer Science Department
School of Computer Science, Carnegie Mellon University
A Symbiotic Relationship Between Formal Methods and Security
Jeannette M. Wing
December 1998
This paper will appear in an edited volume resulting from the series of two
workshops held in 1998, sponsored by the ONR and HSF, entitled
Workshops on Computer Security, Fault Tolerance, and Software Assurance:
From Needs to Solutions
CMU-CS-98-188.ps
CMU-CS-98-188.pdf
Security played a significant role in the development of formal
methods in the 70s and early 80s. Have the tables turned? Are formal
methods now ready to play a significant role in the development of
more secure systems? While not a panacea, the answer is yes, formal
methods can and should play such a role. In this paper I first review
the limits of formal methods. Then after a brief historical
excursion, I summarize some recent results on how model checking
and theorem proving tools revealed new and known flaws in
authentication protocols. Looking to the future I discuss the
challenges and opportunities for formal methods in analyzing the
security of systems, above and beyond the protocol level.
13 pages
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu
School of Computer Science homepage