Assured Cloud Computing Special Seminar: Design and Validation of Distributed Data Stores using Formal Methods

  • Posted on January 25, 2016 at 3:17 pm by
  • Categorized Events.
  • Comments are off for this post.

Peter OlveczkyPeter Ölveczky, University of Oslo
February 10, 4 p.m. 2405 Siebel Center


Abstract: To deal with large amounts of data and to ensure high availability, many cloud computing systems rely on distributed, partitioned, and/or replicated data stores. However, such data stores are complex artifacts that are very hard to design and analyze, as they satisfy different notions of “consistency”.

We therefore propose to use formal methods to model distributed data stores, and to analyze both their correctness properties and their performance. In particular, one goal is to identify key building blocks in the design of such data stores, and their properties, so that new data stores, or different versions of existing data stores, can be designed by reusing such “components”.

This talk, which is based on joint work with Jon Grov and a number of members of the Assured Cloud Computing Center, gives a high-level overview of this ongoing work, which has already been used to design and analyze new versions of Google’s Megastore, Facebook/Apache’s Cassandra, and UC Berkeley’s RAMP distributed data stores.

Bio: Peter Ölveczky received his PhD in computer science from the University of Bergen, Norway, in 2000, having performed his thesis research at SRI International. He was assistant and then associate professor at the University of Oslo 2001-2008, and has been a full professor there since 2008. He was also a post-doctoral researcher at the University of Illinois at Urbana-Champaign (UIUC) 2002-2004, and has been a visiting researcher at UIUC since 2008.

Ölveczky’s research focuses on formal methods, in particular for real-time systems. He  is the developer of the Real-Time Maude tool, which has been used to formally model and analyze a large range of advanced systems, including scheduling protocols, distributed data stores, wireless sensor network algorithms, the human thermoregulatory system, mobile ad hoc networks, avionics systems, and so on. Ölveczky has organized 9 international scientific workshops/conferences, and has edited a number of scientific books and journal issues.

Trust & Security/Assured Cloud Computing Joint Seminar: Security-Aware Virtual Machine Allocation in the Cloud: A Game Theoretic Approach

  • Posted on September 3, 2015 at 11:40 am by
  • Categorized Events.
  • Comments are off for this post.

Charles Kamhoua

Charles A. Kamhoua, U.S. Air Force Research Laboratory
September 2, 4:00 p.m., 2405 Siebel Center

Slides | Video

Research paper presented: Luke Kwiat, Charles A. Kamhoua, Kevin Kwiat, Jian Tang, and Andrew Martin, “Security-aware Virtual Machine Allocation in the Cloud: A Game Theoretic Approach”, IEEE International Conference on Cloud Computing (IEEE Cloud 2015), New York, NY, June 27-July 2, 2015. [full text]

Abstract: With the growth of cloud computing, many businesses, both small and large, are opting to use cloud services compelled by a great cost savings potential. This is especially true of public cloud computing which allows for quick, dynamic scalability without many overhead or long-term commitments. However, one of the largest dissuasions from using cloud services comes from the inherent and unknown danger of a shared platform such as the hypervisor. An attacker can attack a virtual machine (VM) and then go on to compromise the hypervisor. If successful, then all virtual machines on that hypervisor can become compromised. This is the problem of negative externalities, where the security of one player affects the security of another. This work shows that there are multiple Nash equilibria for the public cloud security game. It also demonstrates that we can allow the players’ Nash equilibrium profile to not be dependent on the probability that the hypervisor is compromised, reducing the factor externality plays in calculating the equilibrium. Finally, by using our allocation method, the negative externality imposed onto other players can be brought to a minimum compared to other common VM allocation methods.

Bio: Charles A. Kamhoua received his B.S. in Electronic from the University of Douala (ENSET), Cameroon in 1999, and the M.S. in Telecommunication and Networking and PhD in Electrical Engineering from Florida International University in 2008 and 2011 respectively. In 2011, he joined the Cyber Assurance Branch of the U.S. Air Force Research Laboratory (AFRL), Rome, New York, as a National Academies Postdoctoral Fellow and became a Research Electronics Engineer in 2012. Prior to joining AFRL, he was an educator for more than 10 years. His current research interests cover the application of game theory and mechanism design to cyber security and survivability, with over 50 technical publications in prestigious journals and International conferences including a Best Paper Award at the 2013 IEEE FOSINT-SI. Dr. Kamhoua has been recognized for his scholarship and leadership with numerous prestigious awards including ten Air Force Notable Achievement Awards, the 2015 AFOSR Windows on the World Visiting Research Fellowship at Oxford University, UK, an AFOSR basic research award of $645K, the 2015 Black Engineer of the Year Award (BEYA), the 2015 NSBE Golden Torch Award – Pioneer of the Year, a selection to the 2015 Heidelberg Laureate Forum, a 2011 NSF PIRE award at Fluminense Federal University, Brazil, and the 2008 FAEDS teacher award. He is an advisor for the National Research Council, a Senior Member of IEEE, a member of ACM, the FIU alumni association, and NSBE.