1
Introduction

Roy H. Campbell

Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL, USA

Mission assurance for critical cloud applications is of growing importance to governments and military organizations, yet mission-critical cloud computing may face the challenge of needing to use hybrid (public, private, and/or heterogeneous) clouds and require the realization of “end-to-end” and “cross-layered” security, dependability, and timeliness. In this book, we consider cloud applications in which assigned tasks or duties are performed in accordance with an intended purpose or plan in order to accomplish an assured mission.

1.1 Introduction

Rapid technological advancements in global networking, commercial off-the-shelf technology, security, agility, scalability, reliability, and mobility created a window of opportunity in 2009 for reducing the costs of computation and led to the development of what is now known as cloud computing [1–3]. Later, in 2010, the Obama Administration [4] announced an

“extensive adoption of cloud computing in the federal government to improve information technology (IT) efficiency, reduce costs, and provide a standard platform for delivering government services. In a cloud computing environment, IT resources—services, applications, storage devices and servers, for example—are pooled and managed centrally. These resources can be provisioned and made available on demand via the Internet. The cloud model strengthens the resiliency of mission-critical applications by removing dependency on underlying hardware. Applications can be easily moved from one system to another in the event of system failures or cyber attacks” [5].

In the same year, the Air Force signed an initial contract with IBM to build a mission-assured cloud computing capability [5].

Cloud computing was eventually defined by the National Institute of Standards and Technology (as finalized in 2011) as follows [6]: “Cloud computing is a model for enabling ubiquitous, convenient, on-demand network access to a shared pool of configurable computing resources (e.g., networks, servers, storage, applications, and services) that can be rapidly provisioned and released with minimal management effort or service provider interaction. This cloud model is composed of five essential characteristics, three service models, and four deployment models.” That model of cloud computing is depicted in Table 1.1.

Table 1.1 Model of cloud computing.

Service Models

Deployment Models

Software as a Service

Private Cloud Community Cloud Hybrid Cloud Public Cloud

Platform as a Service

Infrastructure as a Service

Essential Characteristics

Resource Pooling

Rapid Elasticity

Measured Service

Broad Network Access

One of the economic reasons for the success of cloud computing has been the scalability of the computational resources that it provides to an organization. Instead of requiring users to size a planned computation exactly (e.g., in terms of the number of needed Web servers, file systems, databases, or compute engines), cloud computing allows the computation to scale easily in a time-dependent way. Thus, if a service has high demand, it can be replicated to make it more available. Instead of having two Web servers provide a mission-critical service, the system might allow five more Web servers to be added to the service to increase its availability. Likewise, if demand for a service drops, the resources it uses can be released, and thus be freed up to be used for other worthwhile computation. This flexible approach allows a cloud to economically support a number of organizations at the same time, thereby lowering the costs of cloud computation. In later chapters, we will discuss scaling performance and how to assure the correctness of a mission-oriented cloud computation as it changes in size, especially when the scaling occurs dynamically (i.e., is elastic).

1.1.1 Mission-Critical Cloud Solutions for the Military

As government organizations began to adopt cloud computing, security, availability, and robustness became growing concerns; there was a desire to use cloud computing even in mission-critical contexts, where a mission-critical system is one that is essential to the survival of an organization. In 2010, in response to military recognition of the inadequacy of the then state-of-the-art technologies, IBM was awarded an Air Force contract to build a secure cloud computing infrastructure capable of supporting defense and intelligence networks [5]. However, the need for cloud computing systems that could support missions involved more numerous major concerns than could easily be solved in a single, focused initiative and, in particular, raised the question of how to assure cloud support for mission-oriented computations—the subject of this book. Mission-critical cloud computing can stretch across private, community, hybrid, and public clouds, requiring the realization of “end-to-end” and “cross-layered” security, dependability, and timeliness. That is, cloud computations and computing systems should survive malicious attacks and accidental failures, should be secure, and should execute in a timely manner, despite the heterogeneous ownership and nature of the hardware components.

End-to-end implies that the properties should hold throughout the lifetime of individual events, for example, a packet transit or a session between two machines, and that they should be assured in a manner that is independent of the environment through which such events pass. Similarly, cross-layer encompasses multiple layers, from the end device through the network and up to the applications or computations in the cloud. A survivable and distributed cloud-computing-based infrastructure requires the configuration and management of dynamic systems-of-systems with both trusted and partially trusted resources (including data, sensors, networks, computers, etc.) and services sourced from multiple organizations. For mission-critical computations and workflows that rely on such dynamically configured systems-of-systems, we must ensure that a given configuration doesn't violate any security or reliability requirements. Furthermore, we should be able to model the trustworthiness of a workflow or computation's completion for a given configuration in order to specify the right configuration for high assurance.

Rapid technological advances and computer-based weapons systems have created the need for net-centric military superiority. Overseas commitments and operations stretch net-centricity with global networking requirements, use of government and commercial off-the-shelf technology, and the need for agility, mobility, and secure computing over a mixture of blue and gray networks. (Blue networks are military networks that are considered secure, while gray networks are those in private hands, or run by other nations, that may not be secure.) An important goal is to ensure the confidentiality and integrity of data and communications needed to get missions done, even amid cyberattacks and failures.

1.2 Overview of the Book

This book encompasses the topics of architecture, design, testing, and formal verification for assured cloud computing. The authors propose approaches for using formal methods to analyze, reason, prototype, and evaluate the architectures, designs, and performance of secure, timely, fault-tolerant, mission-oriented cloud computing. They examine a wide range of necessary assured cloud computing components and many urgent concerns of these systems.

The chapters of this book provide research overviews of (1) flexible and dynamic distributed cloud-computing-based architectures that are survivable; (2) novel security primitives, protocols, and mechanisms to secure and support assured computations; (3) algorithms and techniques to enhance end-to-end timeliness of computations; (4) algorithms that detect security policy or reliability requirement violations in a given configuration; (5) algorithms that dynamically configure resources for a given workflow based on security policy and reliability requirements; and (6) algorithms, models, and tools to estimate the probability of completion of a workflow for a given configuration. Further, we discuss how formal methods can be used to analyze designed architectures, algorithms, protocols, and techniques to verify the properties they enable. Prototypes and implementations may be built, formally verified against specifications, and tested as components in real systems, and their performance can be evaluated.

While our research has spanned most of the cloud computing phenomenon's lifetime to date, it has had, like all fast-moving technological advances, only a short history (starting 2011). Much work is still to be done as cloud computing evolves and “mission-critical” takes on new meanings within the modern world. Wherever possible, throughout the volume (and in the concluding chapter) we have offered reflections on the state of the art and commented on future directions.

• Chapter 2: Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude, José Meseguer in...