| Building a secure system is one of the most complex and error-prone processes in computing. Unfortunately, the current design and development process is primarily manual, ad hoc, and far from satisfactory. In this thesis, I propose a new automatic approach for building secure systems. With this approach, users only need to specify desired security and system requirements. Such an automatic system can then explore the possible design space, generate design candidates, evaluate those candidates to find the most efficient correct design, and finally generate source code implementing the optimal design. Compared to the manual design and development process, this automatic approach is faster, more economical, yields protocols and implementations of higher security and efficiency.; To demonstrate this automatic approach for building secure systems, we have focused on one of the most important aspects, designing and developing security protocols. In particular, I have designed and developed an automatic toolbox, called Athena, for automatic protocol generation, verification and implementation. The system contains three components: the automatic protocol generator (APG), the automatic protocol verifier (APV), and the automatic code generator (ACG). APV proposes a new automatic approach for security protocol analysis. Given a security protocol and desired security requirements, APV analyzes the protocol automatically. When APV terminates, it can either generate a proof of correctness, if the protocol satisfies the given requirements, or generate a counterexample, if the protocol is flawed. APV is the first automatic approach that has both the capability of providing a proof of correctness when the protocol is correct and the capability of generating a counterexample when the protocol is flawed. Athena runs efficiently and this high efficiency enables the approach of automatic protocol generation. APG uses powerful pruning techniques to drastically reduce the protocol search space. It is the first approach for automatic generation of security protocols. In our experiments, APG has generated new protocols that are more efficient than previous protocols proposed in the literature for different system settings. The composition of APG, APV and ACG forms an end-to-end system, Athena, which is the first system able to automatically generate, verify, and implement security protocols. |
