Colloquium Details
Automatic Tools for Building Secure Systems
| Author: | Dawn Song Department of Computer Science, University of California, Berkeley |
|---|---|
| Date: | February 07, 2002 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
Abstract
Building a secure system is one of the most complex and error-prone processes in computing. As a system designer/developer, one is often puzzled by many questions and challenges: What does it really mean for my system to be secure? How do I know whether my system is secure? Will the security of my system break if I add this new component? How can I find a more efficient authentication protocol for my new system? How can I know that 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 are often beyond the reach of even the most 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 designed and built a suite of automatic tools to facilitate understanding, analyzing, optimizing, and implementing real-world secure systems:
Athena: an Automatic Protocol Analyzer.
Security protocols are notoriously hard to get right. Many proposed protocols in the literature have serious flaws, even though they are often designed and scrutinized by security experts. I designed a new efficient algorithm for analyzing security protocols, and built an automatic security protocol analyzer: Athena. Athena was one of the first automatic tools able to both produce a proof (when a protocol is correct), and generate a counter example (when a protocol is flawed). Athena exploits powerful state-space reduction techniques. This system runs orders of magnitudes faster than previous automatic protocol verifiers (often taking only milliseconds to analyze a protocol on a contemporary PC).
APG: an Automatic Protocol Generator.
Given a set of security requirements and system metrics, APG explores the protocol space and finds the optimal security protocols satisfying the security requirements. (Optimality is measured using the specified system metrics.) The APG project was the first to propose automatic generation of security protocols and demonstrate that this is a viable new approach for designing and building secure systems. APG has generated new protocols that are faster and more secure than the published results in the security literature for a variety of system settings.
ACG: an Automatic Code Generator.
Human programming errors are inevitable and hard to detect and debug. These programming errors significantly jeopardize the security of a system even when the design has no flaws. ACG is an automatic compiler; it translates high level specifications of security protocols directly and faithfully into low level implementations (Java source code), eliminating the need for manual implementation of security protocols.
These tools allow developers to specify high level security properties, and then automatically generate the security protocols that suit the given system the best and automatically implement it into Java source code. With these tools, the system development process will become more productive and effective, and the systems will become more secure. This is an important first step towards a new programming model for building systems efficiently and securely.
Biography
Dawn Xiaodong Song is a Ph.D. candidate in the Department of Computer Science at the University of California, Berkeley. She received her M.S. in Computer Science from Carnegie Mellon University and her B.S. from Tsinghua Unversity, China. Her main research interests are security and applied cryptography (including security in systems, networking, databases, and electronic commerce), applications of program analysis, model checking, and software engineering techniques to computer security.