Automatic Tools for Building Secure Systems

Building a secure system is a complex and error-prone process in computing. System designers and developers face many challenges: What does it mean for a system to be secure? How do I know whether my system is secure? Will the security of my system break if I add a new component? SSL/TLS and other standard protocols do not work in my scenario. How can I find ways to achieve security in my system efficiently? How can I make sure the implementation adheres to the design? Finding answers to these questions is essential to building secure, efficient systems; however, the complexity, subtlety, and interactions among different components in a large system put the problem beyond the reach of even experienced security experts, not to mention average programmers who lack security expertise. As a result, the current design and implementation process for secure systems is slow, expensive, and often results in a vulnerable system. In my thesis, I propose a new automatic approach for building security protocols. In particular, I designed and built a suite of automatic tools, Athena, containing three components: 1) APV: an Automatic Protocol Analyzer; 2) APG: an Automatic Protocol Generator; 3) ACG: an Automatic Code Generator. In this talk, I'll discuss how this toolkit enables a new automatic approach for building security protocols that is more efficient, economical, and with higher security guarantee than the current approach.