Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/120112
Title: FORMALLY ANALYZING AND VERIFYING SECURE SYSTEM DESIGN AND IMPLEMENTATION
Authors: BAI GUANGDONG
Keywords: Security, Formal Analysis, Model Checking, Authentication, Trusted Computing, Android
Issue Date: 17-Feb-2015
Source: BAI GUANGDONG (2015-02-17). FORMALLY ANALYZING AND VERIFYING SECURE SYSTEM DESIGN AND IMPLEMENTATION. ScholarBank@NUS Repository.
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.
URI: http://scholarbank.nus.edu.sg/handle/10635/120112
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
BaiGD.pdf1.61 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

177
checked on Jan 20, 2018

Download(s)

279
checked on Jan 20, 2018

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.