Formal Modeling and Verification of CloudProxy

Wei Yang Tan

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2014-112
May 16, 2014

http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-112.pdf

Services running in the cloud face threats from several parties, including malicious clients, administrators, and external attackers. CloudProxy is a recently-proposed framework for secure deployment of cloud applications. In this thesis, we present the first formal model of CloudProxy, including a formal specification of desired security properties. We model CloudProxy as a transition system in the UCLID modeling language, using term-level abstraction. Our formal specification includes both safety and non-interference properties. We use induction to prove these properties, employing a back-end SMT-based verification engine. Further, we structure our proof as an "assurance case", showing how we decompose the proof into various lemmas, and listing all assumptions and axioms employed. We also perform some limited model validation to gain assurance that the formal model correctly captures behaviors of the implementation.

Advisor: Sanjit A. Seshia


BibTeX citation:

@mastersthesis{Tan:EECS-2014-112,
    Author = {Tan, Wei Yang},
    Title = {Formal Modeling and Verification of CloudProxy},
    School = {EECS Department, University of California, Berkeley},
    Year = {2014},
    Month = {May},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-112.html},
    Number = {UCB/EECS-2014-112},
    Abstract = {Services running in the cloud face threats from several parties, including malicious clients, administrators, and external attackers. CloudProxy is a recently-proposed framework for secure deployment of cloud applications. In this thesis, we present the first formal model of CloudProxy, including a formal specification of desired security properties. We model CloudProxy as a transition system in the UCLID modeling language, using term-level abstraction. Our formal specification  includes both safety and non-interference properties. We use induction to prove these properties, employing a back-end SMT-based verification engine. Further, we structure our proof as an "assurance case", showing how we decompose the proof into various lemmas, and listing all assumptions and axioms employed. We also perform some limited model validation to gain assurance that the formal model correctly captures behaviors of the implementation.}
}

EndNote citation:

%0 Thesis
%A Tan, Wei Yang
%T Formal Modeling and Verification of CloudProxy
%I EECS Department, University of California, Berkeley
%D 2014
%8 May 16
%@ UCB/EECS-2014-112
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-112.html
%F Tan:EECS-2014-112