FORMALLY ANALYZING AND VERIFYING SECURE SYSTEM DESIGN AND IMPLEMENTATION

Abstract

It is imperative to formally verify the design and implementation of secure systems before they are deployed for real-life use. Unfortunately, existing formal methods are unscalable and often only work with highly abstract models, and thus they are far from expectation of industrial practitioners. As a result, we still have not witnessed a wide range of practical use. Therefore, this thesis aims to extend and improve the techniques of formal methods to enhance their practical use for analyzing secure system design and implementation, and we focus on three of the most security-critical scenarios: trusted computing, web authentication and mobile computing. This thesis adapts formal methods, including symbolic model checking, specification extraction and software model checking, to detect vulnerabilities in these scenarios. Many real-world systems, such as Facebook Connect Protocol, Windows Live Messenger Connect and Android applications are analyzed.