Formal Modeling and Verification of CloudProxy

Wei Yang Tan, Rohit Sinha, John Manferdelli, and Sanjit A. Seshia. Formal Modeling and Verification of CloudProxy. In 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), pp. 87–104, July 2014.

Download

[pdf] 

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 work, 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.

BibTeX

@inproceedings{tan-vstte14,
  author    = {Wei Yang Tan and Rohit Sinha and John Manferdelli and Sanjit A. Seshia},
  title     = {Formal Modeling and Verification of CloudProxy},
 booktitle = {6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE)},
 month = "July",
 year = {2014},
 pages = {87--104},
  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 work, 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.},
}